Source indexedlemma · leanprover/lean4:v4.32.0

Real.Stirling.log_three_le_coef_mul_log_one_add

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/StripBounds.lean:71 to 81

Source documentation

For x ≥ 1, log 3 ≤ (log 3 / log 2) * log (1 + x).

Exact Lean statement

lemma log_three_le_coef_mul_log_one_add {x : ℝ} (hx : 1 ≤ x) :
    Real.log 3 ≤ (Real.log 3 / Real.log 2) * Real.log (1 + x)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma log_three_le_coef_mul_log_one_add {x : ℝ} (hx : 1 ≤ x) :    Real.log 3 ≤ (Real.log 3 / Real.log 2) * Real.log (1 + x) := by  have hlog2_pos : 0 < Real.log 2 := Real.log_pos (by norm_num : (1 : ℝ) < 2)  have hlog2_ne : Real.log 2 ≠ 0 := ne_of_gt hlog2_pos  have hlog3_pos : 0 < Real.log 3 := Real.log_pos (by norm_num : (1 : ℝ) < 3)  have hcoef_nonneg : 0 ≤ Real.log 3 / Real.log 2 := div_nonneg hlog3_pos.le hlog2_pos.le  have hscaled :      (Real.log 3 / Real.log 2) * Real.log 2 ≤        (Real.log 3 / Real.log 2) * Real.log (1 + x) :=    mul_le_mul_of_nonneg_left (log_one_add_ge_log_two hx) hcoef_nonneg  simpa [div_mul_cancel₀ _ hlog2_ne] using hscaled