noncomputable def G12BandOutput.clip (N : ℕ) (ε : ℝ) (T V : ℕ → ℝ) (m : ℕ) : Finset ℕ

One global clipped window, independent of the number of grid cells.

Equations

• G12BandOutput.clip N ε T V m = G12ClippedWindow.window N (G12ClippedWindow.clampLower N ε T V) (G12ClippedWindow.clampUpper N ε V) m

noncomputable def G12BandOutput.productLo (N : ℕ) (l : ℝ) (m : ℕ) : ℝ

Equations

• G12BandOutput.productLo N l m = l * ↑N / ↑m

noncomputable def G12BandOutput.roughLo (a : ℝ) (m : ℕ) : ℝ

Equations

• G12BandOutput.roughLo a m = ↑m.minFac / a

noncomputable def G12BandOutput.top (N : ℕ) : ℕ → ℝ

Equations

• G12BandOutput.top N = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiHi N

theorem G12BandOutput.mem_clip (N m r : ℕ) (ε : ℝ) (T V : ℕ → ℝ) : r ∈ clip N ε T V m ↔ r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow N ε m ∧ T m < ↑r ∧ ↑r ≤ V m

theorem G12BandOutput.product_clip_good_le (N : ℕ) (ε l u : ℝ) : goodMass N (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N) (G12ClippedWindow.clampLower N ε (productLo N l) (productLo N u)) (G12ClippedWindow.clampUpper N ε (productLo N u)) ≤ G12FineGrid.bandMass N ε l u

theorem G12BandOutput.rough_clip_good_le (N : ℕ) (ε : ℝ) {a : ℝ} (ha : 0 < a) : goodMass N (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N) (G12ClippedWindow.clampLower N ε (roughLo a) (top N)) (G12ClippedWindow.clampUpper N ε (top N)) ≤ G12RoughBoundary.nearWindowMass N ε a

noncomputable def G12BandOutput.pairs (N : ℕ) (ε : ℝ) (T V : ℕ → ℝ) : Finset (ℕ × ℕ)

Literal pair carrier; it does not identify distinct body representations.

Equations

• G12BandOutput.pairs N ε T V = {p ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N ×ˢ Finset.range (N + 1) | p.2 ∈ G12BandOutput.clip N ε T V p.1}

theorem G12BandOutput.mem_pairs (N : ℕ) (ε : ℝ) (T V : ℕ → ℝ) (p : ℕ × ℕ) : p ∈ pairs N ε T V ↔ p.1 ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N ∧ p.2 ∈ clip N ε T V p.1

noncomputable def G12BandOutput.atom (N : ℕ) (p : ℕ × ℕ) : ℝ

Equations

• G12BandOutput.atom N p = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * if Nat.Prime (N - p.2 * p.1) then 1 else 0

theorem G12BandOutput.atom_nonneg (N : ℕ) (p : ℕ × ℕ) : 0 ≤ atom N p

theorem G12BandOutput.pairs_output_eq (N : ℕ) (ε : ℝ) (T V : ℕ → ℝ) : 400 * ∑ p ∈ pairs N ε T V, atom N p = G12ClippedWindow.primeOutput N (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N) (G12ClippedWindow.clampLower N ε T V) (G12ClippedWindow.clampUpper N ε V)

noncomputable def G12BandOutput.cover (N : ℕ) (ε a : ℝ) : Finset (ℕ × ℕ)

The three global source pair sets, with a genuinely strict rough lower endpoint.

Equations

• G12BandOutput.cover N ε a = G12BandOutput.pairs N ε (G12BandOutput.productLo N (ε / a)) (G12BandOutput.productLo N (a * ε)) ∪ G12BandOutput.pairs N ε (G12BandOutput.productLo N (1 / a)) (G12BandOutput.productLo N 1) ∪ G12BandOutput.pairs N ε (G12BandOutput.roughLo a) (G12BandOutput.top N)

theorem G12BandOutput.band_mem_pairs {N : ℕ} {ε l u : ℝ} {p : ℕ × ℕ} (hm : p.1 ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N) (hr : p.2 ∈ G12FineGrid.bandWindow N ε l u p.1) : p ∈ pairs N ε (productLo N l) (productLo N u)

theorem G12BandOutput.rough_mem_pairs {ρ 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 ∈ pairs N ε (roughLo a) (top N)

Strict containment retains q=r; no endpoint atom is deleted.

theorem G12BandOutput.boundary_subset_cover {ρ a ε : ℝ} {N : ℕ} (hN : 1 ≤ N) (ha : 1 < a) (he : 0 < ε) (hmesh : ∀ k ∈ G12FineGrid.indices ρ N, ↑(G12FineGrid.shortUpper ρ N k) ≤ a * ↑(G12FineGrid.shortLower ρ N k)) : (G12FineGrid.indices ρ N).biUnion (G12FineGrid.boundaryCell ρ N ε) ⊆ cover N ε a