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

The actual C10 integral for B9, without the sieve factor eight.

Equations

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

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridUpperIntegrand n x = ∑ q ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridCells n, 1 / (1 - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9AlphaGridPoint n (↑q.1 + 1) - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9BetaGridPoint n (↑q.2 + 1)) * (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridCell n q).indicator MathlibNt.SieveTheory.LiuWeight.liuLogDensity x

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogDensity_bounds {x : ℝ × ℝ} (hx : x ∈ goldbachB9LogAmbientBox) : 0 ≤ LiuWeight.liuLogDensity x ∧ LiuWeight.liuLogDensity x ≤ 80

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogKernel_bounds {x : ℝ × ℝ} (hx : x ∈ goldbachB9LogAmbientBox) : 0 ≤ LiuWeight.liuLogKernel x ∧ LiuWeight.liuLogKernel x ≤ 6

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogIntegrand_bounds {x : ℝ × ℝ} (hx : x ∈ goldbachB9LogAmbientBox) : 0 ≤ LiuWeight.liuLogIntegrand x ∧ LiuWeight.liuLogIntegrand x ≤ 480

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.continuousOn_goldbachB9LogDensity : ContinuousOn LiuWeight.liuLogDensity goldbachB9LogAmbientBox

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.continuousOn_goldbachB9LogKernel : ContinuousOn LiuWeight.liuLogKernel goldbachB9LogAmbientBox

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.continuousOn_goldbachB9LogIntegrand : ContinuousOn LiuWeight.liuLogIntegrand goldbachB9LogAmbientBox

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.continuousOn_goldbachB9MainInner {u : ℝ} (hu : u ∈ Set.Icc (4 / 53) (1 / 3)) : ContinuousOn (fun (v : ℝ) => 1 / (u * v * (1 - u - v))) (Set.Icc (1 / 3) ((1 - u) / 2))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.intervalIntegrable_goldbachB9MainInner {u : ℝ} (hu : u ∈ Set.Icc (4 / 53) (1 / 3)) : IntervalIntegrable (fun (v : ℝ) => 1 / (u * v * (1 - u - v))) MeasureTheory.volume (1 / 3) ((1 - u) / 2)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.integrableOn_goldbachB9LogDensity {s : Set (ℝ × ℝ)} (hs : MeasurableSet s) (hsub : s ⊆ goldbachB9LogAmbientBox) : MeasureTheory.IntegrableOn LiuWeight.liuLogDensity s MeasureTheory.volume

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.integrable_goldbachB9SourceIndicator : MeasureTheory.Integrable (goldbachB9LogSourceRegion.indicator LiuWeight.liuLogIntegrand) MeasureTheory.volume

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9MainIntegral_eq_iteratedSetIntegral : goldbachB9MainIntegral = ∫ (u : ℝ) in Set.Ioc (4 / 53) (1 / 3), ∫ (v : ℝ) in Set.Ioc (1 / 3) ((1 - u) / 2), LiuWeight.liuLogIntegrand (u, v)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9SourceIndicator_integral_section (u : ℝ) : ∫ (v : ℝ), goldbachB9LogSourceRegion.indicator LiuWeight.liuLogIntegrand (u, v) = (Set.Ioc (4 / 53) (1 / 3)).indicator (fun (u : ℝ) => ∫ (v : ℝ) in Set.Ioc (1 / 3) ((1 - u) / 2), LiuWeight.liuLogIntegrand (u, v)) u

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.intervalIntegrable_goldbachB9MainOuter : IntervalIntegrable (fun (u : ℝ) => ∫ (v : ℝ) in 1 / 3..(1 - u) / 2, 1 / (u * v * (1 - u - v))) MeasureTheory.volume (4 / 53) (1 / 3)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9MainIntegral_eq_setIntegral : goldbachB9MainIntegral = ∫ (x : ℝ × ℝ) in goldbachB9LogSourceRegion, LiuWeight.liuLogIntegrand x

Fubini is applied to an integrable indicator, not to an unspecified integral.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9MainIntegral_nonneg : 0 ≤ goldbachB9MainIntegral

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridUpperSum_eq_integral (n : ℕ) (hn : 0 < n) : goldbachB9LogGridUpperSum n = ∫ (x : ℝ × ℝ), goldbachB9LogGridUpperIntegrand n x

The selected-cell sum retains its actual logarithmic rectangle masses.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridUpperIntegrand_eq_of_mem {n : ℕ} (hn : 0 < n) {q : Fin n × Fin n} (hq : q ∈ goldbachB9LogGridCells n) {x : ℝ × ℝ} (hx : x ∈ goldbachB9LogGridCell n q) : goldbachB9LogGridUpperIntegrand n x = 1 / (1 - goldbachB9AlphaGridPoint n (↑q.1 + 1) - goldbachB9BetaGridPoint n (↑q.2 + 1)) * LiuWeight.liuLogDensity x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridUpperIntegrand_eq_zero {n : ℕ} {x : ℝ × ℝ} (hx : x ∉ goldbachB9LogGridRegion n) : goldbachB9LogGridUpperIntegrand n x = 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridUpperIntegrand_le {n : ℕ} (hn : 0 < n) {x : ℝ × ℝ} (hx : x ∈ goldbachB9LogGridRegion n) : goldbachB9LogGridUpperIntegrand n x ≤ 480

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGrid_kernel_variation_step {n : ℕ} (hn : 0 < n) (q : Fin n × Fin n) {x : ℝ × ℝ} (hx : x ∈ goldbachB9LogGridCell n q) : 0 ≤ 1 / (1 - goldbachB9AlphaGridPoint n (↑q.1 + 1) - goldbachB9BetaGridPoint n (↑q.2 + 1)) - LiuWeight.liuLogKernel x ∧ 1 / (1 - goldbachB9AlphaGridPoint n (↑q.1 + 1) - goldbachB9BetaGridPoint n (↑q.2 + 1)) - LiuWeight.liuLogKernel x ≤ 36 * (goldbachB9AlphaGridStep n + goldbachB9BetaGridStep n)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGrid_kernel_error (n : ℕ) : 36 * (goldbachB9AlphaGridStep n + goldbachB9BetaGridStep n) = 96 / (5 * ↑n) ∧ 96 / (5 * ↑n) ≤ 20 / ↑n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGrid_kernel_variation {n : ℕ} (hn : 0 < n) (q : Fin n × Fin n) {x : ℝ × ℝ} (hx : x ∈ goldbachB9LogGridCell n q) : 0 ≤ 1 / (1 - goldbachB9AlphaGridPoint n (↑q.1 + 1) - goldbachB9BetaGridPoint n (↑q.2 + 1)) - LiuWeight.liuLogKernel x ∧ 1 / (1 - goldbachB9AlphaGridPoint n (↑q.1 + 1) - goldbachB9BetaGridPoint n (↑q.2 + 1)) - LiuWeight.liuLogKernel x ≤ 20 / ↑n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridUpperIntegrand_le_integrand_add {n : ℕ} (hn : 0 < n) {x : ℝ × ℝ} (hx : x ∈ goldbachB9LogGridRegion n) : goldbachB9LogGridUpperIntegrand n x ≤ LiuWeight.liuLogIntegrand x + 1600 / ↑n

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridErrorConstant_pos : 0 < 10000

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGridUpperSum_sub_mainIntegral_le (n : ℕ) (hn : 0 < n) : goldbachB9LogGridUpperSum n - goldbachB9MainIntegral ≤ 10000 / ↑n

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.exists_goldbachB9LogGridUpperSum_le_mainIntegral_add (δ : ℝ) (hδ : 0 < δ) : ∃ (n : ℕ), 0 < n ∧ goldbachB9LogGridUpperSum n ≤ goldbachB9MainIntegral + δ

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PairLogKernel_le_mainIntegral_eventually (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachB9PairLogKernel N ≤ goldbachB9MainIntegral + δ

First choose n from the tolerance, then take the fixed-n prime-size limit.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PairLogKernel_le_doubleIntegral_eventually (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachB9PairLogKernel N ≤ (∫ (u : ℝ) in 4 / 53..1 / 3, ∫ (v : ℝ) in 1 / 3..(1 - u) / 2, 1 / (u * v * (1 - u - v))) + δ

The terminal statement displays the actual double integral explicitly.