Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.abs_zetaCountingMainTerm_core_le

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:928 to 940

Source documentation

Triangle bound for the RvM main term after writing A = T/(2*pi).

Exact Lean statement

lemma abs_zetaCountingMainTerm_core_le (A : ℝ) :
    |A * Real.log A - A + 7 / 8| ≤
      |A * Real.log A| + |A| + (1 : ℝ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma abs_zetaCountingMainTerm_core_le (A : ℝ) :    |A * Real.log A - A + 7 / 8| ≤      |A * Real.log A| + |A| + (1 : ℝ) := by  have hconst : |(7 / 8 : ℝ)| ≤ (1 : ℝ) := by norm_num  calc    |A * Real.log A - A + 7 / 8|        = |(A * Real.log A - A) + (7 / 8 : ℝ)| := by ring_nf    _ ≤ |A * Real.log A - A| + |(7 / 8 : ℝ)| := abs_add_le _ _    _ ≤ (|A * Real.log A| + |A|) + |(7 / 8 : ℝ)| := by          exact add_le_add_left (abs_sub _ _) _    _ ≤ (|A * Real.log A| + |A|) + 1 := by          exact add_le_add_right hconst _    _ = |A * Real.log A| + |A| + 1 := by ring