Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.log_dyadic_le_nat_succ

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:879 to 890

Source documentation

The logarithm of a dyadic height is bounded by its dyadic exponent.

Exact Lean statement

lemma log_dyadic_le_nat_succ (k : ℕ) :
    Real.log ((2 : ℝ) ^ (k + 1)) ≤ ((k + 1 : ℕ) : ℝ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma log_dyadic_le_nat_succ (k : ℕ) :    Real.log ((2 : ℝ) ^ (k + 1)) ≤ ((k + 1 : ℕ) : ℝ) := by  have hlog2_le_one : Real.log (2 : ℝ) ≤ 1 := by    linarith [Real.log_le_sub_one_of_pos (by norm_num : (0 : ℝ) < 2)]  have hk_nonneg : 0 ≤ ((k + 1 : ℕ) : ℝ) := by positivity  calc    Real.log ((2 : ℝ) ^ (k + 1))        = ((k + 1 : ℕ) : ℝ) * Real.log (2 : ℝ) := by          rw [Real.log_pow]    _ ≤ ((k + 1 : ℕ) : ℝ) * 1 := by          exact mul_le_mul_of_nonneg_left hlog2_le_one hk_nonneg    _ = ((k + 1 : ℕ) : ℝ) := by ring