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

Nonnegative high-band envelope: only the short-prime copN filter is dropped. The original long labelled coefficient is unchanged.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AllPrimeWeight N v = ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) v.1) * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta v.2

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

Equations

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

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

Equations

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

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

Equations

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AllPrimeWeight_nonneg (N : ℕ) (v : ℕ × ℕ) : 0 ≤ goldbachG11AllPrimeWeight N v

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectangleWeight_le_allPrime (N : ℕ) (v : ℕ × ℕ) : goldbachG11RectangleWeight N v ≤ goldbachG11AllPrimeWeight N v

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectanglePrimeMass_le_allPrime (N : ℕ) (U V : Finset ℕ) : goldbachG11RectanglePrimeMass N U V ≤ goldbachG11AllPrimeMass N U V

The high envelope is explicitly an upper bound on the unchanged actual count.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AllPrimeMass_le_sifted_add_small (N : ℕ) (U V : Finset ℕ) (z : ℝ) : goldbachG11AllPrimeMass N U V ≤ goldbachG11AllPrimeSiftedMass N U V (fouvryG9SievePrimes N z) + goldbachG11AllPrimeSmallMass N U V z

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectangleSiftedMass_le_allPrime (N : ℕ) (U V P : Finset ℕ) : goldbachG11RectangleSiftedMass N U V P ≤ goldbachG11AllPrimeSiftedMass N U V P

Drop the short copN filter only in the sifted term, not in the small-output budget.

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

The already paid original small-output term suffices for the high envelope.