English
For a > 0, the function x ↦ log x / x^a is decreasing on [exp(1/a), ∞).
Русский
Для a > 0 функция x ↦ log x / x^a убывает на [exp(1/a), ∞).
LaTeX
$$$\forall x,y\in\mathbb{R},\ e^{1/a} \le x \le y \Rightarrow \dfrac{\log x}{x^a} \ge \dfrac{\log y}{y^a}$, \quad a>0$$
Lean4
theorem log_div_self_antitoneOn : AntitoneOn (fun x : ℝ => log x / x) {x | exp 1 ≤ x} :=
by
simp only [AntitoneOn, mem_setOf_eq]
intro x hex y hey hxy
have x_pos : 0 < x := (exp_pos 1).trans_le hex
have y_pos : 0 < y := (exp_pos 1).trans_le hey
have hlogx : 1 ≤ log x := by rwa [le_log_iff_exp_le x_pos]
have hyx : 0 ≤ y / x - 1 := by rwa [le_sub_iff_add_le, le_div_iff₀ x_pos, zero_add, one_mul]
rw [div_le_iff₀ y_pos, ← sub_le_sub_iff_right (log x)]
calc
log y - log x = log (y / x) := by rw [log_div y_pos.ne' x_pos.ne']
_ ≤ y / x - 1 := (log_le_sub_one_of_pos (div_pos y_pos x_pos))
_ ≤ log x * (y / x - 1) := (le_mul_of_one_le_left hyx hlogx)
_ = log x / x * y - log x := by ring
