@[instance_reducible]

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachRepeatBound (P : Prop) : Decidable P

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachRepeatBound P = Classical.propDecidable P

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachR_le_twenty_mul_goldbachQA (A : Finset ℕ) (N : ℕ) (κ y : ℝ) (hA : ∀ n ∈ A, 1 ≤ n ∧ n < N) (hk : 1 / 21 < κ) : goldbachR A N (↑N ^ κ) y ≤ 20 * goldbachQA A N (↑N ^ κ)

The actual repeat mass is controlled by 20 copies of the actual square mass QA, using the unique repeated-prime encoding from Li--Liu's proof.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachR_real_le_forty_mul_div (A : Finset ℕ) (N : ℕ) (κ y : ℝ) (hA : ∀ n ∈ A, 1 ≤ n ∧ n < N) (hk : 1 / 21 < κ) (hz : 2 ≤ ↑N ^ κ) : ↑(goldbachR A N (↑N ^ κ) y) ≤ 40 * ↑N / ↑N ^ κ

Combined with the already-proved square-tail estimate, the repeat mass is bounded by 40 N / z once z = N^κ ≥ 2.