Documentation

MathlibNt.SieveTheory.LiLiuGoldbachG11PrimeKernelMeshIntegration

source
noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshDensity (x : (ℝ × ℝ) × ℝ × ℝ) :
ℝ
Equations
Instances For
    Inspect dependencies

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

    source
    noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshIntegrand (h : ℝ → ℝ) (x : (ℝ × ℝ) × ℝ × ℝ) :
    ℝ
    Equations
    Instances For
      Inspect dependencies

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

      source
      theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.continuousOn_goldbachG11MeshDensity :
      ContinuousOn goldbachG11MeshDensity goldbachG11MeshAmbient
      Inspect dependencies

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

      source
      theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshDensity_nonneg {x : (ℝ × ℝ) × ℝ × ℝ} (hx : x ∈ goldbachG11MeshAmbient) :
      0 ≤ goldbachG11MeshDensity x
      Inspect dependencies

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

      source
      theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.integrableOn_goldbachG11MeshDensity {s : Set ((ℝ × ℝ) × ℝ × ℝ)} (hs : MeasurableSet s) (hsub : s ⊆ goldbachG11MeshAmbient) :
      MeasureTheory.IntegrableOn goldbachG11MeshDensity s MeasureTheory.volume
      Inspect dependencies

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

      source
      theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.integrable_goldbachG11MeshSource (h : ℝ → ℝ) (hh : ContinuousOn h (Set.Icc (4 / 53) (4 / 33))) :
      MeasureTheory.Integrable (goldbachG11MeshSource.indicator (goldbachG11MeshIntegrand h)) MeasureTheory.volume
      Inspect dependencies

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

      source
      theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LogBoxMass_eq_meshIntegral (n : ℕ) (j : (Fin (n + 1) × Fin (n + 1)) × Fin (n + 1) × Fin (n + 1)) :
      goldbachG11LogBoxMass (goldbachG11MeshLo n j) (goldbachG11MeshHi n j) = ∫ (x : (ℝ × ℝ) × ℝ × ℝ) in goldbachG11MeshCell n j, goldbachG11MeshDensity x
      Inspect dependencies

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

      source
      theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MeshSource_mem_iff (r q s t : ℝ) :
      ((r, q), s, t) ∈ goldbachG11MeshSource ↔ r ∈ Set.Ioc (4 / 53) (4 / 33) ∧ q ∈ Set.Icc r (4 / 33) ∧ s ∈ Set.Icc q (4 / 33) ∧ t ∈ Set.Icc s (4 / 33)
      Inspect dependencies

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

      source
      theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeIntegral_eq_meshSource (h : ℝ → ℝ) (hh : ContinuousOn h (Set.Icc (4 / 53) (4 / 33))) :
      goldbachG11PrimeIntegral h = ∫ (x : (ℝ × ℝ) × ℝ × ℝ), goldbachG11MeshSource.indicator (goldbachG11MeshIntegrand h) x
      Inspect dependencies

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