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

The high C10 double integral, without the sieve factor eight.

Equations

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

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighMainIntegral_eq_iteratedSetIntegral : goldbachB9HighMainIntegral = ∫ (u : ℝ) in Set.Ioc (1 / 10) (1 / 3), ∫ (v : ℝ) in Set.Ioc (1 / 3) ((1 - u) / 2), LiuWeight.liuLogIntegrand (u, v)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighSourceIndicator_integral_section (u : ℝ) : ∫ (v : ℝ), goldbachB9HighLogSourceRegion.indicator LiuWeight.liuLogIntegrand (u, v) = (Set.Ioc (1 / 10) (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_goldbachB9HighMainOuter : IntervalIntegrable (fun (u : ℝ) => ∫ (v : ℝ) in 1 / 3..(1 - u) / 2, 1 / (u * v * (1 - u - v))) MeasureTheory.volume (1 / 10) (1 / 3)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighMainIntegral_eq_setIntegral : goldbachB9HighMainIntegral = ∫ (x : ℝ × ℝ) in goldbachB9HighLogSourceRegion, LiuWeight.liuLogIntegrand x

Fubini uses the integrability of this high source indicator.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighMainIntegral_nonneg : 0 ≤ goldbachB9HighMainIntegral

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighLogGridUpperSum_sub_mainIntegral_le (n : ℕ) (hn : 0 < n) : goldbachB9HighLogGridUpperSum n - goldbachB9HighMainIntegral ≤ 10000 / ↑n

All three strip areas are those of the high domain, for every positive mesh.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.exists_goldbachB9HighLogGridUpperSum_le_mainIntegral_add (δ : ℝ) (hδ : 0 < δ) : ∃ (n : ℕ), 0 < n ∧ goldbachB9HighLogGridUpperSum n ≤ goldbachB9HighMainIntegral + δ

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

Choose the mesh from delta before taking its fixed-mesh prime-size limit.

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5HighFirstClosed_normalized_upper_integral (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hεu : ε < 2 / 15) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachS5Closed (goldbachDifferenceCarrier N ε) N (↑N ^ (1 / 10)) (↑N ^ (1 / 3))) ≤ (8 * goldbachB9HighMainIntegral + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

The actual high S5 consumer, with every analytic error paid into delta.