Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.zeroImagSquareTail_le_dyadic_inv_sq

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:760 to 767

Source documentation

Inside dyadic shell k, each height-square term is bounded by 2^(-2k).

Exact Lean statement

lemma zeroImagSquareTail_le_dyadic_inv_sq {k : ℕ} {rho : NontrivialZeros}
    (hrho : zeroHeightDyadicShell k rho) :
    zeroImagSquareTail rho ≤ (((2 : ℝ) ^ k)⁻¹) ^ (2 : ℕ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma zeroImagSquareTail_le_dyadic_inv_sq {k : ℕ} {rho : NontrivialZeros}    (hrho : zeroHeightDyadicShell k rho) :    zeroImagSquareTail rho ≤ (((2 : ℝ) ^ k)⁻¹) ^ (2 : ℕ) := by  unfold zeroImagSquareTail  have hpow_pos : 0 < (2 : ℝ) ^ k := pow_pos (by norm_num) k  have hinv : |(rho : ℂ).im|⁻¹ ≤ ((2 : ℝ) ^ k)⁻¹ := inv_anti₀ hpow_pos hrho.1  have hinv_nonneg : 0 ≤ |(rho : ℂ).im|⁻¹ := inv_nonneg.mpr (abs_nonneg _)  exact pow_le_pow_left₀ hinv_nonneg hinv 2