Documentation

MathlibNt.SieveTheory.LiLiuFouvryG9WeightedBoundaryGeometry

source
def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9WeightedRegion (n : ℕ) (h : ℝ) :
Set (ℝ × ℝ)
Equations
Instances For
    Inspect dependencies

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

    source
    def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9WeightedRightStrip (n : ℕ) :
    Set (ℝ × ℝ)
    Equations
    Instances For
      Inspect dependencies

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

      source
      theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_fouvryG9WeightedRightStrip (n : ℕ) :
      MeasurableSet (fouvryG9WeightedRightStrip n)
      Inspect dependencies

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

      source
      theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.volume_fouvryG9WeightedRightStrip (n : ℕ) :
      MeasureTheory.volume (fouvryG9WeightedRightStrip n) = ENNReal.ofReal (17 / 240 / ↑n)
      Inspect dependencies

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

      source
      def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9WeightedObliqueStrip (n : ℕ) (h : ℝ) :
      Set (ℝ × ℝ)
      Equations
      Instances For
        Inspect dependencies

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

        source
        theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.measurableSet_fouvryG9WeightedObliqueStrip (n : ℕ) (h : ℝ) :
        MeasurableSet (fouvryG9WeightedObliqueStrip n h)
        Inspect dependencies

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

        source
        theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9WeightedObliqueStrip_section (n : ℕ) (h u : ℝ) :
        Prod.mk u ⁻¹' fouvryG9WeightedObliqueStrip n h = if u ∈ Set.Icc (4 / 53) (1 / 3) then Set.Ioo ((1 - u) / 2) ((1 - u) / 2 + (h + goldbachB9AlphaGridStep n + 2 * goldbachB9BetaGridStep n) / 2) else ∅
        Inspect dependencies

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

        source
        theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.volume_fouvryG9WeightedObliqueStrip (n : ℕ) (h : ℝ) (hh : 0 ≤ h) :
        MeasureTheory.volume (fouvryG9WeightedObliqueStrip n h) = ENNReal.ofReal (41 / 318 * h + 1927 / 19080 / ↑n)
        Inspect dependencies

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

        source
        theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9WeightedRegion_subset_ambient {n : ℕ} (hn : 0 < n) (h : ℝ) :
        fouvryG9WeightedRegion n h ⊆ goldbachB9LogAmbientBox
        Inspect dependencies

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

        source
        theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9WeightedRegion_excess_subset {n : ℕ} (hn : 0 < n) (h : ℝ) :
        fouvryG9WeightedRegion n h \ fouvryG9WeightedSource ⊆ goldbachB9LeftStrip n ∪ goldbachB9BottomStrip n ∪ fouvryG9WeightedObliqueStrip n h ∪ fouvryG9WeightedRightStrip n
        Inspect dependencies

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