Source indexedtheorem · leanprover/lean4:v4.32.0

Real.log_two_le_log_two_mul_mul_inv_norm_of_norm_le

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/ExpGrowth.lean:66 to 74

Source documentation

If z ≠ 0 and ‖z‖ ≤ R, then log 2 ≤ log (2R * ‖z‖⁻¹).

Exact Lean statement

theorem log_two_le_log_two_mul_mul_inv_norm_of_norm_le {z : F} {R : ℝ} (hz0 : z ≠ 0)
    (hz : ‖z‖ ≤ R) :
    Real.log 2 ≤ Real.log ((2 * R) * ‖z‖⁻¹)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem log_two_le_log_two_mul_mul_inv_norm_of_norm_le {z : F} {R : ℝ} (hz0 : z ≠ 0)    (hz : ‖z‖ ≤ R) :    Real.log 2 ≤ Real.log ((2 * R) * ‖z‖⁻¹) := by  have hzpos : 0 < ‖z‖ := norm_pos_iff.2 hz0  have hRdiv : (1 : ℝ) ≤ R / ‖z‖ := (one_le_div hzpos).2 hz  have hle2 : (2 : ℝ) ≤ (2 * R) * ‖z‖⁻¹ := by    have : (2 : ℝ) ≤ 2 * (R / ‖z‖) := by nlinarith    simpa [div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm] using this  exact Real.log_le_log (by norm_num) hle2