def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogGridCell (n : ℕ) (q : Fin n × Fin n) : Set (ℝ × ℝ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogGridCell n q = Set.Ioc (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8AlphaGridPoint n ↑q.1) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8AlphaGridPoint n (↑q.1 + 1)) ×ˢ Set.Ioc (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8BetaGridPoint n ↑q.2) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8BetaGridPoint n (↑q.2 + 1))

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogGridRegion n = ⋃ q ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogGridCells n, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogGridCell n q

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogSourceRegion : Set (ℝ × ℝ)

Half-open continuous source; this does not alter the finite closed carrier.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogSourceRegion = {x : ℝ × ℝ | x.1 ∈ Set.Ioc (3 / 11) (1 / 3) ∧ x.2 ∈ Set.Ioc x.1 ((1 - x.1) / 2)}

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogAmbientBox : Set (ℝ × ℝ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogAmbientBox = Set.Icc (1 / 4) (1 / 3) ×ˢ Set.Icc (1 / 4) (4 / 11)

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LeftStrip n = Set.Ioc (3 / 11 - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8AlphaGridStep n) (3 / 11) ×ˢ Set.Icc (1 / 4) (4 / 11)

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8ObliqueStrip n = {x : ℝ × ℝ | x.1 ∈ Set.Icc (3 / 11) (1 / 3) ∧ (1 - x.1) / 2 < x.2 ∧ x.2 < (1 - x.1) / 2 + (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8AlphaGridStep n + 2 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8BetaGridStep n) / 2}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachB8LogGridCell (n : ℕ) (q : Fin n × Fin n) : MeasurableSet (goldbachB8LogGridCell n q)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachB8LogGridRegion (n : ℕ) : MeasurableSet (goldbachB8LogGridRegion n)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachB8LogSourceRegion : MeasurableSet goldbachB8LogSourceRegion

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachB8LogAmbientBox : MeasurableSet goldbachB8LogAmbientBox

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.isCompact_goldbachB8LogAmbientBox : IsCompact goldbachB8LogAmbientBox

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachB8LeftStrip (n : ℕ) : MeasurableSet (goldbachB8LeftStrip n)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachB8ObliqueStrip (n : ℕ) : MeasurableSet (goldbachB8ObliqueStrip n)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogSourceRegion_section (u : ℝ) : Prod.mk u ⁻¹' goldbachB8LogSourceRegion = if u ∈ Set.Ioc (3 / 11) (1 / 3) then Set.Ioc u ((1 - u) / 2) else ∅

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LeftStrip_section (n : ℕ) (u : ℝ) : Prod.mk u ⁻¹' goldbachB8LeftStrip n = if u ∈ Set.Ioc (3 / 11 - goldbachB8AlphaGridStep n) (3 / 11) then Set.Icc (1 / 4) (4 / 11) else ∅

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8DiagonalStrip_section (n : ℕ) (u : ℝ) : Prod.mk u ⁻¹' goldbachB8DiagonalStrip n = if u ∈ Set.Icc (3 / 11) (1 / 3) then Set.Ioc (u - (goldbachB8AlphaGridStep n + goldbachB8BetaGridStep n)) u else ∅

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8ObliqueStrip_section (n : ℕ) (u : ℝ) : Prod.mk u ⁻¹' goldbachB8ObliqueStrip n = if u ∈ Set.Icc (3 / 11) (1 / 3) then Set.Ioo ((1 - u) / 2) ((1 - u) / 2 + (goldbachB8AlphaGridStep n + 2 * goldbachB8BetaGridStep n) / 2) else ∅

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.volume_goldbachB8LeftStrip (n : ℕ) : MeasureTheory.volume (goldbachB8LeftStrip n) = ENNReal.ofReal (5 / 528 / ↑n)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.volume_goldbachB8ObliqueStrip (n : ℕ) : MeasureTheory.volume (goldbachB8ObliqueStrip n) = ENNReal.ofReal (41 / 4356 / ↑n)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogGridCell_pairwiseDisjoint {n : ℕ} (hn : 0 < n) : Set.univ.Pairwise (Function.onFun Disjoint (goldbachB8LogGridCell n))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogGridCell_subset_ambientBox {n : ℕ} (hn : 0 < n) (q : Fin n × Fin n) : goldbachB8LogGridCell n q ⊆ goldbachB8LogAmbientBox

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogGridRegion_subset_ambientBox {n : ℕ} (hn : 0 < n) : goldbachB8LogGridRegion n ⊆ goldbachB8LogAmbientBox

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogSourceRegion_subset_ambientBox : goldbachB8LogSourceRegion ⊆ goldbachB8LogAmbientBox

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogAmbientBox_gap {x : ℝ × ℝ} (hx : x ∈ goldbachB8LogAmbientBox) : 10 / 33 ≤ 1 - x.1 - x.2

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogGridRegion_excess_subset {n : ℕ} (hn : 0 < n) : goldbachB8LogGridRegion n \ goldbachB8LogSourceRegion ⊆ goldbachB8LeftStrip n ∪ goldbachB8DiagonalStrip n ∪ goldbachB8ObliqueStrip n

All excess points, including equality on the diagonal, are paid by three strips.