Documentation

MathlibNt.SieveTheory.LiLiuGoldbachG11AuthorActualContract

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11_author_actual_small_epsilon (δ : ℝ) :
0 < δ → ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachWeightG11 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ (10191 / 100000 + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Exact actual-count input expected by the existing final assembly. The small-epsilon window is furnished here, not assumed by a downstream caller.

Inspect dependencies

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