Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.log_dyadic_le_count_scale

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:857 to 876

Source documentation

The logarithm of a dyadic height is bounded by the dyadic count scale.

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma log_dyadic_le_count_scale (k : ℕ) :    Real.log ((2 : ℝ) ^ (k + 1)) ≤      ((k + 1 : ℕ) : ℝ) * ((2 : ℝ) ^ k) := 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  have hpow1 : (1 : ℝ) ≤ (2 : ℝ) ^ k :=    one_le_pow₀ (by norm_num : (1 : ℝ) ≤ 2)  have hlog_le_k :      ((k + 1 : ℕ) : ℝ) * Real.log (2 : ℝ) ≤ ((k + 1 : ℕ) : ℝ) := by    simpa using mul_le_mul_of_nonneg_left hlog2_le_one hk_nonneg  have hk_le_target :      ((k + 1 : ℕ) : ℝ) ≤ ((k + 1 : ℕ) : ℝ) * ((2 : ℝ) ^ k) := by    simpa using mul_le_mul_of_nonneg_left hpow1 hk_nonneg  calc    Real.log ((2 : ℝ) ^ (k + 1))        = ((k + 1 : ℕ) : ℝ) * Real.log (2 : ℝ) := by          rw [Real.log_pow]    _ ≤ ((k + 1 : ℕ) : ℝ) := hlog_le_k    _ ≤ ((k + 1 : ℕ) : ℝ) * ((2 : ℝ) ^ k) := hk_le_target