theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedOutputFiber_injOn (N p : ℕ) (ε : ℝ) : Set.InjOn (fun (x : GoldbachG11LinkedAtom) => x.snd) ↑({x ∈ goldbachG11LinkedAtoms N ε | goldbachG11LinkedOutput N x = p})

A fixed output determines m after the prime r has been retained.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedOutputFiber_card_le_twenty {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) (p : ℕ) : {x ∈ goldbachG11LinkedAtoms N ε | goldbachG11LinkedOutput N x = p}.card ≤ 20

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedOutputWeight_le_twenty {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) (p : ℕ) : goldbachG11LinkedOutputWeight N ε p ≤ 20

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedSmallOutputMass (N : ℕ) (ε Z : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedSmallOutputMass N ε Z = ∑ p ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedOutputSupport N ε with p < ⌈Z⌉₊, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedOutputWeight N ε p

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedSmallOutputMass_le {N : ℕ} (hN : 2 ≤ N) (ε Z : ℝ) : goldbachG11LinkedSmallOutputMass N ε Z ≤ 20 * ↑⌈Z⌉₊

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeOutput_le_sifted_add_small (N : ℕ) (ε Z : ℝ) : ∑ p ∈ goldbachG11LinkedOutputSupport N ε with Nat.Prime p, goldbachG11LinkedOutputWeight N ε p ≤ goldbachG11LinkedSiftedMass N ε Z + goldbachG11LinkedSmallOutputMass N ε Z

Prime outputs survive the sieve unless they lie below its cutoff.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodTotal_le_linkedSifted {N : ℕ} (hN : 2 ≤ N) (ε Z : ℝ) : ↑(goldbachG11GoodSwitchedTotal N ε (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ 400 * goldbachG11LinkedSiftedMass N ε Z + 8000 * ↑⌈Z⌉₊

Original good labelled count, with all multiplicity retained and the actual small-output loss bounded; this is not yet an analytic upper-sieve estimate.