MathlibNt.SieveTheory.LiLiuFouvryG9WeightedBoundaryKernel

source

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

0 ≤ 1 / ((1 - x.1 - x.2) * (1 - x.1)) ∧ 1 / ((1 - x.1 - x.2) * (1 - x.1)) ≤ 9

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9WeightedIntegrand_eq (x : ℝ × ℝ) :

fouvryG9WeightedIntegrand x = 1 / ((1 - x.1 - x.2) * (1 - x.1)) * LiuWeight.liuLogDensity x

Inspect dependencies

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

source

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

0 ≤ fouvryG9WeightedIntegrand x ∧ fouvryG9WeightedIntegrand x ≤ 720

Inspect dependencies

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

source

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

fouvryG9RelaxedIntegralCorner n 0 q = 9 / 5 * (1 / ((1 - goldbachB9AlphaGridPoint n (↑q.1 + 1) - goldbachB9BetaGridPoint n (↑q.2 + 1)) * (1 - goldbachB9AlphaGridPoint n (↑q.1 + 1))))

Inspect dependencies

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

source

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

fouvryG9WeightedUpperIntegrand n h x = fouvryG9RelaxedIntegralCorner n 0 q * LiuWeight.liuLogDensity x

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9WeightedUpperIntegrand_eq_zero {n : ℕ} {h : ℝ} {x : ℝ × ℝ} (hx : x ∉ fouvryG9WeightedRegion n h) :

fouvryG9WeightedUpperIntegrand n h x = 0

Inspect dependencies

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

source

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

fouvryG9WeightedUpperIntegrand n h x ≤ 1500

Inspect dependencies

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

source

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

fouvryG9WeightedUpperIntegrand n h x ≤ 9 / 5 * fouvryG9WeightedIntegrand x + 20000 / ↑n

Inspect dependencies

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