theorem
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGrid_publicAudit :
0 ≤ goldbachB9MainIntegral ∧ (∀ (n : ℕ), 0 < n → goldbachB9LogGridUpperSum n - goldbachB9MainIntegral ≤ 10000 / ↑n) ∧ (∀ (δ : ℝ), 0 < δ → ∃ (n : ℕ), 0 < n ∧ goldbachB9LogGridUpperSum n ≤ goldbachB9MainIntegral + δ) ∧ ∀ (δ : ℝ), 0 < δ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachB9PairLogKernel N ≤ goldbachB9MainIntegral + δ
Inspect dependencies
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LogGrid_publicAudit · compiled type and proof/definition references.