noncomputable def G12BandOutput.clipMass (N : ℕ) (ε : ℝ) (T V : ℕ → ℝ) : ℝ

Equations

• G12BandOutput.clipMass N ε T V = G12ClippedWindow.mass N (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N) (G12ClippedWindow.clampLower N ε T V) (G12ClippedWindow.clampUpper N ε V)

noncomputable def G12BandOutput.sourceMass (N : ℕ) (ε a : ℝ) : ℝ

Equations

• G12BandOutput.sourceMass N ε a = G12BandOutput.clipMass N ε (G12BandOutput.productLo N (ε / a)) (G12BandOutput.productLo N (a * ε)) + G12BandOutput.clipMass N ε (G12BandOutput.productLo N (1 / a)) (G12BandOutput.productLo N 1) + G12BandOutput.clipMass N ε (G12BandOutput.roughLo a) (G12BandOutput.top N)

theorem G12BandOutput.sourceMass_nonneg {N : ℕ} (hN : 2 ≤ N) (ε a : ℝ) : 0 ≤ sourceMass N ε a

theorem G12BandOutput.product_clip_mass_le {N : ℕ} (hN : 4 ≤ N) (ε l u : ℝ) : clipMass N ε (productLo N l) (productLo N u) ≤ G12FineGrid.bandMass N ε l u + 21 * ↑N / ↑N ^ (4 / 53)

theorem G12BandOutput.rough_clip_mass_le {N : ℕ} (hN : 4 ≤ N) (ε : ℝ) {a : ℝ} (ha : 0 < a) : clipMass N ε (roughLo a) (top N) ≤ G12RoughBoundary.nearWindowMass N ε a + 21 * ↑N / ↑N ^ (4 / 53)

theorem G12BandOutput.sourceMass_le {N : ℕ} (hN : 4 ≤ N) {ε a : ℝ} (ha : 1 < a) (he : 0 < ε) : 400 * sourceMass N ε a ≤ ((MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ThinSum N (fun (x : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11Label) => ε / a) fun (x : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11Label) => a * ε) + MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ThinSum N (fun (x : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11Label) => 1 / a) fun (x : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11Label) => 1) + G12RoughBoundary.nearMass N a + 25200 * ↑N / ↑N ^ (4 / 53)

Three bad-prime transports are paid once, independently of the grid cardinality.

theorem G12BandOutput.bad_transport_eventually (δ : ℝ) (hδ : 0 < δ) : ∃ (K : ℕ), ∀ N ≥ K, 25200 * Real.log ↑N / ↑N ^ (4 / 53) ≤ δ

theorem G12BandOutput.sourceMass_budget {a ε : ℝ} (ha : 1 < a) (ha2 : a ≤ 2) (he : 0 < ε) (he2 : ε ≤ 2 / 15) (δ : ℝ) (hδ : 0 < δ) : ∃ (K : ℕ), 4 ≤ K ∧ ∀ N ≥ K, Real.log ↑N / ↑N * (400 * sourceMass N ε a) ≤ G12RoughBoundary.fullConstant * (a - 1) + δ

The complete three-window source mass, including the ungated transport.