Documentation

MathlibNt.SieveTheory.LiLiuGoldbachG12BoundingSieve

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

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

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

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

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

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

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

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

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

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

          Equations
          Instances For
            Inspect dependencies

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

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

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

            source
            noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedBoundingSieve (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 G12 weighted pushforward.

            Equations
            Instances For
              Inspect dependencies

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

              source
              theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedOutput_sum (N : ℕ) (ε : ℝ) (P : ℕ → Prop) [DecidablePred P] :
              ∑ p ∈ goldbachG12LinkedOutputSupport N ε with P p, goldbachG12LinkedOutputWeight N ε p = ∑ m ∈ goldbachG12ActiveProductSupport N, goldbachG12NormalizedCoefficient N m * ↑{r ∈ goldbachG11LinkedPrimeWindow N ε m | P (N - r * m)}.card
              Inspect dependencies

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

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

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

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

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

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

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

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

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

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

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