English
For a > 0, the function log x / x^a is decreasing on [exp(1/a), ∞).
Русский
Для a > 0 функция log x / x^a убывает на [exp(1/a), ∞).
LaTeX
$$$\forall x,y\in\mathbb{R},\ e^{1/a} \le x \le y \Rightarrow \frac{\log x}{x^a} \ge \frac{\log y}{y^a}$, \quad a>0$$
Lean4
theorem log_div_self_rpow_antitoneOn {a : ℝ} (ha : 0 < a) :
AntitoneOn (fun x : ℝ => log x / x ^ a) {x | exp (1 / a) ≤ x} :=
by
simp only [AntitoneOn, mem_setOf_eq]
intro x hex y _ hxy
have x_pos : 0 < x := lt_of_lt_of_le (exp_pos (1 / a)) hex
have y_pos : 0 < y := by linarith
nth_rw 1 [← rpow_one y]
nth_rw 1 [← rpow_one x]
rw [← div_self (ne_of_lt ha).symm, div_eq_mul_one_div a a, rpow_mul y_pos.le, rpow_mul x_pos.le,
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_iff_right₀ (one_div_pos.mpr ha)]
refine log_div_self_antitoneOn ?_ ?_ ?_
· simp only [Set.mem_setOf_eq]
convert rpow_le_rpow _ hex (le_of_lt ha) using 1
· rw [← exp_mul]
simp only [Real.exp_eq_exp]
field_simp
positivity
· simp only [Set.mem_setOf_eq]
convert rpow_le_rpow _ (_root_.trans hex hxy) (le_of_lt ha) using 1
· rw [← exp_mul]
simp only [Real.exp_eq_exp]
field_simp
positivity
gcongr
