noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectangleMass (N : ℕ) (ρ : ℝ) (k : ℕ × ℕ × ℕ) : ℝ

Actual labelled rectangle mass; no multiplicity is removed.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectangleMass N ρ k = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongProducts N ρ k, ∑ n ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectanglePrimeSupport N ρ k, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongAlpha N ρ k m * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectangleBeta N n

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedPairs (N : ℕ) (ρ : ℝ) : Finset (ℕ × ℕ)

Positive enlargement of the original pair curve, not the original C10 carrier.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedPairs N ρ = {rs ∈ Finset.range (N + 1) ×ˢ Finset.range (N + 1) | Nat.Prime rs.1 ∧ Nat.Prime rs.2 ∧ ↑N ^ (4 / 53) ≤ ↑rs.1 ∧ ↑rs.1 < ↑N ^ (1 / 10) ∧ ↑N ^ (1 / 3) ≤ ↑rs.2 ∧ ↑rs.1 * ↑rs.2 ^ 2 ≤ ρ ^ 3 * ↑N}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedPairKernel (N : ℕ) (ρ δ : ℝ) : ℝ

Logarithmic kernel for the genuinely enlarged pair region.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedPairKernel N ρ δ = ∑ rs ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RelaxedPairs N ρ, have u := Real.log ↑rs.1 / Real.log ↑N; have v := Real.log ↑rs.2 / Real.log ↑N; have w := 1 + 3 * Real.log ρ / Real.log ↑N; 1 / (↑rs.1 * ↑rs.2 * (w - u - v) * (5 / 9 * (1 - u) - δ))