MathlibNt.SieveTheory.LiLiuGoldbachB9HighFirstLogRegion

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

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighLogGridRegion n = ⋃ q ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighLogGridCells n, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridCell n q

Instances For

Inspect dependencies

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

source

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighLogSourceRegion :

Set (ℝ × ℝ)

Equations

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

Instances For

Inspect dependencies

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

source

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

Set (ℝ × ℝ)

Equations

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

Instances For

Inspect dependencies

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

source

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

Set (ℝ × ℝ)

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighBottomStrip n = Set.Icc (1 / 10) (1 / 3) ×ˢ Set.Ioc (1 / 3 - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridStep n) (1 / 3)

Instances For

Inspect dependencies

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

source

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

Set (ℝ × ℝ)

Equations

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighObliqueStrip n = {x : ℝ × ℝ | x.1 ∈ Set.Icc (1 / 10) (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.goldbachB9HighObliqueStrip · compiled type and proof/definition references.

Inspect dependencies

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

source

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

MeasurableSet (goldbachB9HighLogGridRegion n)

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_goldbachB9HighLogSourceRegion :

MeasurableSet goldbachB9HighLogSourceRegion

Inspect dependencies

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

source

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

MeasurableSet (goldbachB9HighLeftStrip n)

Inspect dependencies

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

source

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

MeasurableSet (goldbachB9HighBottomStrip n)

Inspect dependencies

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

source

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

MeasurableSet (goldbachB9HighObliqueStrip n)

Inspect dependencies

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

source

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

goldbachB9HighLogGridRegion n ⊆ goldbachB9LogGridRegion n

Inspect dependencies

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

source

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

goldbachB9HighLogGridRegion n ⊆ goldbachB9LogAmbientBox

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighLogSourceRegion_subset_ambientBox :

goldbachB9HighLogSourceRegion ⊆ goldbachB9LogAmbientBox

Inspect dependencies

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

source

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

goldbachB9HighLogSourceRegion ⊆ goldbachB9HighLogGridRegion n

Inspect dependencies

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

source

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

goldbachB9HighLogGridRegion n \ goldbachB9HighLogSourceRegion ⊆ goldbachB9HighLeftStrip n ∪ goldbachB9HighBottomStrip n ∪ goldbachB9HighObliqueStrip n

Inspect dependencies

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

source

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

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

Inspect dependencies

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

source

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

MeasureTheory.volume (goldbachB9HighBottomStrip n) = ENNReal.ofReal ((1 / 3 - 1 / 10) * goldbachB9BetaGridStep n)

Inspect dependencies

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

source

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

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

Inspect dependencies

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

source

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

MeasureTheory.volume (goldbachB9HighObliqueStrip n) = ENNReal.ofReal ((1 / 3 - 1 / 10) * (goldbachB9AlphaGridStep n + 2 * goldbachB9BetaGridStep n) / 2)

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.integrable_goldbachB9HighSourceIndicator :

MeasureTheory.Integrable (goldbachB9HighLogSourceRegion.indicator LiuWeight.liuLogIntegrand) MeasureTheory.volume

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.integrable_goldbachB9HighLogGridUpperIntegrand (n : ℕ) (hn : 0 < n) :

MeasureTheory.Integrable (goldbachB9HighLogGridUpperIntegrand n) MeasureTheory.volume

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighLogGridUpperSum_eq_integral (n : ℕ) (hn : 0 < n) :

goldbachB9HighLogGridUpperSum n = ∫ (x : ℝ × ℝ), goldbachB9HighLogGridUpperIntegrand n x

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighLogGridUpperIntegrand_eq_of_mem {n : ℕ} (hn : 0 < n) {q : Fin n × Fin n} (hq : q ∈ goldbachB9HighLogGridCells n) {x : ℝ × ℝ} (hx : x ∈ goldbachB9LogGridCell n q) :

goldbachB9HighLogGridUpperIntegrand n x = 1 / (1 - goldbachB9AlphaGridPoint n (↑q.1 + 1) - goldbachB9BetaGridPoint n (↑q.2 + 1)) * LiuWeight.liuLogDensity x

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighLogGridUpperIntegrand_eq_zero {n : ℕ} {x : ℝ × ℝ} (hx : x ∉ goldbachB9HighLogGridRegion n) :

goldbachB9HighLogGridUpperIntegrand n x = 0

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighLogGridUpperIntegrand_eq_full_of_mem {n : ℕ} (hn : 0 < n) {x : ℝ × ℝ} (hx : x ∈ goldbachB9HighLogGridRegion n) :

goldbachB9HighLogGridUpperIntegrand n x = goldbachB9LogGridUpperIntegrand n x

Equality only on selected cells lets us reuse the produced corner estimates.

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighLogGridUpperIntegrand_le {n : ℕ} (hn : 0 < n) {x : ℝ × ℝ} (hx : x ∈ goldbachB9HighLogGridRegion n) :

goldbachB9HighLogGridUpperIntegrand n x ≤ 480

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighLogGridUpperIntegrand_le_integrand_add {n : ℕ} (hn : 0 < n) {x : ℝ × ℝ} (hx : x ∈ goldbachB9HighLogGridRegion n) :

goldbachB9HighLogGridUpperIntegrand n x ≤ LiuWeight.liuLogIntegrand x + 1600 / ↑n

Inspect dependencies

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