Documentation

MathlibNt.SieveTheory.LiLiuGoldbachProductCoefficientCap

source
theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductCoefficient_le_four_hundred_of_cutoff (N m : ℕ) (c : ℝ) :
goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) c m ≤ 400

The product-fibre cap does not depend on the upper cutoff.

Inspect dependencies

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

source
theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodBodySubset_product_fiber_card_le_four_hundred (N m : ℕ) (c : ℝ) (B : Finset GoldbachG11SwitchedBody) (hB : B ⊆ goldbachG11GoodSwitchedBodies N (↑N ^ (4 / 53)) c) :
{u ∈ B | goldbachG11SwitchedBodyProd u = m}.card ≤ 400

Any subset of good bodies retains the cap, without identifying equal products.

Inspect dependencies

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

source
noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11FilteredProductCoefficient (N : ℕ) (z c : ℝ) (C : GoldbachG11SwitchedBody → Prop) (m : ℕ) :
ℕ

Filter actual bodies first, then count every body representation in the product fibre.

Equations
Instances For
    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11FilteredProductCoefficient_le (N m : ℕ) (z c : ℝ) (C : GoldbachG11SwitchedBody → Prop) :
    goldbachG11FilteredProductCoefficient N z c C m ≤ goldbachG11ProductCoefficient N z c m
    Inspect dependencies

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

    source
    theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11FilteredProductCoefficient_le_four_hundred (N m : ℕ) (c : ℝ) (C : GoldbachG11SwitchedBody → Prop) :
    goldbachG11FilteredProductCoefficient N (↑N ^ (4 / 53)) c C m ≤ 400
    Inspect dependencies

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

    source
    noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11NormalizedFilteredProductCoefficient (N : ℕ) (z c : ℝ) (C : GoldbachG11SwitchedBody → Prop) (m : ℕ) :
    ℝ
    Equations
    Instances For
      Inspect dependencies

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

      source
      theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11NormalizedFilteredProductCoefficient_mem_Icc (N m : ℕ) (c : ℝ) (C : GoldbachG11SwitchedBody → Prop) :
      goldbachG11NormalizedFilteredProductCoefficient N (↑N ^ (4 / 53)) c C m ∈ Set.Icc 0 1
      Inspect dependencies

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

      source
      theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11NormalizedProductCoefficient_mem_Icc_of_cutoff (N m : ℕ) (c : ℝ) :
      goldbachG11NormalizedProductCoefficient N (↑N ^ (4 / 53)) c m ∈ Set.Icc 0 1
      Inspect dependencies

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