Documentation

MathlibNt.SieveTheory.LiLiuGoldbachWeightTriplePartition

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

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

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

    The part of S6Closed with middle prime s ≤ b, keeping the original t,r,s nesting and all closed-endpoint/repeat contributions.

    Equations
    Instances For
      Inspect dependencies

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

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

      The complementary part of S6Closed with b < s.

      Equations
      Instances For
        Inspect dependencies

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

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

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

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

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

        source
        theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightT14_eq_goldbachS6Closed (A : Finset ℕ) (N : ℕ) (z b : ℝ) :
        goldbachWeightT14 A N z b = goldbachS6Closed A N z b
        Inspect dependencies

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

        source
        theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightLowMiddle_add_goldbachWeightUpperMiddle_eq_goldbachS6Closed (A : Finset ℕ) (N : ℕ) (z b y : ℝ) :
        goldbachWeightLowMiddle A N z b y + goldbachWeightUpperMiddle A N z b y = goldbachS6Closed A N z y
        Inspect dependencies

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

        source
        theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightT14_add_goldbachWeightT15_eq_goldbachWeightLowMiddle_add_goldbachB6 (A : Finset ℕ) (N : ℕ) (z b c : ℝ) (_hz : 2 ≤ z) (hzb : z ≤ b) (hbc : b ≤ c) :
        goldbachWeightT14 A N z b + goldbachWeightT15 A N z b c = goldbachWeightLowMiddle A N z b c + goldbachB6 A N z b
        Inspect dependencies

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

        source
        theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightLowMiddle_monotone_right (A : Finset ℕ) (N : ℕ) (z b c u : ℝ) (hcu : c ≤ u) :
        goldbachWeightLowMiddle A N z b c ≤ goldbachWeightLowMiddle A N z b u
        Inspect dependencies

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

        source
        theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightT14_add_goldbachWeightT15_add_goldbachWeightUpperMiddle_le_goldbachS6Closed_add_goldbachB6 (A : Finset ℕ) (N : ℕ) (z b c u : ℝ) (hz : 2 ≤ z) (hzb : z ≤ b) (hbc : b ≤ c) (hcu : c ≤ u) :
        goldbachWeightT14 A N z b + goldbachWeightT15 A N z b c + goldbachWeightUpperMiddle A N z b u ≤ goldbachS6Closed A N z u + goldbachB6 A N z b
        Inspect dependencies

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