@[instance_reducible]

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

Equations

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachBadCount_le_primeFactors (N : ℕ) (ε : ℝ) (hN : N ≠ 0) : goldbachBadCount (goldbachDifferenceCarrier N ε) N ≤ ↑N.primeFactors.card

An actual noncoprime difference N-p comes from a prime divisor of N. No coprimality or parity exception is removed from the original carrier.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbach_primeFactors_card_le_sqrt_add_one (N : ℕ) (hN : N ≠ 0) : N.primeFactors.card ≤ N.sqrt + 1

At most one distinct prime divisor lies above the integer square root.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachBadCount_twice_le_four_div (N : ℕ) (ε z : ℝ) (hN : 1 ≤ N) (hz : 0 < z) (hzN : z ^ 2 ≤ ↑N) : ↑(2 * goldbachBadCount (goldbachDifferenceCarrier N ε) N) ≤ 4 * ↑N / z

The exact bad-set contribution is paid uniformly whenever z²≤N. This finite estimate requires no analytic distribution theorem.