noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2LogCoefficient (ε : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2LogCoefficient ε = 8 * Real.log ((1 - (9 / 19 - ε)) / (9 / 19 - ε))

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightKnownCoefficient (ε : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightKnownCoefficient ε = (1 - ε) * Real.exp (-Real.eulerMascheroniConstant) * (159 / 2 * MathlibNt.SieveTheory.SwitchingPrinciple.dimensionOneLowerLinearSieveFactor 6 + 33 / 2 * MathlibNt.SieveTheory.SwitchingPrinciple.dimensionOneLowerLinearSieveFactor (33 / 8)) - 4 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2LogCoefficient ε - 8 * (1 - ε) * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10I10

@[simp]

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2LogCoefficient_zero : goldbachS2LogCoefficient 0 = 8 * Real.log (10 / 9)

@[simp]

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightKnownCoefficient_zero : goldbachWeightKnownCoefficient 0 = Real.exp (-Real.eulerMascheroniConstant) * (159 / 2 * SwitchingPrinciple.dimensionOneLowerLinearSieveFactor 6 + 33 / 2 * SwitchingPrinciple.dimensionOneLowerLinearSieveFactor (33 / 8)) - 32 * Real.log (10 / 9) - 8 * goldbachB10I10

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2_g3_upper_small_epsilon (δ : ℝ) (hδ : 0 < δ) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 2 / 15 ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachS2 (goldbachDifferenceCarrier N ε) N (↑N ^ (9 / 19 - ε))) ≤ (8 * Real.log (10 / 9) + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

The small epsilon is selected before the large-N threshold. No uniform threshold over all small epsilon is asserted.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_remainingEight_small_epsilon (δ : ℝ) (hδ : 0 < δ) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 2 / 15 ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachWeightRemainingEight (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11))) + (goldbachWeightKnownCoefficient 0 - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ 4 * ↑(D19 N)

A single epsilon restriction controls all already-consumed coefficients. The remaining eight signed counts retain their actual epsilon-dependent carrier.