noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPairIdealWeight (N : ℕ) (ρ : ℝ) (m : ℕ) : ℝ

The ideal coordinate retains the actual product, before prime-pair quadrature.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPairIdealWeight N ρ m = max 0 (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965f ((1 / 2 - Real.log ↑m / Real.log ↑N) / (4 / 53)) - ρ) / ↑m.totient

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPairIdealSum N ρ T = ∑ a ∈ T, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPairIdealWeight N ρ (a.1 * a.2)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPair_ideal_clip_eventually (B ρ : ℝ) (hB : 0 ≤ B) (hρ : 0 < ρ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (m : ℕ), 0 < m → ↑m ≤ ↑N ^ (13 / 33) → max 0 (JurkatRichert1965ChenGammaOneQOne.jr1965f ((1 / 2 - Real.log ↑m / Real.log ↑N) / (4 / 53)) - 2 * ρ) ≤ max 0 (JurkatRichert1965ChenGammaOneQOne.jr1965f (Real.log ↑(LiuWeight.panModulusCutoff N B / m + 1) / Real.log (↑N ^ (4 / 53))) - ρ)

Uniform transport of a nonnegative clipped lower kernel, including crossings of two.