Documentation

MathlibNt.SieveTheory.LiLiuGoldbachG12OutsideBudgetTransport

source
noncomputable def G12OutsideBudget.outside (N : ℕ) (A : Finset MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG12LinkedAtom) (Z Q : ℝ) (c : ℕ → ℝ) :
ℝ

Original full weights on precisely the reduced non-primorial carrier.

Equations
Instances For
    Inspect dependencies

    G12OutsideBudget.outside · compiled type and proof/definition references.

    source
    theorem G12OutsideBudget.outside_eq (N : ℕ) (A : Finset MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG12LinkedAtom) (Z Q : ℝ) (c : ℕ → ℝ) :
    outside N A Z Q c = ∑ d ∈ Finset.Icc 1 ⌊Q⌋₊ with ¬d ∣ (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z).prod id, c d * if (↑N).gcd ↑d = 1 then residue N A d else 0

    Only the remainder, not the well-factorable coefficient, absorbs coprimality.

    Inspect dependencies

    G12OutsideBudget.outside_eq · compiled type and proof/definition references.

    source
    theorem G12OutsideBudget.masked_majorant {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) (A : Finset MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG12LinkedAtom) (hA : A ⊆ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε) (T d : ℕ) :
    d ∈ Finset.Icc 1 T → |if (↑N).gcd ↑d = 1 then residue N A d else 0| ≤ 20 * ↑N / ↑d.totient
    Inspect dependencies

    G12OutsideBudget.masked_majorant · compiled type and proof/definition references.

    source
    theorem G12OutsideBudget.family_budget {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) (A : Finset MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG12LinkedAtom) (hA : A ⊆ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε) (Z Q η : ℝ) (hD : 2 ≤ MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) (hη : 0 < η) (hηsmall : η < 1 / 8) :
    ∑ t ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags true (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z) (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) η Z, |outside N A Z Q ⇑(MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm true (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z) (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) η Z t)| ≤ ↑(MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags true (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z) (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) η Z).card * (20 * ↑N) * (4 / MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η ^ η ^ 2) * (1 + Real.log ↑⌊Q⌋₊) ^ 2

    Explicit transport payment for any genuine submother; no majorant premise.

    Inspect dependencies

    G12OutsideBudget.family_budget · compiled type and proof/definition references.

    source
    theorem G12OutsideBudget.rectangle_residue (N : ℕ) (ε : ℝ) (M T d : ℕ) :
    residue N (Finset.image G12RectangleWF.linkedEmbed (G12LowRectangle.rectangle N ε M T)) d = G12RectangleWF.residue N ε M T d

    Pair cells retain their original coefficient after the canonical embedding.

    Inspect dependencies

    G12OutsideBudget.rectangle_residue · compiled type and proof/definition references.

    source
    theorem G12OutsideBudget.rectangle_outside (N : ℕ) (ε Z Q : ℝ) (M T : ℕ) (c : ℕ → ℝ) :
    outside N (Finset.image G12RectangleWF.linkedEmbed (G12LowRectangle.rectangle N ε M T)) Z Q c = G12RectangleWF.outsidePrimorial N ε Z Q M T c
    Inspect dependencies

    G12OutsideBudget.rectangle_outside · compiled type and proof/definition references.

    source
    theorem G12OutsideBudget.rectangle_family_budget {N : ℕ} (hN : 2 ≤ N) (ε Z Q η : ℝ) (M T : ℕ) (hlow : ↑N ^ (4 / 53) ≤ ↑T) (hhigh : ↑(2 * T) < ↑N ^ (1 / 10)) (hD : 2 ≤ MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) (hη : 0 < η) (hηsmall : η < 1 / 8) :
    ∑ t ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags true (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z) (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) η Z, |G12RectangleWF.outsidePrimorial N ε Z Q M T ⇑(MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm true (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z) (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) η Z t)| ≤ ↑(MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags true (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z) (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) η Z).card * (20 * ↑N) * (4 / MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η ^ η ^ 2) * (1 + Real.log ↑⌊Q⌋₊) ^ 2

    The literal third term in the accepted dyadic G12 decomposition is paid.

    Inspect dependencies

    G12OutsideBudget.rectangle_family_budget · compiled type and proof/definition references.