noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiHi (N m : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiHi N m = min (↑m.minFac) (↑N / ↑m)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiLo (N : ℕ) (ε : ℝ) (m : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiLo N ε m = min (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiHi N m) (max (↑N ^ (4 / 53)) (ε * ↑N / ↑m))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiEndpoints_bounds {N m : ℕ} {ε : ℝ} (hN : 2 ≤ N) (hm : m ∈ goldbachG11EffectiveProductSupport N ε) : ↑N ^ (4 / 53) ≤ goldbachG11PiLiLo N ε m ∧ goldbachG11PiLiLo N ε m ≤ goldbachG11PiLiHi N m ∧ goldbachG11PiLiHi N m ≤ ↑N / ↑m

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiLi_normalization (κ x : ℝ) : LiuWeight.liuLogarithmicIntegral κ x - LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) x = κ - 2 / Real.log 2

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLi_real_pnt (κ s γ : ℝ) (hs : 0 < s) (hγ : 0 < γ) : ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (y : ℝ), ↑N ^ γ ≤ y → |AnalyticNumberTheory.LargeSieve.PanPrincipal.primeCount ⌊y⌋₊ - LiuWeight.liuLogarithmicIntegral κ y| ≤ C * y / Real.log ↑N ^ s

Natural-endpoint PNT, with the actual floor-to-real interval paid separately.

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiEndpointError (κ : ℝ) (N : ℕ) (ε : ℝ) (m : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiEndpointError κ N ε m = AnalyticNumberTheory.LargeSieve.PanPrincipal.primeCount ⌊MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiHi N m⌋₊ - AnalyticNumberTheory.LargeSieve.PanPrincipal.primeCount ⌊MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiLo N ε m⌋₊ - (MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral κ (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiHi N m) - MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral κ (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiLo N ε m))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiEndpointError_eq_zero {κ ε : ℝ} {N m : ℕ} (h : goldbachG11PiLiLo N ε m = goldbachG11PiLiHi N m) : goldbachG11PiLiEndpointError κ N ε m = 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiLo_one (N m : ℕ) : goldbachG11PiLiLo N 1 m = goldbachG11PiLiHi N m

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLi_endpoint_pnt (κ s : ℝ) (hs : 0 < s) : ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ε : ℝ), ∀ m ∈ goldbachG11EffectiveProductSupport N ε, |goldbachG11PiLiEndpointError κ N ε m| ≤ C * (↑N / ↑m) / Real.log ↑N ^ s

The two actual geometric endpoints retain the reciprocal-product scale.