Source indexedlemma · leanprover/lean4:v4.32.0

Complex.one_sub_re_ge_one_sub_zetaAbelContinuationReLower_of_re_le

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFiniteOrder · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/ZetaFiniteOrder.lean:99 to 110

Source documentation

If re z ≤ σ₀, then 1 - σ₀ ≤ re (1 - z) for σ₀ = zetaAbelContinuationReLower.

Exact Lean statement

lemma one_sub_re_ge_one_sub_zetaAbelContinuationReLower_of_re_le {z : ℂ}
    (hz : z.re ≤ zetaAbelContinuationReLower) :
    (1 - zetaAbelContinuationReLower) ≤ (1 - z).re

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma one_sub_re_ge_one_sub_zetaAbelContinuationReLower_of_re_le {z : ℂ}    (hz : z.re ≤ zetaAbelContinuationReLower) :    (1 - zetaAbelContinuationReLower) ≤ (1 - z).re := by  have hz' : z.re ≤ (1 / 10 : ℝ) := by    dsimp [zetaAbelContinuationReLower] at hz    exact hz  have h : (9 / 10 : ℝ) ≤ 1 - z.re := by linarith [hz']  calc (1 - zetaAbelContinuationReLower : ℝ)      = (9 / 10 : ℝ) := by        norm_num [zetaAbelContinuationReLower, one_sub_zetaAbelContinuationReLower]    _ ≤ 1 - z.re := h    _ = (1 - z).re := by simp [Complex.sub_re]