Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.zeroSquareTail_le_imagSquareTail_of_large_im

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:723 to 733

Source documentation

Above height one, the norm-square tail is bounded by the height-square tail.

Exact Lean statement

lemma zeroSquareTail_le_imagSquareTail_of_large_im {rho : NontrivialZeros}
    (hlarge : 1 ≤ |(rho : ℂ).im|) :
    zeroSquareTail 0 rho ≤ zeroImagSquareTail rho

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma zeroSquareTail_le_imagSquareTail_of_large_im {rho : NontrivialZeros}    (hlarge : 1 ≤ |(rho : ℂ).im|) :    zeroSquareTail 0 rho ≤ zeroImagSquareTail rho := by  have him_pos : 0 < |(rho : ℂ).im| := lt_of_lt_of_le zero_lt_one hlarge  have hinv : ‖(rho : ℂ)‖⁻¹ ≤ |(rho : ℂ).im|⁻¹ :=    inv_anti₀ him_pos (Complex.abs_im_le_norm (rho : ℂ))  have hinv_nonneg : 0 ≤ ‖(rho : ℂ)‖⁻¹ := inv_nonneg.mpr (norm_nonneg _)  have hpow := pow_le_pow_left₀ hinv_nonneg hinv 2  unfold zeroSquareTail zeroImagSquareTail  rw [zero_sub, norm_neg]  exact hpow