def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachAffineDiagonalStrip (a b h : ℝ) : Set (ℝ × ℝ)

A closed horizontal window and a half-open strip below its diagonal.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachAffineDiagonalStrip a b h = {p : ℝ × ℝ | p.1 ∈ Set.Icc a b ∧ p.2 ∈ Set.Ioc (p.1 - h) p.1}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachAffineDiagonalStrip (a b h : ℝ) : MeasurableSet (goldbachAffineDiagonalStrip a b h)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachAffineDiagonalStrip_section (a b h u : ℝ) : Prod.mk u ⁻¹' goldbachAffineDiagonalStrip a b h = if u ∈ Set.Icc a b then Set.Ioc (u - h) u else ∅

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.volume_goldbachAffineDiagonalStrip (a b h : ℝ) (hh : 0 ≤ h) : MeasureTheory.volume (goldbachAffineDiagonalStrip a b h) = ENNReal.ofReal (h * (b - a))

Exact volume from vertical sections, not a bound on finite prime points.

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8DiagonalStrip (n : ℕ) : Set (ℝ × ℝ)

The diagonal excess strip for the B8 ambient mesh widths 1/12 and 5/44. This definition does not assert the still separate grid-excess classification.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8DiagonalStrip n = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachAffineDiagonalStrip (3 / 11) (1 / 3) (1 / 12 / ↑n + 5 / 44 / ↑n)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachB8DiagonalStrip (n : ℕ) : MeasurableSet (goldbachB8DiagonalStrip n)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.volume_goldbachB8DiagonalStrip (n : ℕ) : MeasureTheory.volume (goldbachB8DiagonalStrip n) = ENNReal.ofReal (13 / 1089 / ↑n)