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

The actual two-variable integral I10 from Liu's printed (5.46).

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10MainIntegral = ∫ (u : ℝ) in MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Beta..MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Gamma, ∫ (v : ℝ) in MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10Gamma..(1 - u) / 2, 1 / (u * v * (1 - u - v))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10MainIntegral_eq_setIntegral : goldbachB10MainIntegral = ∫ (x : ℝ × ℝ) in MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10LogSourceRegion✝, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10LogIntegrand✝ x

The actual B10 main integral is the set integral of the logarithmic kernel over the exact half-open source triangle.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10LogGridUpperSum_sub_mainIntegral_le (n : ℕ) (hn : 0 < n) : goldbachB10LogGridUpperSum n - goldbachB10MainIntegral ≤ 260 / ↑n

The selected B10 upper sum exceeds the exact integral by at most 260/n.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.tendsto_goldbachB10LogGridUpperSum_mainIntegral : Filter.Tendsto (fun (n : ℕ) => goldbachB10LogGridUpperSum (n + 1)) Filter.atTop (nhds goldbachB10MainIntegral)

The B10 logarithmic-grid upper sums converge to the exact printed integral I10 as the mesh tends to zero.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.eventually_abs_goldbachB10LogGridUpperSum_sub_mainIntegral_lt {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, |goldbachB10LogGridUpperSum (n + 1) - goldbachB10MainIntegral| < ε

Eventual epsilon form of goldbachB10LogGridUpperSum → I10.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.exists_abs_goldbachB10LogGridUpperSum_sub_mainIntegral_lt {ε : ℝ} (hε : 0 < ε) : ∃ (n₀ : ℕ), ∀ (n : ℕ), n₀ ≤ n → |goldbachB10LogGridUpperSum (n + 1) - goldbachB10MainIntegral| < ε

Threshold form of goldbachB10LogGridUpperSum → I10.