Documentation

MathlibNt.SieveTheory.LiLiuGoldbachG11MainMassBuchstab

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

An actual-label finite sum, not a prime integral or a numerical evaluation.

Equations
Instances For
    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_rough_upper_buchstab (η : ℝ) (hη : 0 < η) :
    ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), ↑(LiLiuPrereqBuchstab.roughCount (↑N / ↑(goldbachG11LabelProd v)) ↑v.snd.snd.snd) ≤ goldbachG11BuchstabMass (↑N / ↑(goldbachG11LabelProd v)) ↑v.snd.snd.snd + η * (↑N / ↑(goldbachG11LabelProd v)) / Real.log ↑v.snd.snd.snd

    Consume the nonempty upper endpoint, not the empty epsilon-one window difference.

    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11FullRoughMass_le_buchstabUpper (η : ℝ) (hη : 0 < η) :
    ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachG11FullRoughMass N ≤ goldbachG11BuchstabUpperMass N η
    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11BuchstabUpperMass_eventually_nonneg (η : ℝ) (hη : 0 < η) :
    ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → 0 ≤ goldbachG11BuchstabUpperMass N η
    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeWindowMainMass_le_buchstabUpper (η : ℝ) (hη : 0 < η) :
    ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (ε : ℝ), 400 * goldbachG11PrimeWindowMainMass N ε ≤ goldbachG11BuchstabUpperMass N η + 8400 * ↑N / ↑N ^ (4 / 53)

    A single threshold precedes every actual window parameter; no factor 1 - epsilon survives the passage to the full rough mother.

    Inspect dependencies

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