noncomputable def G12FlexibleWF.labels (N : ℕ) (A : Finset (ℕ × ℕ)) : Finset G12RectangleWF.Atom

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

Equations

• G12FlexibleWF.labels N A = Finset.image (fun (p : (_ : ℕ × ℕ) × ℕ) => (p.fst, p.snd)) (A.sigma fun (p : ℕ × ℕ) => Finset.range (G12RectangleWF.multiplicity N p.1))

noncomputable def G12FlexibleWF.mass (N : ℕ) (A : Finset (ℕ × ℕ)) : ℝ

Equations

• G12FlexibleWF.mass N A = ∑ p ∈ A, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1

theorem G12FlexibleWF.labels_test (N : ℕ) (A : Finset (ℕ × ℕ)) (f : ℕ × ℕ → ℝ) : ∑ a ∈ labels N A, f a.1 = 400 * ∑ p ∈ A, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * f p

Every test retains precisely the original factor 400.

theorem G12FlexibleWF.labels_card (N : ℕ) (A : Finset (ℕ × ℕ)) : ↑(labels N A).card = 400 * mass N A

noncomputable def G12FlexibleWF.smallOutput (N : ℕ) (A : Finset (ℕ × ℕ)) (Z : ℝ) : ℝ

Equations

• G12FlexibleWF.smallOutput N A Z = ∑ a ∈ G12FlexibleWF.labels N A, if G12RectangleWF.output N a < ⌈Z⌉₊ then 1 else 0

noncomputable def G12FlexibleWF.primeCount (N : ℕ) (A : Finset (ℕ × ℕ)) : ℝ

Equations

• G12FlexibleWF.primeCount N A = ∑ a ∈ G12FlexibleWF.labels N A, if Nat.Prime (G12RectangleWF.output N a) then 1 else 0

theorem G12FlexibleWF.primeCount_eq_original (N : ℕ) (A : Finset (ℕ × ℕ)) : primeCount N A = 400 * ∑ p ∈ A, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * if Nat.Prime (N - p.2 * p.1) then 1 else 0

theorem G12FlexibleWF.prime_le_sifted_small (N : ℕ) (A : Finset (ℕ × ℕ)) (Z : ℝ) : primeCount N A ≤ MathlibNt.SieveTheory.LiLiuPrereqWF.sequenceSifted (labels N A) (G12RectangleWF.output N) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z) + smallOutput N A Z

theorem G12FlexibleWF.exists_atom_sieve : ∃ (K : ℝ) (C : ℝ), 1 < K ∧ 0 < C ∧ ∀ (η : ℝ), 0 < η → η < 1 / 8 → ∃ (Q₀ : ℝ), 4 ≤ Q₀ ∧ ∀ (Q : ℝ), Q₀ ≤ Q → ∀ (N : ℕ), Even N → ∀ (A : Finset (ℕ × ℕ)) (Z : ℝ), 2 ≤ Z → Z ≤ √Q → have P := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z; have D := MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η; have V := ∏ p ∈ P, (1 - AnalyticNumberTheory.Sieve.goldbachNu p); have E := C * (η + (η ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log Q ^ (-(1 / 3))); (∀ t ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags true P D η Z, MathlibNt.SieveTheory.LiLiuPrereqWF.WellFactorable (MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm true P D η Z t) Q) ∧ primeCount N A ≤ 400 * mass N A * V * (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965F (Real.log Q / Real.log Z) + E) + MathlibNt.SieveTheory.LiLiuPrereqWF.externalRemainder true P D η Z (labels N A) (G12RectangleWF.output N) (400 * mass N A) AnalyticNumberTheory.Sieve.goldbachNu + smallOutput N A Z

The genuine producer is called on the actual repeated labels on any finite atom set. The remainder is the signed sum of exactly the displayed family members.