theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9MainScalar_initial {N : ℕ} {Q : ℝ} (hN : 1 < ↑N) (hQ : 1 < Q) (hQN : Q ≤ ↑N) : JurkatRichert1965ChenGammaOneQOne.jr1965F (Real.log Q / Real.log √↑N) = Real.exp Real.eulerMascheroniConstant * Real.log ↑N / Real.log Q ∧ Real.exp Real.eulerMascheroniConstant ≤ JurkatRichert1965ChenGammaOneQOne.jr1965F (Real.log Q / Real.log √↑N)

The real initial branch, with the sqrt logarithm cancelled exactly.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9MainScalar_normalize {N : ℕ} {Q C K η ζ A : ℝ} (hN : 1 < ↑N) (hQ : 1 < Q) (hQN : Q ≤ ↑N) (hζ : 0 < ζ) (hV : 0 ≤ fouvryG9BaseEuler N √↑N) (hbase : fouvryG9BaseEuler N √↑N * Real.log ↑N ≤ 4 * Real.exp (-Real.eulerMascheroniConstant) * (1 + ζ) * SingularSeries.liuSingularSeries N) (hA : 0 ≤ A) (hAu : A ≤ 1 + ζ) (herr : C * (η + (η ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log Q ^ (-(1 / 3))) ≤ ζ * Real.exp Real.eulerMascheroniConstant) : fouvryG9BaseEuler N √↑N * A * fouvryG9UpperFactor N Q C K η ≤ 4 * (1 + ζ) ^ 3 * SingularSeries.liuSingularSeries N / Real.log Q

Load-bearing normalization of the actual base product and actual upper factor. The hypotheses here are precisely the three near-one estimates, discharged below.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9MainScalar_cube {x : ℝ} (hx : 0 ≤ x) (hxu : x ≤ 1) : (1 + x) ^ 3 ≤ 1 + 7 * x

Elementary budget: the entire correction cube pays only one near-one factor.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9MainScalar_payment (C K τ : ℝ) (hC : 0 < C) (_hK : 1 < K) (hτ : 0 < τ) : ∃ (η : ℝ), 0 < η ∧ η < 1 / 8 ∧ ∀ (δ : ℝ), 0 ≤ δ → δ < 1 / 4 → ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → Even N → ∀ (T : ℝ), 1 ≤ T → T ≤ ↑N ^ (1 / 10) → have Q := ↑N ^ (5 / 9 - δ) / T ^ (5 / 9); fouvryG9BaseEuler N √↑N * (1 + 1 / (↑N ^ (4 / 53) / 2 - 2)) ^ 3 * fouvryG9UpperFactor N Q C K η ≤ 4 * (1 + τ) * SingularSeries.liuSingularSeries N / Real.log Q

The complete scalar payment. Eta is fixed before delta, N and the short scale. No scalar estimate is assumed: the product normalization and all tails are paid.