Documentation

MathlibNt.SieveTheory.LiLiuGoldbachB10LogMass

source
noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ActualTriangleMass (N : ℕ) :
ℝ

The actual finite C10 weighted prime-pair mass whose one-sided limit is controlled by Liu's printed integral I10.

Equations
Instances For
    Inspect dependencies

    MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ActualTriangleMass · compiled type and proof/definition references.

    source
    noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10I10 :
    ℝ

    The exact double integral I10 from Liu's printed (5.46).

    Equations
    Instances For
      Inspect dependencies

      MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10I10 · compiled type and proof/definition references.

      source
      theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ActualTriangleMass_le_I10_eventually {η : ℝ} (hη : 0 < η) :
      ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachB10ActualTriangleMass N ≤ goldbachB10I10 + η

      The actual C10 weighted prime-pair mass is eventually bounded above by I10 + η for every fixed η > 0.

      Inspect dependencies

      MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ActualTriangleMass_le_I10_eventually · compiled type and proof/definition references.