Source indexedtheorem · leanprover/lean4:v4.32.0

Kadiri.zetaCounting_abs_N_le_backlund_majorant

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:805 to 830

Source documentation

Any RvM estimate gives an absolute-value bound for N(T).

Exact Lean statement

theorem zetaCounting_abs_N_le_backlund_majorant {b₁ b₂ b₃ T : ℝ}
    (hRvM : riemannZeta.Riemann_vonMangoldt_bound b₁ b₂ b₃) (hT : 2 ≤ T) :
    |riemannZeta.N T| ≤ zetaCountingBacklundMajorant b₁ b₂ b₃ T

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem zetaCounting_abs_N_le_backlund_majorant {b₁ b₂ b₃ T : ℝ}    (hRvM : riemannZeta.Riemann_vonMangoldt_bound b₁ b₂ b₃) (hT : 2 ≤ T) :    |riemannZeta.N T| ≤ zetaCountingBacklundMajorant b₁ b₂ b₃ T := by  have hbound := hRvM T hT  unfold zetaCountingBacklundMajorant zetaCountingMainTerm  calc    |riemannZeta.N T|        = |(riemannZeta.N T -              (T / (2 * Real.pi) * Real.log (T / (2 * Real.pi)) -                T / (2 * Real.pi) + 7 / 8)) +              (T / (2 * Real.pi) * Real.log (T / (2 * Real.pi)) -                T / (2 * Real.pi) + 7 / 8)| := by          ring_nf    _ ≤ |riemannZeta.N T -              (T / (2 * Real.pi) * Real.log (T / (2 * Real.pi)) -                T / (2 * Real.pi) + 7 / 8)| +          |T / (2 * Real.pi) * Real.log (T / (2 * Real.pi)) -                T / (2 * Real.pi) + 7 / 8| := by          exact abs_add_le _ _    _ ≤ riemannZeta.RvM b₁ b₂ b₃ T +          |T / (2 * Real.pi) * Real.log (T / (2 * Real.pi)) -                T / (2 * Real.pi) + 7 / 8| := by          exact add_le_add_left hbound _    _ = |T / (2 * Real.pi) * Real.log (T / (2 * Real.pi)) -                T / (2 * Real.pi) + 7 / 8| + riemannZeta.RvM b₁ b₂ b₃ T := by          ring