MathlibNt.SieveTheory.LiLiuGoldbachG12RectangleWF

source

@[reducible, inline]

abbrev G12RectangleWF.Atom :

Type

Equations

G12RectangleWF.Atom = ((ℕ × ℕ) × ℕ)

Instances For

Inspect dependencies

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

source

noncomputable def G12RectangleWF.multiplicity (N m : ℕ) :

ℕ

Equations

G12RectangleWF.multiplicity N m = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)) m

Instances For

Inspect dependencies

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

source

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

Finset Atom

Actual repeated labels, not a replacement of the normalized weight by one.

Equations

G12RectangleWF.labels N ε M T = Finset.image (fun (p : (_ : ℕ × ℕ) × ℕ) => (p.fst, p.snd)) ((G12LowRectangle.rectangle N ε M T).sigma fun (p : ℕ × ℕ) => Finset.range (G12RectangleWF.multiplicity N p.1))

Instances For

Inspect dependencies

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

source

def G12RectangleWF.output (N : ℕ) (a : Atom) :

ℕ

Equations

G12RectangleWF.output N a = N - a.1.2 * a.1.1

Instances For

Inspect dependencies

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

source

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

ℝ

Equations

G12RectangleWF.mass N ε M T = ∑ p ∈ G12LowRectangle.rectangle N ε M T, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1

Instances For

Inspect dependencies

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

source

theorem G12RectangleWF.labels_test (N : ℕ) (ε : ℝ) (M T : ℕ) (f : ℕ × ℕ → ℝ) :

∑ a ∈ labels N ε M T, f a.1 = 400 * ∑ p ∈ G12LowRectangle.rectangle N ε M T, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * f p

Every test retains precisely the original factor 400.

Inspect dependencies

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

source

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

↑(labels N ε M T).card = 400 * mass N ε M T

Inspect dependencies

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

source

noncomputable def G12RectangleWF.outputWeight (N : ℕ) (ε : ℝ) (M T n : ℕ) :

ℝ

Equations

G12RectangleWF.outputWeight N ε M T n = ∑ p ∈ G12LowRectangle.rectangle N ε M T with N - p.2 * p.1 = n, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1

Instances For

Inspect dependencies

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

source

noncomputable def G12RectangleWF.sieve (N : ℕ) (hEven : Even N) (ε Z : ℝ) (M T : ℕ) :

BoundingSieve

Only the finite weighted mother changes; B10's local density is inherited.

Equations

G12RectangleWF.sieve N hEven ε Z M T = { support := Finset.image (fun (p : ℕ × ℕ) => N - p.2 * p.1) (G12LowRectangle.rectangle N ε M T), prodPrimes := (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BoundingSieve N hEven 0 0 0 Z (G12RectangleWF.mass N ε M T)).prodPrimes, prodPrimes_squarefree := ⋯, weights := G12RectangleWF.outputWeight N ε M T, weights_nonneg := ⋯, totalMass := (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BoundingSieve N hEven 0 0 0 Z (G12RectangleWF.mass N ε M T)).totalMass, nu := (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BoundingSieve N hEven 0 0 0 Z (G12RectangleWF.mass N ε M T)).nu, nu_mult := ⋯, nu_pos_of_prime := ⋯, nu_lt_one_of_prime := ⋯ }

Instances For

Inspect dependencies

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

source

theorem G12RectangleWF.sieve_nu (N : ℕ) (hEven : Even N) (ε Z : ℝ) (M T : ℕ) :

(sieve N hEven ε Z M T).nu = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BoundingSieve N hEven 0 0 0 Z (mass N ε M T)).nu

Inspect dependencies

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

source

theorem G12RectangleWF.sieve_prodPrimes (N : ℕ) (hEven : Even N) (ε Z : ℝ) (M T : ℕ) :

(sieve N hEven ε Z M T).prodPrimes = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProdPrimes N Z

Inspect dependencies

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

source

noncomputable def G12RectangleWF.gate (N : ℕ) (S : Finset (ℕ × ℕ)) (Q : Finset ℕ) (c : ℕ → ℝ) :

ℝ

The gcd gate is explicit and signed, and is not paid in this module.

Equations

G12RectangleWF.gate N S Q c = ∑ d ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q ↑N, c d * ((∑ p ∈ S, if ¬(p.1 * p.2).Coprime d then MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 else 0) / ↑d.totient)

Instances For

Inspect dependencies

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

source

noncomputable def G12RectangleWF.common (N : ℕ) (S : Finset (ℕ × ℕ)) (Q : Finset ℕ) (c : ℕ → ℝ) :

ℝ

Equations

G12RectangleWF.common N S Q c = ∑ d ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q ↑N, c d * ((∑ p ∈ S, if ↑p.1 * ↑p.2 ≡ ↑N [ZMOD ↑d] then MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 else 0) - (∑ p ∈ S, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1) / ↑d.totient)

Instances For

Inspect dependencies

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

source

theorem G12RectangleWF.common_eq_discrepancy_sub_gate (N : ℕ) (S : Finset (ℕ × ℕ)) (Q : Finset ℕ) (c : ℕ → ℝ) :

common N S Q c = G12LowRectangle.discrepancy N S Q c - gate N S Q c

Exact C2 coprime-main decomposition, with no absolute values or masks.

Inspect dependencies

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