noncomputable def MathlibNt.SieveTheory.proposition131iiPhaseConstant : ℝ

An exported spelling of the (private) constant in Proposition 10.23.

Equations

• MathlibNt.SieveTheory.proposition131iiPhaseConstant = Section10CanonicalXi.xi (Real.exp 2) + Real.log (Section10CanonicalXi.xi (Real.exp 2) + 3)

theorem MathlibNt.SieveTheory.proposition1023_coarse_phase_exported : ∀ᶠ (s : ℝ) in Filter.atTop, ∫ (t : ℝ) in 1..s, Section10CanonicalXi.xi t ≤ s * Real.log s + s * Real.log (Real.log (3 * s)) + proposition131iiPhaseConstant * s

theorem MathlibNt.SieveTheory.proposition131iiUniformQuantitativeLower_of_source {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : SwitchingPrinciple.SuzukiLemma144KappaOne.Proposition131iiUniformQuantitativeLower H

Proposition 13.1(ii), lower half, uniformly for the two signs. All analytic inputs are extracted from the Section-13 source contract.