@[instance_reducible]

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

Equations

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

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.gateLoss (N : ℕ) (b c : ℝ) (w : ℕ → ℝ) (d : ℕ) : ℝ

The modulus-d loss from deleting the non-coprime part of the actual C10 product support.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.gateLoss N b c w d = |(↑d.totient)⁻¹ * ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10ProductSupport N b c with ¬m.Coprime d, w m|

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.gateLoss_eq (N : ℕ) (b c : ℝ) (w : ℕ → ℝ) (d : ℕ) : gateLoss N b c w d = |1 / ↑d.totient * ∑ m ∈ goldbachC10ProductSupport N b c with ¬m.Coprime d, w m|

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.sum_gateLoss_le_logCube {N Q : ℕ} {b c T : ℝ} {w : ℕ → ℝ} (hQ : Q ≤ N) (hN : 2 ≤ N) (hb : 0 < b) (hT : 0 ≤ T) (hw : ∀ ⦃m : ℕ⦄, m ∈ goldbachC10ProductSupport N b c → |w m| ≤ T / ↑m) : ∑ d ∈ Finset.Icc 1 Q, gateLoss N b c w d ≤ 4 * T / b * (1 + Real.log ↑N) ^ 3

Finite reciprocal-totient budget for deleting the non-coprime part of the actual C10 main support.