noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8MainIntegral : ℝ

The actual two-dimensional B8 main integral, without the sieve factor eight.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8MainIntegral = ∫ (u : ℝ) in 3 / 11..1 / 3, ∫ (v : ℝ) in u..(1 - u) / 2, 1 / (u * v * (1 - u - v))

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogGridUpperIntegrand (n : ℕ) (x : ℝ × ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogGridUpperIntegrand n x = ∑ q ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogGridCells n, 1 / (1 - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8AlphaGridPoint n (↑q.1 + 1) - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8BetaGridPoint n (↑q.2 + 1)) * (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogGridCell n q).indicator MathlibNt.SieveTheory.LiuWeight.liuLogDensity x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogIntegrand_eq (u v : ℝ) : LiuWeight.liuLogIntegrand (u, v) = 1 / (u * v * (1 - u - v))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogDensity_bounds {x : ℝ × ℝ} (hx : x ∈ goldbachB8LogAmbientBox) : 0 ≤ LiuWeight.liuLogDensity x ∧ LiuWeight.liuLogDensity x ≤ 16

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogKernel_bounds {x : ℝ × ℝ} (hx : x ∈ goldbachB8LogAmbientBox) : 0 ≤ LiuWeight.liuLogKernel x ∧ LiuWeight.liuLogKernel x ≤ 4

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogIntegrand_bounds {x : ℝ × ℝ} (hx : x ∈ goldbachB8LogAmbientBox) : 0 ≤ LiuWeight.liuLogIntegrand x ∧ LiuWeight.liuLogIntegrand x ≤ 64

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.integrableOn_goldbachB8LogIntegrand {s : Set (ℝ × ℝ)} (hs : MeasurableSet s) (hsub : s ⊆ goldbachB8LogAmbientBox) : MeasureTheory.IntegrableOn LiuWeight.liuLogIntegrand s MeasureTheory.volume

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.integrable_goldbachB8SourceIndicator : MeasureTheory.Integrable (goldbachB8LogSourceRegion.indicator LiuWeight.liuLogIntegrand) MeasureTheory.volume

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8MainIntegral_eq_setIntegral : goldbachB8MainIntegral = ∫ (x : ℝ × ℝ) in goldbachB8LogSourceRegion, LiuWeight.liuLogIntegrand x

Fubini identifies the continuous half-open triangle with the stated double integral.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8MainIntegral_nonneg : 0 ≤ goldbachB8MainIntegral

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.integrable_goldbachB8LogGridUpperIntegrand (n : ℕ) (hn : 0 < n) : MeasureTheory.Integrable (goldbachB8LogGridUpperIntegrand n) MeasureTheory.volume

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogGridUpperSum_eq_integral (n : ℕ) (hn : 0 < n) : goldbachB8LogGridUpperSum n = ∫ (x : ℝ × ℝ), goldbachB8LogGridUpperIntegrand n x

This is the production upper sum, with its original selected cells unchanged.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogGrid_kernel_variation {n : ℕ} (hn : 0 < n) (q : Fin n × Fin n) {x : ℝ × ℝ} (hx : x ∈ goldbachB8LogGridCell n q) : 0 ≤ 1 / (1 - goldbachB8AlphaGridPoint n (↑q.1 + 1) - goldbachB8BetaGridPoint n (↑q.2 + 1)) - LiuWeight.liuLogKernel x ∧ 1 / (1 - goldbachB8AlphaGridPoint n (↑q.1 + 1) - goldbachB8BetaGridPoint n (↑q.2 + 1)) - LiuWeight.liuLogKernel x ≤ 4 / ↑n

The reciprocal gap changes by at most 4/n on every ambient cell.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogGridErrorConstant_pos : 0 < 1000

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8LogGridUpperSum_sub_mainIntegral_le (n : ℕ) (hn : 0 < n) : goldbachB8LogGridUpperSum n - goldbachB8MainIntegral ≤ 1000 / ↑n

One-sided structural error for every positive mesh size, not an assumed limit.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.exists_goldbachB8LogGridUpperSum_le_mainIntegral_add (δ : ℝ) (hδ : 0 < δ) : ∃ (n : ℕ), 0 < n ∧ goldbachB8LogGridUpperSum n ≤ goldbachB8MainIntegral + δ

Choose the mesh after the tolerance; no prime-size threshold is selected here.