noncomputable def G12ClippedWindow.atoms (N : ℕ) (L U : ℕ → ℝ) : Finset MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG12LinkedAtom

Equations

• G12ClippedWindow.atoms N L U = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N).sigma (G12ClippedWindow.window N L U)

noncomputable def G12ClippedWindow.outputSupport (N : ℕ) (L U : ℕ → ℝ) : Finset ℕ

Equations

• G12ClippedWindow.outputSupport N L U = Finset.image (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedOutput N) (G12ClippedWindow.atoms N L U)

noncomputable def G12ClippedWindow.outputWeight (N : ℕ) (g L U : ℕ → ℝ) (p : ℕ) : ℝ

All representations of one output retain their actual long weights.

Equations

• G12ClippedWindow.outputWeight N g L U p = ∑ x ∈ G12ClippedWindow.atoms N L U with MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedOutput N x = p, g x.fst

theorem G12ClippedWindow.atoms_subset {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} (h : Admissible N ε g L U) : atoms N L U ⊆ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε

theorem G12ClippedWindow.outputWeight_nonneg {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} (h : Admissible N ε g L U) (p : ℕ) : 0 ≤ outputWeight N g L U p

theorem G12ClippedWindow.outputWeight_le_old {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} (h : Admissible N ε g L U) (p : ℕ) : outputWeight N g L U p ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedOutputWeight N ε p

Pointwise domination of whole fibres; no output injection is asserted.

theorem G12ClippedWindow.outputWeight_le_twenty {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} (hN : 2 ≤ N) (h : Admissible N ε g L U) (p : ℕ) : outputWeight N g L U p ≤ 20

theorem G12ClippedWindow.output_pos {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} (h : Admissible N ε g L U) {x : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG12LinkedAtom} (hx : x ∈ atoms N L U) : 0 < MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedOutput N x

theorem G12ClippedWindow.zero_not_mem_outputSupport {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} (h : Admissible N ε g L U) : 0 ∉ outputSupport N L U

theorem G12ClippedWindow.output_sum (N : ℕ) (g L U : ℕ → ℝ) (P : ℕ → Prop) [DecidablePred P] : ∑ p ∈ outputSupport N L U with P p, outputWeight N g L U p = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, g m * ↑{r ∈ window N L U m | P (N - r * m)}.card

Exact pushforward for arbitrary output predicates, including divisibility.

noncomputable def G12ClippedWindow.primeOutput (N : ℕ) (g L U : ℕ → ℝ) : ℝ

Ungated prime outputs, not the coprime-r subcount.

Equations

• G12ClippedWindow.primeOutput N g L U = 400 * ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, g m * ↑{r ∈ G12ClippedWindow.window N L U m | Nat.Prime (N - r * m)}.card

noncomputable def G12ClippedWindow.siftedMass (N : ℕ) (g L U : ℕ → ℝ) (Z : ℝ) : ℝ

Equations

• G12ClippedWindow.siftedMass N g L U Z = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, g m * ↑{r ∈ G12ClippedWindow.window N L U m | (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProdPrimes N Z).Coprime (N - r * m)}.card

noncomputable def G12ClippedWindow.outputSieve (N : ℕ) (hEven : Even N) (g L U : ℕ → ℝ) (ε : ℝ) (h : Admissible N ε g L U) (Z X : ℝ) : BoundingSieve

Only support and weights change; the ordinary prime product and nu do not.

Equations

• G12ClippedWindow.outputSieve N hEven g L U ε h Z X = { support := G12ClippedWindow.outputSupport N L U, prodPrimes := (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BoundingSieve N hEven 0 0 0 Z X).prodPrimes, prodPrimes_squarefree := ⋯, weights := G12ClippedWindow.outputWeight N g L U, weights_nonneg := ⋯, totalMass := (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BoundingSieve N hEven 0 0 0 Z X).totalMass, nu := (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10BoundingSieve N hEven 0 0 0 Z X).nu, nu_mult := ⋯, nu_pos_of_prime := ⋯, nu_lt_one_of_prime := ⋯ }

theorem G12ClippedWindow.outputSieve_multSum {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} (hEven : Even N) (h : Admissible N ε g L U) (Z X : ℝ) (d : ℕ) : BoundingSieve.multSum d = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, g m * ↑{r ∈ window N L U m | d ∣ N - r * m}.card

theorem G12ClippedWindow.outputSieve_siftedSum {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} (hEven : Even N) (h : Admissible N ε g L U) (Z X : ℝ) : BoundingSieve.siftedSum = siftedMass N g L U Z

theorem G12ClippedWindow.outputSieve_rem {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} (hEven : Even N) (h : Admissible N ε g L U) (Z : ℝ) {d : ℕ} (hd : d ∣ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ProdPrimes N Z) : BoundingSieve.rem d = commonResidual N g L U d

theorem G12ClippedWindow.primeOutput_le_sifted {N : ℕ} {ε : ℝ} {g L U : ℕ → ℝ} (hN : 2 ≤ N) (h : Admissible N ε g L U) (Z : ℝ) : primeOutput N g L U ≤ 400 * siftedMass N g L U Z + 8000 * ↑⌈Z⌉₊

The actual small-output payment applies to every clipped fibre.