MathlibNt.SieveTheory.LiLiuGoldbachB9LogGridRegion

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridCell · compiled type and proof/definition references.

source

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridRegion (n : ℕ) :

Set (ℝ × ℝ)

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridRegion n = ⋃ q ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridCells n, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridCell n q

Instances For

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridRegion · compiled type and proof/definition references.

source

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogSourceRegion :

Set (ℝ × ℝ)

This half-open continuous region does not change the finite closed carrier.

Equations

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

Instances For

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogSourceRegion · compiled type and proof/definition references.

source

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogAmbientBox :

Set (ℝ × ℝ)

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogAmbientBox = Set.Icc (1 / 20) (1 / 3) ×ˢ Set.Icc (1 / 4) (1 / 2)

Instances For

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogAmbientBox · compiled type and proof/definition references.

source

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LeftStrip (n : ℕ) :

Set (ℝ × ℝ)

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LeftStrip n = Set.Ioc (4 / 53 - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridStep n) (4 / 53) ×ˢ Set.Icc (1 / 4) (1 / 2)

Instances For

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LeftStrip · compiled type and proof/definition references.

source

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BottomStrip (n : ℕ) :

Set (ℝ × ℝ)

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BottomStrip n = Set.Icc (4 / 53) (1 / 3) ×ˢ Set.Ioc (1 / 3 - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridStep n) (1 / 3)

Instances For

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BottomStrip · compiled type and proof/definition references.

source

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9ObliqueStrip (n : ℕ) :

Set (ℝ × ℝ)

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9ObliqueStrip n = {x : ℝ × ℝ | x.1 ∈ Set.Icc (4 / 53) (1 / 3) ∧ (1 - x.1) / 2 < x.2 ∧ x.2 < (1 - x.1) / 2 + (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridStep n + 2 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridStep n) / 2}

Instances For

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9ObliqueStrip · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachB9LogGridCell (n : ℕ) (q : Fin n × Fin n) :

MeasurableSet (goldbachB9LogGridCell n q)

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachB9LogGridCell · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachB9LogGridRegion (n : ℕ) :

MeasurableSet (goldbachB9LogGridRegion n)

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachB9LogGridRegion · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachB9LogSourceRegion :

MeasurableSet goldbachB9LogSourceRegion

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachB9LogSourceRegion · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachB9LogAmbientBox :

MeasurableSet goldbachB9LogAmbientBox

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachB9LogAmbientBox · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.isCompact_goldbachB9LogAmbientBox :

IsCompact goldbachB9LogAmbientBox

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.isCompact_goldbachB9LogAmbientBox · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachB9LeftStrip (n : ℕ) :

MeasurableSet (goldbachB9LeftStrip n)

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachB9LeftStrip · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachB9BottomStrip (n : ℕ) :

MeasurableSet (goldbachB9BottomStrip n)

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachB9BottomStrip · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachB9ObliqueStrip (n : ℕ) :

MeasurableSet (goldbachB9ObliqueStrip n)

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachB9ObliqueStrip · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogSourceRegion_section (u : ℝ) :

Prod.mk u ⁻¹' goldbachB9LogSourceRegion = if u ∈ Set.Ioc (4 / 53) (1 / 3) then Set.Ioc (1 / 3) ((1 - u) / 2) else ∅

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogSourceRegion_section · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LeftStrip_section (n : ℕ) (u : ℝ) :

Prod.mk u ⁻¹' goldbachB9LeftStrip n = if u ∈ Set.Ioc (4 / 53 - goldbachB9AlphaGridStep n) (4 / 53) then Set.Icc (1 / 4) (1 / 2) else ∅

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LeftStrip_section · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BottomStrip_section (n : ℕ) (u : ℝ) :

Prod.mk u ⁻¹' goldbachB9BottomStrip n = if u ∈ Set.Icc (4 / 53) (1 / 3) then Set.Ioc (1 / 3 - goldbachB9BetaGridStep n) (1 / 3) else ∅

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BottomStrip_section · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9ObliqueStrip_section (n : ℕ) (u : ℝ) :

Prod.mk u ⁻¹' goldbachB9ObliqueStrip n = if u ∈ Set.Icc (4 / 53) (1 / 3) then Set.Ioo ((1 - u) / 2) ((1 - u) / 2 + (goldbachB9AlphaGridStep n + 2 * goldbachB9BetaGridStep n) / 2) else ∅

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9ObliqueStrip_section · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.volume_goldbachB9LeftStrip (n : ℕ) :

MeasureTheory.volume (goldbachB9LeftStrip n) = ENNReal.ofReal (17 / 240 / ↑n)

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.volume_goldbachB9LeftStrip · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.volume_goldbachB9BottomStrip (n : ℕ) :

MeasureTheory.volume (goldbachB9BottomStrip n) = ENNReal.ofReal (41 / 636 / ↑n)

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.volume_goldbachB9BottomStrip · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.volume_goldbachB9ObliqueStrip (n : ℕ) :

MeasureTheory.volume (goldbachB9ObliqueStrip n) = ENNReal.ofReal (1927 / 19080 / ↑n)

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.volume_goldbachB9ObliqueStrip · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridCell_pairwiseDisjoint {n : ℕ} (hn : 0 < n) :

Set.univ.Pairwise (Function.onFun Disjoint (goldbachB9LogGridCell n))

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridCell_pairwiseDisjoint · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridCell_subset_ambientBox {n : ℕ} (hn : 0 < n) (q : Fin n × Fin n) :

goldbachB9LogGridCell n q ⊆ goldbachB9LogAmbientBox

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridCell_subset_ambientBox · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridRegion_subset_ambientBox {n : ℕ} (hn : 0 < n) :

goldbachB9LogGridRegion n ⊆ goldbachB9LogAmbientBox

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridRegion_subset_ambientBox · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogSourceRegion_subset_ambientBox :

goldbachB9LogSourceRegion ⊆ goldbachB9LogAmbientBox

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogSourceRegion_subset_ambientBox · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogAmbientBox_gap {x : ℝ × ℝ} (hx : x ∈ goldbachB9LogAmbientBox) :

1 / 6 ≤ 1 - x.1 - x.2

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogAmbientBox_gap · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridRegion_excess_subset {n : ℕ} (hn : 0 < n) :

goldbachB9LogGridRegion n \ goldbachB9LogSourceRegion ⊆ goldbachB9LeftStrip n ∪ goldbachB9BottomStrip n ∪ goldbachB9ObliqueStrip n

The source has a horizontal lower edge, not the B8 diagonal edge.

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridRegion_excess_subset · compiled type and proof/definition references.