noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG67JRIntegral (τ : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG67JRIntegral τ = (1 / 2 * ∫ (u : ℝ) (v : ℝ) in 4 / 53..4 / 33, LiLiuGoldbachIdealPairKernel.kernel τ (u, v) / (u * v)) + ∫ (u : ℝ) in 4 / 53..4 / 33, ∫ (v : ℝ) in 4 / 33..3 / 11, LiLiuGoldbachIdealPairKernel.kernel τ (u, v) / (u * v)

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG67LogRectangleMass = 1 / 2 * MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.logarithmicRectangleMass (4 / 53) (4 / 33) (4 / 53) (4 / 33) + MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.logarithmicRectangleMass (4 / 53) (4 / 33) (4 / 33) (3 / 11)

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG67IntegralConstant = 53 / (2 * Real.exp Real.eulerMascheroniConstant) * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG67JRIntegral 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachJRKernel_symmetric (τ u v : ℝ) : LiLiuGoldbachIdealPairKernel.kernel τ (u, v) = LiLiuGoldbachIdealPairKernel.kernel τ (v, u)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPairKernelSum_le_ideal (N : ℕ) (τ : ℝ) (T : Finset (ℕ × ℕ)) (hT : ∀ p ∈ T, 0 < p.1 ∧ 0 < p.2) : goldbachPairKernelSum N (LiLiuGoldbachIdealPairKernel.kernel τ) T ≤ goldbachPairIdealSum N τ T

Pointwise passage keeps the actual totient, including its square diagonal.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG67JRIntegral_lower (τ η : ℝ) (hη : 0 < η) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachG67JRIntegral τ - η ≤ goldbachPairIdealSum N τ (goldbachG6Pairs N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) + goldbachPairIdealSum N τ (goldbachG7Pairs N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)))

Actual JR kernel and actual original pair sums, with a common threshold.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG67JRIntegral_truncation {τ : ℝ} (hτ : 0 ≤ τ) : goldbachG67JRIntegral 0 - τ * goldbachG67LogRectangleMass ≤ goldbachG67JRIntegral τ

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG67IdealSum_integral_lower (τ η : ℝ) (hτ : 0 ≤ τ) (hη : 0 < η) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachG67JRIntegral 0 - τ * goldbachG67LogRectangleMass - η ≤ goldbachPairIdealSum N τ (goldbachG6Pairs N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) + goldbachPairIdealSum N τ (goldbachG7Pairs N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)))