noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectangleWeight (N : ℕ) (v : ℕ × ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectangleWeight N v = ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) v.1) * if v.2.Coprime N then MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta v.2 else 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectangleWeight_nonneg (N : ℕ) (v : ℕ × ℕ) : 0 ≤ goldbachG11RectangleWeight N v

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectangleMotherCount (N : ℕ) (ε : ℝ) (U V : Finset ℕ) : ℝ

The original first-prime fibre, merely restricted to a rectangle.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectangleMotherCount N ε U V = ∑ m ∈ U, ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m) * ↑{p ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m | p ∈ V}.card

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectanglePrimeMass (N : ℕ) (U V : Finset ℕ) : ℝ

Positive rectangular enlargement, retaining all coefficient multiplicities.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectanglePrimeMass N U V = ∑ v ∈ U ×ˢ V, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectangleWeight N v * if Nat.Prime (↑N - ↑v.1 * ↑v.2).natAbs then 1 else 0

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectangleSiftedMass (N : ℕ) (U V P : Finset ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectangleSiftedMass N U V P = MathlibNt.SieveTheory.LiLiuPrereqWF.weightedSequenceSifted (U ×ˢ V) (fun (v : ℕ × ℕ) => (↑N - ↑v.1 * ↑v.2).natAbs) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectangleWeight N) P

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectangleSmallMass (N : ℕ) (U V : Finset ℕ) (z : ℝ) : ℝ

Includes zero and all outputs below the real cutoff; no injectivity is presumed.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectangleSmallMass N U V z = ∑ v ∈ U ×ˢ V, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectangleWeight N v * if ↑(↑N - ↑v.1 * ↑v.2).natAbs < z then 1 else 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectangleMotherCount_le_primeMass (N : ℕ) (ε : ℝ) (U V : Finset ℕ) : goldbachG11RectangleMotherCount N ε U V ≤ goldbachG11RectanglePrimeMass N U V

Actual prime-output fibres embed into the overhanging rectangle by positivity.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectanglePrimeMass_le_sifted_add_small (N : ℕ) (U V : Finset ℕ) (z : ℝ) : goldbachG11RectanglePrimeMass N U V ≤ goldbachG11RectangleSiftedMass N U V (fouvryG9SievePrimes N z) + goldbachG11RectangleSmallMass N U V z

Prime outputs below the actual cutoff remain explicitly charged.