noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10MainLogProductSum (N : ℕ) (b c : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10MainLogProductSum N b c = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10ProductSupport N b c, 1 / (↑m * (1 - Real.log ↑m / Real.log ↑N))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10MainLogProductSum_nonneg {N : ℕ} {b γ : ℝ} (hN : 2 ≤ N) (hγ : γ < 1 / 3) : 0 ≤ goldbachB10MainLogProductSum N b (↑N ^ γ)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10ContinuousMainMass_le_logProductSum (ε γ η : ℝ) (hε : 0 < ε) (hεlt : ε < 1) (hγ : γ < 1 / 3) (hη : 0 < η) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (b : ℝ), goldbachB10ContinuousMainMass N ε b (↑N ^ γ) ≤ (1 - ε + η) * (↑N / Real.log ↑N) * goldbachB10MainLogProductSum N b (↑N ^ γ)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10MainMass_le_logProductSum (ε γ η τ : ℝ) (hε : 0 < ε) (hεlt : ε < 1) (hγ : γ < 1 / 3) (hη : 0 < η) (hτ : 0 < τ) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (β : ℝ), 1 / 18 < β → goldbachB10MainMass N ε (↑N ^ β) (↑N ^ γ) ≤ ((1 - ε + η) * goldbachB10MainLogProductSum N (↑N ^ β) (↑N ^ γ) + τ) * (↑N / Real.log ↑N)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10MainLogProductSum_eq_pair_sum (N : ℕ) (b c : ℝ) : goldbachB10MainLogProductSum N b c = ∑ rs ∈ goldbachC10Pairs N b c, 1 / (↑rs.1 * ↑rs.2 * (1 - Real.log ↑rs.1 / Real.log ↑N - Real.log ↑rs.2 / Real.log ↑N))

Reindexing preserves the actual prime-pair carrier, including repeated factors and closed endpoints.