Documentation

MathlibNt.SieveTheory.LiLiuGoldbachB10UpperError

source
@[instance_reducible]
noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableB10UpperError (P : Prop) :
Decidable P
Equations
Instances For
    Inspect dependencies

    MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableB10UpperError · compiled type and proof/definition references.

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10_upperErrSum_le_commonModulusSum (N : ℕ) (hEven : Even N) (ε b c Z X : ℝ) (Q : ℕ) :
    have S := goldbachB10BoundingSieve N hEven ε b c Z X; LinearSieve.upperErrSum S (Q + 1) (LinearSieve.upperRosserWeight S.prodPrimes (Q + 1)) ≤ ∑ d ∈ Finset.Icc 1 Q with d.Coprime N, |↑(goldbachB10DivisorAtoms N d ε b c).card - X / ↑d.totient|

    The actual Rosser remainder needs only the unweighted coprime modulus sum. The natural Rosser level is Q+1, so its strict support is exactly d≤Q.

    Inspect dependencies

    MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10_upperErrSum_le_commonModulusSum · compiled type and proof/definition references.