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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshBox = (Set.Ioc (4 / 53) (4 / 33) ×ˢ Set.Ioc (4 / 53) (4 / 33)) ×ˢ Set.Ioc (4 / 53) (4 / 33) ×ˢ Set.Ioc (4 / 53) (4 / 33)

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshAmbient = (Set.Icc (4 / 53) (4 / 33) ×ˢ Set.Icc (4 / 53) (4 / 33)) ×ˢ Set.Icc (4 / 53) (4 / 33) ×ˢ Set.Icc (4 / 53) (4 / 33)

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshSource = {x : (ℝ × ℝ) × ℝ × ℝ | x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshBox ∧ x.1.1 ≤ x.1.2 ∧ x.1.2 ≤ x.2.1 ∧ x.2.1 ≤ x.2.2}

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCell (n : ℕ) (j : (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1)) : Set ((ℝ × ℝ) × ℝ × ℝ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCell n j = (Set.Ioc (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshLo n j 0) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshHi n j 0) ×ˢ Set.Ioc (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshLo n j 1) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshHi n j 1)) ×ˢ Set.Ioc (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshLo n j 2) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshHi n j 2) ×ˢ Set.Ioc (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshLo n j 3) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshHi n j 3)

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshRegion n = ⋃ j ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCells n, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCell n j

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachG11MeshCell (n : ℕ) (j : (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1)) : MeasurableSet (goldbachG11MeshCell n j)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachG11MeshAmbient : MeasurableSet goldbachG11MeshAmbient

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.isCompact_goldbachG11MeshAmbient : IsCompact goldbachG11MeshAmbient

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachG11MeshSource : MeasurableSet goldbachG11MeshSource

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshBox_subset_ambient : goldbachG11MeshBox ⊆ goldbachG11MeshAmbient

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCell_subset_box (n : ℕ) (j : (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1)) : goldbachG11MeshCell n j ⊆ goldbachG11MeshBox

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCell_unique {n : ℕ} {j k : (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1)} {x : (ℝ × ℝ) × ℝ × ℝ} (hj : x ∈ goldbachG11MeshCell n j) (hk : x ∈ goldbachG11MeshCell n k) : j = k

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshBox_cover (n : ℕ) {x : (ℝ × ℝ) × ℝ × ℝ} (hx : x ∈ goldbachG11MeshBox) : ∃ (j : (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1)), x ∈ goldbachG11MeshCell n j

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshSource_cover (n : ℕ) {x : (ℝ × ℝ) × ℝ × ℝ} (hx : x ∈ goldbachG11MeshSource) : ∃ j ∈ goldbachG11MeshCells n, x ∈ goldbachG11MeshCell n j

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshCell_order_error {n : ℕ} {j : (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1)} (hj : j ∈ goldbachG11MeshCells n) {x : (ℝ × ℝ) × ℝ × ℝ} (hx : x ∈ goldbachG11MeshCell n j) : x.1.1 < x.1.2 + goldbachG11MeshStep n ∧ x.1.2 < x.2.1 + goldbachG11MeshStep n ∧ x.2.1 < x.2.2 + goldbachG11MeshStep n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Mesh_prime_cover (n N : ℕ) (hN : 4 ≤ N) (v : GoldbachG11Label) (hv : v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) : ∃ j ∈ goldbachG11MeshCells n, v ∈ goldbachG11PrimeBox N (goldbachG11MeshLo n j) (goldbachG11MeshHi n j)