noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11FamilyErrorFactor (Q C K θ : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11FamilyErrorFactor Q C K θ = C * (θ + (θ ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log Q ^ (-(1 / 3)))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MixedLevel_positive {N : ℕ} {δ ρ : ℝ} (hN : 0 < N) (hρ : 0 < ρ) (k : ℕ × ℕ) : 0 < goldbachG11MixedLevel N δ ρ k

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MixedLevel_le_originalN {N : ℕ} {ε ρ δ : ℝ} (hN : 4 ≤ N) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (hbig : 4 ≤ ↑N ^ (4 / 53)) (hδ : 0 ≤ δ) {k : ℕ × ℕ} (hk : k ∈ goldbachG11GridUsed N ε ρ) : goldbachG11MixedLevel N δ ρ k ≤ ↑N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11UpperFactor_normalization {N : ℕ} {Q C K θ : ℝ} (hN : 4 ≤ N) (hQ : 0 < Q) (hlogQ : 0 < Real.log Q) (hQN : Q ≤ ↑N) : 4 * Real.exp (-Real.eulerMascheroniConstant) * fouvryG9UpperFactor N Q C K θ = 4 * Real.log ↑N / Real.log Q + 4 * Real.exp (-Real.eulerMascheroniConstant) * goldbachG11FamilyErrorFactor Q C K θ

Exact cancellation of the Euler--Mascheroni normalization, retaining the actual external-family error rather than discarding it.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorFactor_with_errors (ζ : ℝ) (hζ : 0 < ζ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ∀ (ε ρ δ θ C K : ℝ), 1 < ρ → ρ ≤ 5 / 4 → 0 ≤ δ → δ < 1 / 4 → 0 < θ → 0 ≤ C → 4 ≤ ↑N ^ (4 / 53) → ∀ k ∈ goldbachG11GridUsed N ε ρ, ∀ p ∈ goldbachG11GridShort N ρ k, fouvryG9UpperFactor N (goldbachG11MixedLevel N δ ρ k) C K θ * fouvryG9BaseEuler N √↑N * goldbachG11EulerCorrection N ≤ (1 + ζ) * goldbachG11EulerCorrection N * (goldbachG11AuthorWeight (Real.log ↑p / Real.log ↑N) + 32 * δ + 4 * Real.exp (-Real.eulerMascheroniConstant) * goldbachG11FamilyErrorFactor (goldbachG11MixedLevel N δ ρ k) C K θ) * (SingularSeries.liuSingularSeries N / Real.log ↑N)

Finite normalized author-weight bound, including every sieve and Euler correction. Subsequent small-parameter choices may absorb them, not erase them.