noncomputable def G12RoughBoundary.nearWindow (N : ℕ) (ε a : ℝ) (m : ℕ) : Finset ℕ

Equations

• G12RoughBoundary.nearWindow N ε a m = {r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow N ε m | ¬r ∣ N ∧ ↑m.minFac ≤ a * ↑r}

noncomputable def G12RoughBoundary.nearWindowMass (N : ℕ) (ε a : ℝ) : ℝ

Equations

• G12RoughBoundary.nearWindowMass N ε a = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N m * ↑(G12RoughBoundary.nearWindow N ε a m).card

theorem G12RoughBoundary.nearWindowMass_le_nearMass {N : ℕ} (ε a : ℝ) : 400 * nearWindowMass N ε a ≤ nearMass N a

All body multiplicities, not merely one minFac witness, are injected.

theorem G12RoughBoundary.pairMass_le_nearWindowMass (N : ℕ) (ε a : ℝ) (S : Finset (ℕ × ℕ)) (hS : ∀ p ∈ S, p.1 ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N ∧ p.2 ∈ nearWindow N ε a p.1) : ∑ p ∈ S, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 ≤ nearWindowMass N ε a

theorem G12RoughBoundary.roughBoundary_in_nearWindow {ρ a ε : ℝ} {N : ℕ} (hN : 1 ≤ N) (ha : 0 < a) (hmesh : ∀ k ∈ G12FineGrid.indices ρ N, ↑(G12FineGrid.shortUpper ρ N k) ≤ a * ↑(G12FineGrid.shortLower ρ N k)) {p : ℕ × ℕ} (hp : p ∈ G12FineGrid.roughBoundary ρ N ε) : p.1 ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N ∧ p.2 ∈ nearWindow N ε a p.1

The literal failed-roughness branch uses the real body minFac.

theorem G12RoughBoundary.roughBoundary_mass_le_nearMass {ρ a ε : ℝ} {N : ℕ} (hN : 1 ≤ N) (ha : 0 < a) (hmesh : ∀ k ∈ G12FineGrid.indices ρ N, ↑(G12FineGrid.shortUpper ρ N k) ≤ a * ↑(G12FineGrid.shortLower ρ N k)) : 400 * ∑ p ∈ G12FineGrid.roughBoundary ρ N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 ≤ nearMass N a

The source-level physical rough-boundary mass, with all factor 400 restored.