noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_oneThirdExpFreeIntegral : ℝ

Exact exp-free integral for beta = 1 / 3; this is not a rational bound.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_oneThirdExpFreeIntegral = ∫ (s : ℝ) in 53 / 24..45 / 8, (fun (s : ℝ) => (if s ≤ 3 then 1 else if s ≤ 5 then 1 + MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertInnerIntegral s else 1 + MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertInnerIntegral 5 + ∫ (t : ℝ) in 5..s, (Real.log (t - 2) + ∫ (v : ℝ) in 3..t - 2, MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertInnerIntegral v / v) / (t - 1)) / (s * (53 / 8 - s))) s

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_oneThirdExpFreeIntegral_integrable : IntervalIntegrable (fun (s : ℝ) => (if s ≤ 3 then 1 else if s ≤ 5 then 1 + SwitchingPrinciple.jurkatRichertInnerIntegral s else 1 + SwitchingPrinciple.jurkatRichertInnerIntegral 5 + ∫ (t : ℝ) in 5..s, (Real.log (t - 2) + ∫ (v : ℝ) in 3..t - 2, SwitchingPrinciple.jurkatRichertInnerIntegral v / v) / (t - 1)) / (s * (53 / 8 - s))) MeasureTheory.volume (53 / 24) (45 / 8)

Integrability of the actual exp-free endpoint expression.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_oneThird_coefficient_eq : 53 / 2 * Real.exp (-Real.eulerMascheroniConstant) * goldbachS3_primeKernelIntegral (1 / 3) = 53 * goldbachS3_oneThirdExpFreeIntegral

Exact identification with the unchanged production coefficient.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_normalized_upper_oneThird_exp_free (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hεu : ε < 2 / 15) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachS3Closed (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (1 / 3))) ≤ ((1 - ε) * (53 * goldbachS3_oneThirdExpFreeIntegral) + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Actual normalized count at beta = 1 / 3, with the full strict mother carrier, epsilon range, threshold, parity and (1-epsilon) retained. The rational scalar bound is deliberately not claimed here.

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_threeEleventhsExpFreeIntegral : ℝ

Exact exp-free integral for beta = 3 / 11; this is not a rational bound.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_threeEleventhsExpFreeIntegral = ∫ (s : ℝ) in 265 / 88..45 / 8, (fun (s : ℝ) => (if s ≤ 3 then 1 else if s ≤ 5 then 1 + MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertInnerIntegral s else 1 + MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertInnerIntegral 5 + ∫ (t : ℝ) in 5..s, (Real.log (t - 2) + ∫ (v : ℝ) in 3..t - 2, MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertInnerIntegral v / v) / (t - 1)) / (s * (53 / 8 - s))) s

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_threeEleventhsExpFreeIntegral_integrable : IntervalIntegrable (fun (s : ℝ) => (if s ≤ 3 then 1 else if s ≤ 5 then 1 + SwitchingPrinciple.jurkatRichertInnerIntegral s else 1 + SwitchingPrinciple.jurkatRichertInnerIntegral 5 + ∫ (t : ℝ) in 5..s, (Real.log (t - 2) + ∫ (v : ℝ) in 3..t - 2, SwitchingPrinciple.jurkatRichertInnerIntegral v / v) / (t - 1)) / (s * (53 / 8 - s))) MeasureTheory.volume (265 / 88) (45 / 8)

Integrability of the actual exp-free endpoint expression.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_threeElevenths_coefficient_eq : 53 / 2 * Real.exp (-Real.eulerMascheroniConstant) * goldbachS3_primeKernelIntegral (3 / 11) = 53 * goldbachS3_threeEleventhsExpFreeIntegral

Exact identification with the unchanged production coefficient.

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

Actual normalized count at beta = 3 / 11, with the full strict mother carrier, epsilon range, threshold, parity and (1-epsilon) retained. The rational scalar bound is deliberately not claimed here.