Source indexedtheorem · leanprover/lean4:v4.32.0

Kadiri.zetaCountingDyadicMajorantGrowthSource_of_main_term_growth

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:1012 to 1027

Source documentation

Main-term dyadic growth gives growth of the full Backlund majorant.

Exact Lean statement

theorem zetaCountingDyadicMajorantGrowthSource_of_main_term_growth
    (hmain : zetaCountingMainTermDyadicGrowthSource) :
    zetaCountingDyadicMajorantGrowthSource

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem zetaCountingDyadicMajorantGrowthSource_of_main_term_growth    (hmain : zetaCountingMainTermDyadicGrowthSource) :    zetaCountingDyadicMajorantGrowthSource := by  rcases hmain with ⟨C, hC_nonneg, hmain⟩  refine ⟨C + 7, by nlinarith, ?_⟩  intro k  have hmaink := hmain k  have hrvm := zetaCountingRvM_dyadic_le k  unfold zetaCountingDyadicMajorant zetaCountingBacklundMajorant  calc    |zetaCountingMainTerm ((2 : ℝ) ^ (k + 1))| +        riemannZeta.RvM 0.137 0.443 6.1 ((2 : ℝ) ^ (k + 1))        ≤ C * ((k + 1 : ℕ) : ℝ) * ((2 : ℝ) ^ k) +          7 * ((k + 1 : ℕ) : ℝ) * ((2 : ℝ) ^ k) := by          exact add_le_add hmaink hrvm    _ = (C + 7) * ((k + 1 : ℕ) : ℝ) * ((2 : ℝ) ^ k) := by ring