Documentation

MathlibNt.SieveTheory.LiLiuGoldbachWeightInitial

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

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

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

    The weakly ordered closed double sum Σ_{z≤r≤s≤b, r,s∈P(N)} H(A,N,rs;z).

    Equations
    Instances For
      Inspect dependencies

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

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

      The closed cross double sum Σ_{z≤r≤b≤t≤c, r,t∈P(N)} H(A,N,rt;z).

      Equations
      Instances For
        Inspect dependencies

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

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

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

        Equations
        Instances For
          Inspect dependencies

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

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

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

          Equations
          Instances For
            Inspect dependencies

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

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

            The actual diagonal square contribution Σ_{z≤r<b, r∈P(N)} H(A,N,r²;z).

            Equations
            Instances For
              Inspect dependencies

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

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

              The closed endpoint pair mass Σ_{z≤r≤s=b, r,s∈P(N)} H(A,N,rs;z), including r = s = b.

              Equations
              Instances For
                Inspect dependencies

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

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

                The closed endpoint cross mass Σ_{r=b≤t≤c, r,t∈P(N)} H(A,N,rt;z), including r = t = b.

                Equations
                Instances For
                  Inspect dependencies

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

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

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

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

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

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

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

                  source
                  theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_initial_refinement (A : Finset ℕ) (N : ℕ) (z b c : ℝ) (_hz : 2 ≤ z) (hzb : z ≤ b) (hbc : b ≤ c) :
                  goldbachS1 A N b - goldbachS3Closed A N b c ≥ goldbachS1 A N z - goldbachS3Closed A N z c + goldbachWeightG6 A N z b + goldbachWeightG7 A N z b c - goldbachWeightG14 A N z b - goldbachWeightG15 A N z b c - goldbachWeightD6 A N z b - goldbachWeightB6pair A N z b - goldbachWeightB7 A N z b c
                  Inspect dependencies

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