Documentation

MathlibNt.SieveTheory.LiLiuGoldbachWeightQuadruple

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

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

    source
    noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightT14 (A : Finset ℕ) (N : ℕ) (z b : ℝ) :
    ℤ

    The weakly ordered closed triple sum Σ_{z≤r≤s≤t≤b} H(A,N*r,rst;s).

    Equations
    Instances For
      Inspect dependencies

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

      source
      noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightT15 (A : Finset ℕ) (N : ℕ) (z b c : ℝ) :
      ℤ

      The closed cross triple sum Σ_{z≤r≤s≤b≤t≤c} H(A,N*r,rst;s).

      Equations
      Instances For
        Inspect dependencies

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

        source
        noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11 (A : Finset ℕ) (N : ℕ) (z b : ℝ) :
        ℤ

        The weakly ordered closed quadruple sum Σ_{z≤r≤q≤s≤t≤b} H(A,N*r,rqst;q).

        Equations
        Instances For
          Inspect dependencies

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

          source
          noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG12 (A : Finset ℕ) (N : ℕ) (z b c : ℝ) :
          ℤ

          The closed cross quadruple sum Σ_{z≤r≤q≤s≤b≤t≤c} H(A,N*r,rqst;q).

          Equations
          Instances For
            Inspect dependencies

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightT14_nonneg (A : Finset ℕ) (N : ℕ) (z b : ℝ) :
            0 ≤ goldbachWeightT14 A N z b
            Inspect dependencies

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightT15_nonneg (A : Finset ℕ) (N : ℕ) (z b c : ℝ) :
            0 ≤ goldbachWeightT15 A N z b c
            Inspect dependencies

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11_nonneg (A : Finset ℕ) (N : ℕ) (z b : ℝ) :
            0 ≤ goldbachWeightG11 A N z b
            Inspect dependencies

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG12_nonneg (A : Finset ℕ) (N : ℕ) (z b c : ℝ) :
            0 ≤ goldbachWeightG12 A N z b c
            Inspect dependencies

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG14_le_goldbachWeightT14_add_goldbachWeightG11 (A : Finset ℕ) (N : ℕ) (z b : ℝ) :
            goldbachWeightG14 A N z b ≤ goldbachWeightT14 A N z b + goldbachWeightG11 A N z b
            Inspect dependencies

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

            source
            theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG15_le_goldbachWeightT15_add_goldbachWeightG12 (A : Finset ℕ) (N : ℕ) (z b c : ℝ) :
            goldbachWeightG15 A N z b c ≤ goldbachWeightT15 A N z b c + goldbachWeightG12 A N z b c
            Inspect dependencies

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