Documentation

MathlibNt.SieveTheory.LiLiuGoldbachG11BoundingSieve

source
@[reducible, inline]
abbrev MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.GoldbachG11LinkedAtom :
Type
Equations
Instances For
    Inspect dependencies

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

    source
    noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedAtoms (N : ℕ) (ε : ℝ) :
    Finset GoldbachG11LinkedAtom
    Equations
    Instances For
      Inspect dependencies

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

      source
      def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedOutput (N : ℕ) (x : GoldbachG11LinkedAtom) :
      ℕ
      Equations
      Instances For
        Inspect dependencies

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

        source
        noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedOutputSupport (N : ℕ) (ε : ℝ) :
        Finset ℕ
        Equations
        Instances For
          Inspect dependencies

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

          source
          noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedOutputWeight (N : ℕ) (ε : ℝ) (p : ℕ) :
          ℝ

          Weighted fibres, not a set of distinct outputs with weight one.

          Equations
          Instances For
            Inspect dependencies

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedOutputWeight_nonneg (N : ℕ) (ε : ℝ) (p : ℕ) :
            0 ≤ goldbachG11LinkedOutputWeight N ε p
            Inspect dependencies

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

            source
            noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedBoundingSieve (N : ℕ) (hEven : Even N) (ε Z X : ℝ) :
            BoundingSieve

            Reuse the accepted Goldbach prime product and dimension function; replace only its finite mother and weights by the actual G11 weighted pushforward.

            Equations
            Instances For
              Inspect dependencies

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

              source
              theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedOutput_sum (N : ℕ) (ε : ℝ) (P : ℕ → Prop) [DecidablePred P] :
              ∑ p ∈ goldbachG11LinkedOutputSupport N ε with P p, goldbachG11LinkedOutputWeight N ε p = ∑ m ∈ goldbachG11EffectiveProductSupport N ε, goldbachG11EffectiveProductCoefficient N ε m * ↑{r ∈ goldbachG11LinkedPrimeWindow N ε m | P (N - r * m)}.card
              Inspect dependencies

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

              source
              noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedSiftedMass (N : ℕ) (ε Z : ℝ) :
              ℝ
              Equations
              Instances For
                Inspect dependencies

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

                source
                theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedBoundingSieve_multSum (N : ℕ) (hEven : Even N) (ε Z X : ℝ) (d : ℕ) :
                BoundingSieve.multSum d = ∑ m ∈ goldbachG11EffectiveProductSupport N ε, goldbachG11EffectiveProductCoefficient N ε m * ↑{r ∈ goldbachG11LinkedPrimeWindow N ε m | d ∣ N - r * m}.card
                Inspect dependencies

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

                source
                theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedBoundingSieve_siftedSum (N : ℕ) (hEven : Even N) (ε Z X : ℝ) :
                BoundingSieve.siftedSum = goldbachG11LinkedSiftedMass N ε Z
                Inspect dependencies

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

                source
                theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedBoundingSieve_nu {N : ℕ} (hEven : Even N) (ε Z X : ℝ) {d : ℕ} (hd : d ∣ goldbachB10ProdPrimes N Z) :
                (goldbachG11LinkedBoundingSieve N hEven ε Z X).nu d = 1 / ↑d.totient
                Inspect dependencies

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

                source
                theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedBoundingSieve_rem (N : ℕ) (hEven : Even N) (ε Z X : ℝ) {d : ℕ} (hd : d ∣ goldbachB10ProdPrimes N Z) :
                BoundingSieve.rem d = ∑ m ∈ goldbachG11EffectiveProductSupport N ε, goldbachG11EffectiveProductCoefficient N ε m * ↑{r ∈ goldbachG11LinkedPrimeWindow N ε m | d ∣ N - r * m}.card - X / ↑d.totient
                Inspect dependencies

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