x y a : ℝ
ha : 0 < a
⊢ ∀ ⦃a_1 : ℝ⦄, exp (1 / a) ≤ a_1 → ∀ ⦃b : ℝ⦄, exp (1 / a) ≤ b → a_1 ≤ b → log b / b ^ a ≤ log a_1 / a_1 ^ a
x y a : ℝ
ha : 0 < a
⊢ AntitoneOn (fun x => log x / x ^ a) {x | exp (1 / a) ≤ x}
simp only [AntitoneOn, mem_setOf_eq]
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
⊢ log y / y ^ a ≤ log x / x ^ a
x y a : ℝ
ha : 0 < a
⊢ ∀ ⦃a_1 : ℝ⦄, exp (1 / a) ≤ a_1 → ∀ ⦃b : ℝ⦄, exp (1 / a) ≤ b → a_1 ≤ b → log b / b ^ a ≤ log a_1 / a_1 ^ a
intro x hex y _ hxy
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
⊢ log y / y ^ a ≤ log x / x ^ a
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
⊢ log y / y ^ a ≤ log x / x ^ a
have x_pos : 0 < x := lt_of_lt_of_le (exp_pos (1 / a)) hex
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ log y / y ^ a ≤ log x / x ^ a
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
⊢ log y / y ^ a ≤ log x / x ^ a
have y_pos : 0 < y := by linarith
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
⊢ log y / y ^ a ≤ log x / x ^ a
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ log y / y ^ a ≤ log x / x ^ a
have x_nonneg : 0 ≤ x := le_trans (le_of_lt (exp_pos (1 / a))) hex
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ log y / y ^ a ≤ log x / x ^ a
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
⊢ log y / y ^ a ≤ log x / x ^ a
have y_nonneg : 0 ≤ y := by linarith
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ log (y ^ 1) / y ^ a ≤ log x / x ^ a
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ log y / y ^ a ≤ log x / x ^ a
nth_rw 1 [← rpow_one y]
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ log (y ^ 1) / y ^ a ≤ log (x ^ 1) / x ^ a
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ log (y ^ 1) / y ^ a ≤ log x / x ^ a
nth_rw 1 [← rpow_one x]
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ log (y ^ a) / y ^ a ≤ log (x ^ a) / x ^ a
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ log (y ^ 1) / y ^ a ≤ log (x ^ 1) / x ^ a
rw [← div_self (ne_of_lt ha).symm, div_eq_mul_one_div a a, rpow_mul y_nonneg, rpow_mul x_nonneg,
  log_rpow (rpow_pos_of_pos y_pos a), log_rpow (rpow_pos_of_pos x_pos a), mul_div_assoc,
  mul_div_assoc, mul_le_mul_left (one_div_pos.mpr ha)]
no goals
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
⊢ 0 < y
linarith
no goals
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
⊢ 0 ≤ y
linarith
case refine'_1
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ x ^ a ∈ {x | exp 1 ≤ x}

case refine'_2
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ y ^ a ∈ {x | exp 1 ≤ x}

case refine'_3
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ x ^ a ≤ y ^ a
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ log (y ^ a) / y ^ a ≤ log (x ^ a) / x ^ a
refine' log_div_self_antitoneOn _ _ _
no goals
case refine'_3
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ x ^ a ≤ y ^ a
exact rpow_le_rpow x_nonneg hxy (le_of_lt ha)
case refine'_1
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ exp 1 ≤ x ^ a
case refine'_1
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ x ^ a ∈ {x | exp 1 ≤ x}
simp only [Set.mem_setOf_eq]
case h.e'_3
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ exp 1 = exp (1 / a) ^ a

case refine'_1
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 0 ≤ exp (1 / a)
case refine'_1
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ exp 1 ≤ x ^ a
convert rpow_le_rpow _ hex (le_of_lt ha) using 1
case h.e'_3
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ exp 1 = exp (1 / a * a)

case refine'_1
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 0 ≤ exp (1 / a)
case h.e'_3
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ exp 1 = exp (1 / a) ^ a

case refine'_1
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 0 ≤ exp (1 / a)
rw [← exp_mul]
case h.e'_3
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 1 = 1 / a * a

case refine'_1
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 0 ≤ exp (1 / a)
case h.e'_3
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ exp 1 = exp (1 / a * a)

case refine'_1
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 0 ≤ exp (1 / a)
simp only [Real.exp_eq_exp]
case refine'_1
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 0 ≤ exp (1 / a)
case h.e'_3
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 1 = 1 / a * a

case refine'_1
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 0 ≤ exp (1 / a)
field_simp [(ne_of_lt ha).symm]
no goals
case refine'_1
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 0 ≤ exp (1 / a)
exact le_of_lt (exp_pos (1 / a))
case refine'_2
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ exp 1 ≤ y ^ a
case refine'_2
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ y ^ a ∈ {x | exp 1 ≤ x}
simp only [Set.mem_setOf_eq]
case h.e'_3
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ exp 1 = exp (1 / a) ^ a

case refine'_2
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 0 ≤ exp (1 / a)
case refine'_2
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ exp 1 ≤ y ^ a
convert rpow_le_rpow _ (_root_.trans hex hxy) (le_of_lt ha) using 1
case h.e'_3
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ exp 1 = exp (1 / a * a)

case refine'_2
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 0 ≤ exp (1 / a)
case h.e'_3
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ exp 1 = exp (1 / a) ^ a

case refine'_2
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 0 ≤ exp (1 / a)
rw [← exp_mul]
case h.e'_3
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 1 = 1 / a * a

case refine'_2
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 0 ≤ exp (1 / a)
case h.e'_3
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ exp 1 = exp (1 / a * a)

case refine'_2
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 0 ≤ exp (1 / a)
simp only [Real.exp_eq_exp]
case refine'_2
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 0 ≤ exp (1 / a)
case h.e'_3
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 1 = 1 / a * a

case refine'_2
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 0 ≤ exp (1 / a)
field_simp [(ne_of_lt ha).symm]
no goals
case refine'_2
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 0 ≤ exp (1 / a)
exact le_of_lt (exp_pos (1 / a))