noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11CollarBoxes (N : ℕ) (ρ : ℝ) : Finset GoldbachG11SwitchedBody

Unordered q,s,t are deliberately an upper carrier. Its fourth coordinate is the short integer p in q<p<=rho*q, not a rough cofactor.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11CollarBoxes N ρ = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachClosedPrimes N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))).sigma fun (_t : ℕ) => (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachClosedPrimes N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))).sigma fun (_s : ℕ) => (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachClosedPrimes N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))).sigma fun (q : ℕ) => Finset.Ioc q ⌊ρ * ↑q⌋₊

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11CollarRoughMass (N : ℕ) (ρ : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11CollarRoughMass N ρ = ∑ v ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11CollarBoxes N ρ, ↑(LiLiuPrereqBuchstab.roughCount (ρ ^ 2 * ↑N / ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11SwitchedBodyProd v)) ↑v.snd.snd.fst)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Expanded_collar_pair_mem {N p : ℕ} {ρ : ℝ} {u : GoldbachG11SwitchedBody} (hu : u ∈ goldbachG11GoodSwitchedBodies N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) (hp : p ∈ goldbachG11ExpandedPrimeWindow N ρ (goldbachG11SwitchedBodyProd u)) (hqp : (goldbachG11SwitchedBodyProd u).minFac < p) : ⟨u.fst, ⟨u.snd.fst, ⟨u.snd.snd.fst, p⟩⟩⟩ ∈ goldbachG11CollarBoxes N ρ ∧ u.snd.snd.snd ∈ LiLiuPrereqBuchstab.roughNumbers (ρ ^ 2 * ↑N / ↑(goldbachG11SwitchedBodyProd ⟨u.fst, ⟨u.snd.fst, ⟨u.snd.snd.fst, p⟩⟩⟩)) ↑u.snd.snd.fst

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Expanded_collar_le_rough (N : ℕ) (ρ : ℝ) (h : ℝ → ℝ) (H : ℝ) (hH : 0 ≤ H) (hh : ∀ (r : ℝ), h r ≤ H) : (goldbachG11ExpandedMotherSlice N ρ h fun (m p : ℕ) => m.minFac < p) ≤ H * goldbachG11CollarRoughMass N ρ

Primality and ordering are dropped only on this positive collar upper carrier. The source body and its rough cofactor still map injectively.