MathlibNt.SieveTheory.LiLiuGoldbachG12RectangleWFRemainder

source

noncomputable def G12RectangleWF.residue (N : ℕ) (ε : ℝ) (M T d : ℕ) :

ℝ

Equations

G12RectangleWF.residue N ε M T d = (∑ p ∈ G12LowRectangle.rectangle N ε M T, if d ∣ N - p.2 * p.1 then MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 else 0) - G12RectangleWF.mass N ε M T / ↑d.totient

Instances For

Inspect dependencies

G12RectangleWF.residue · compiled type and proof/definition references.

source

theorem G12RectangleWF.output_dvd_iff (N : ℕ) (ε : ℝ) (M T d : ℕ) (p : ℕ × ℕ) (hp : p ∈ G12LowRectangle.rectangle N ε M T) :

d ∣ N - p.2 * p.1 ↔ ↑p.1 * ↑p.2 ≡ ↑N [ZMOD ↑d]

Inspect dependencies

G12RectangleWF.output_dvd_iff · compiled type and proof/definition references.

source

theorem G12RectangleWF.residue_eq (N : ℕ) (ε : ℝ) (M T d : ℕ) :

residue N ε M T d = (∑ p ∈ G12LowRectangle.rectangle N ε M T, if ↑p.1 * ↑p.2 ≡ ↑N [ZMOD ↑d] then MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 else 0) - mass N ε M T / ↑d.totient

Inspect dependencies

G12RectangleWF.residue_eq · compiled type and proof/definition references.

source

theorem G12RectangleWF.repeated_remainder (N : ℕ) (hEven : Even N) (ε Z : ℝ) (M T : ℕ) {d : ℕ} (hd : d ∣ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProdPrimes N Z) :

MathlibNt.SieveTheory.LiLiuPrereqWF.sequenceRemainder (labels N ε M T) (output N) (400 * mass N ε M T) AnalyticNumberTheory.Sieve.goldbachNu d = 400 * residue N ε M T d

Inspect dependencies

G12RectangleWF.repeated_remainder · compiled type and proof/definition references.

source

noncomputable def G12RectangleWF.outsidePrimorial (N : ℕ) (ε Z Q : ℝ) (M T : ℕ) (c : ℕ → ℝ) :

ℝ

These are the genuine non-primorial terms introduced by a full-modulus transport. They cannot be erased merely because the primorial is squarefree.

Equations

G12RectangleWF.outsidePrimorial N ε Z Q M T c = ∑ d ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli (Finset.Ioc 0 ⌊Q⌋₊) ↑N with ¬d ∣ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProdPrimes N Z, c d * G12RectangleWF.residue N ε M T d

Instances For

Inspect dependencies

G12RectangleWF.outsidePrimorial · compiled type and proof/definition references.

source

theorem G12RectangleWF.member_full_identity (N : ℕ) (ε Z Q : ℝ) (M T : ℕ) (f : ArithmeticFunction ℝ) (hf : MathlibNt.SieveTheory.LiLiuPrereqWF.WellFactorable f Q) :

∑ d ∈ (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProdPrimes N Z).divisors, f d * residue N ε M T d = common N (G12LowRectangle.rectangle N ε M T) (Finset.Ioc 0 ⌊Q⌋₊) ⇑f - outsidePrimorial N ε Z Q M T ⇑f

The actual coefficient is used on the entire original real-level interval.

Inspect dependencies

G12RectangleWF.member_full_identity · compiled type and proof/definition references.

source

theorem G12RectangleWF.external_remainder_decomposition (N : ℕ) (hEven : Even N) (ε Z Q η : ℝ) (M T : ℕ) (hfamily : ∀ t ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags true (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z) (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) η Z, MathlibNt.SieveTheory.LiLiuPrereqWF.WellFactorable (MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm true (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z) (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) η Z t) Q) :

Exact decomposition of the real producer remainder: C2 discrepancy, gcd gate, and the unavoidable signed full-carrier transport correction. No family member is squarefree-masked and no tuplewise absolute value occurs.

Inspect dependencies

G12RectangleWF.external_remainder_decomposition · compiled type and proof/definition references.

source

theorem G12RectangleWF.member_signedWF (Q : ℝ) (f : ArithmeticFunction ℝ) (hf : MathlibNt.SieveTheory.LiLiuPrereqWF.WellFactorable f Q) :

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.SignedWellFactorable 1 Q fun (d : ℕ) => f d

The very same full function is admissible for C2, without a mask.

Inspect dependencies

G12RectangleWF.member_signedWF · compiled type and proof/definition references.