noncomputable def LiLiuGoldbachIdealPairKernel.kernel (τ : ℝ) (x : ℝ × ℝ) : ℝ

The actual JR lower kernel, with arbitrary real truncation parameter.

Equations

• LiLiuGoldbachIdealPairKernel.kernel τ x = max 0 (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965f ((1 / 2 - x.1 - x.2) / (4 / 53)) - τ)

noncomputable def LiLiuGoldbachIdealPairKernel.kernelLipschitzConstant : NNReal

A uniform constant for the product sup metric; independent of truncation.

Equations

• LiLiuGoldbachIdealPairKernel.kernelLipschitzConstant = ⟨MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965DelayConstant / (4 / 53), LiLiuGoldbachIdealPairKernel.kernelLipschitzConstant._proof_1⟩

theorem LiLiuGoldbachIdealPairKernel.kernel_nonneg (τ : ℝ) (x : ℝ × ℝ) : 0 ≤ kernel τ x

theorem LiLiuGoldbachIdealPairKernel.kernel_lipschitz (τ : ℝ) : LipschitzWith kernelLipschitzConstant (kernel τ)

theorem LiLiuGoldbachIdealPairKernel.primeLogExponent_mul (N : ℕ) {r s : ℕ} (hr : 0 < r) (hs : 0 < s) : MathlibNt.SieveTheory.LiuWeight.primeLogExponent N (r * s) = MathlibNt.SieveTheory.LiuWeight.primeLogExponent N r + MathlibNt.SieveTheory.LiuWeight.primeLogExponent N s

Multiplicative logarithmic coordinates, also when log N is zero.

theorem LiLiuGoldbachIdealPairKernel.kernel_div_totient_eq (N : ℕ) (τ : ℝ) {r s : ℕ} (hr : 0 < r) (hs : 0 < s) : kernel τ (MathlibNt.SieveTheory.LiuWeight.primeLogExponent N r, MathlibNt.SieveTheory.LiuWeight.primeLogExponent N s) / ↑(r * s).totient = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPairIdealWeight N τ (r * s)

Exact genuine totient weight, with no primality or distinctness assumption.

theorem LiLiuGoldbachIdealPairKernel.kernel_div_product_le (N : ℕ) (τ : ℝ) {r s : ℕ} (hr : 0 < r) (hs : 0 < s) : kernel τ (MathlibNt.SieveTheory.LiuWeight.primeLogExponent N r, MathlibNt.SieveTheory.LiuWeight.primeLogExponent N s) / (↑r * ↑s) ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPairIdealWeight N τ (r * s)

The raw reciprocal-product term is dominated by the genuine totient weight.

theorem LiLiuGoldbachIdealPairKernel.kernel_div_totient_square_eq (N : ℕ) (τ : ℝ) {r : ℕ} (hr : 0 < r) : kernel τ (MathlibNt.SieveTheory.LiuWeight.primeLogExponent N r, MathlibNt.SieveTheory.LiuWeight.primeLogExponent N r) / ↑(r ^ 2).totient = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPairIdealWeight N τ (r ^ 2)

The diagonal retains totient of the square, not a product of totients.

theorem LiLiuGoldbachIdealPairKernel.kernel_truncation_loss {τ : ℝ} (hτ : 0 ≤ τ) (x : ℝ × ℝ) : kernel 0 x - τ ≤ kernel τ x

Pointwise truncation loses at most its nonnegative parameter.

theorem LiLiuGoldbachIdealPairKernel.kernel_weighted_integrable (τ : ℝ) {a b c d : ℝ} (ha : 0 < a) (hc : 0 < c) : MeasureTheory.IntegrableOn (fun (x : ℝ × ℝ) => kernel τ x / (x.1 * x.2)) (Set.Ioc a b ×ˢ Set.Ioc c d) MeasureTheory.volume

Weighted integrability is automatic on every positive rectangle.

theorem LiLiuGoldbachIdealPairKernel.integral_truncation_loss {a b c d τ : ℝ} (ha : 0 < a) (hab : a < b) (hc : 0 < c) (hcd : c < d) (hτ : 0 ≤ τ) : (∫ (u : ℝ) in a..b, ∫ (v : ℝ) in c..d, kernel 0 (u, v) / (u * v)) - τ * MathlibNt.SieveTheory.PrimeReciprocalLogRectangle.logarithmicRectangleMass a b c d ≤ ∫ (u : ℝ) in a..b, ∫ (v : ℝ) in c..d, kernel τ (u, v) / (u * v)

Explicit truncation loss for the actual JR kernel on a positive rectangle.