MathlibNt.SieveTheory.LiLiuGoldbachG12FlexibleWFRemainder

source

noncomputable def G12FlexibleWF.residue (N : ℕ) (A : Finset (ℕ × ℕ)) (d : ℕ) :

ℝ

Equations

G12FlexibleWF.residue N A d = (∑ p ∈ A, if d ∣ N - p.2 * p.1 then MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 else 0) - G12FlexibleWF.mass N A / ↑d.totient

Instances For

Inspect dependencies

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

source

theorem G12FlexibleWF.output_dvd_iff (N d : ℕ) (p : ℕ × ℕ) (hp : p.2 * p.1 ≤ N) :

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

Natural subtraction is only converted on genuinely safe atoms.

Inspect dependencies

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

source

theorem G12FlexibleWF.residue_eq (N : ℕ) (A : Finset (ℕ × ℕ)) (d : ℕ) (hsafe : ∀ p ∈ A, p.2 * p.1 ≤ N) :

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

Inspect dependencies

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

source

theorem G12FlexibleWF.repeated_remainder (N : ℕ) (hEven : Even N) (A : Finset (ℕ × ℕ)) (Z : ℝ) {d : ℕ} (hd : d ∣ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProdPrimes N Z) :

MathlibNt.SieveTheory.LiLiuPrereqWF.sequenceRemainder (labels N A) (G12RectangleWF.output N) (400 * mass N A) AnalyticNumberTheory.Sieve.goldbachNu d = 400 * residue N A d

Inspect dependencies

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

source

noncomputable def G12FlexibleWF.outsidePrimorial (N : ℕ) (A : Finset (ℕ × ℕ)) (Z Q : ℝ) (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

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

Instances For

Inspect dependencies

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

source

theorem G12FlexibleWF.member_full_identity (N : ℕ) (A : Finset (ℕ × ℕ)) (Z Q : ℝ) (hsafe : ∀ p ∈ A, p.2 * p.1 ≤ N) (f : ArithmeticFunction ℝ) (hf : MathlibNt.SieveTheory.LiLiuPrereqWF.WellFactorable f Q) :

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

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

Inspect dependencies

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

source

theorem G12FlexibleWF.external_remainder_decomposition (N : ℕ) (hEven : Even N) (A : Finset (ℕ × ℕ)) (Z Q η : ℝ) (hsafe : ∀ p ∈ A, p.2 * p.1 ≤ N) (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

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