2.4. Signed distance and coarea🔗

Theorem2.4.1

uses 1

Used by 2

Reverse dependency previews

Preview

Lemma 2.4.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagsbentkusgaussian-geometrysigned-distancesource-raic-2019fidelity-exact-eikonal

Signed distance and its eikonal identity. Let A\subsetneq\mathbb R^d be a nonempty convex set and define \delta_A(x)=d(x,A)-d(x,A^c) =\begin{cases} -d(x,A^c),&x\in A,\\ d(x,A),&x\notin A. \end{cases} Then \delta_A is Fréchet differentiable at Lebesgue-almost every point and \|D\delta_A(x)\|=1 at almost every such point.

Lean code for Theorem2.4.1●2 declarations

defdefined in ProbabilityApproximation/ConvexGeometry/GaussianShell.lean

complete

def ProbabilityTheory.setSignedDistance {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d))) (x : EuclideanSpace ℝ (Fin d)) :
  ℝ

def ProbabilityTheory.setSignedDistance
  {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d)))
  (x : EuclideanSpace ℝ (Fin d)) : ℝ

The signed distance to a set, negative on its interior side and positive on its exterior
side.  This is Raič's signed-distance function before restricting to a convex set.

theoremdefined in ProbabilityApproximation/ConvexGeometry/GaussianShell.lean

complete

theorem ProbabilityTheory.ae_norm_fderiv_setSignedDistance_eq_one {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} (hne : s.Nonempty)
  (hsne : s ≠ Set.univ) (hs : Convexity.IsConvexSet ℝ s) :
  ∀ᵐ (x : EuclideanSpace ℝ (Fin d)),
    ‖fderiv ℝ (ProbabilityTheory.setSignedDistance s) x‖ = 1

theorem ProbabilityTheory.ae_norm_fderiv_setSignedDistance_eq_one
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hne : s.Nonempty) (hsne : s ≠ Set.univ)
  (hs : Convexity.IsConvexSet ℝ s) :
  ∀ᵐ (x : EuclideanSpace ℝ (Fin d)),
    ‖fderiv ℝ
          (ProbabilityTheory.setSignedDistance
            s)
          x‖ =
      1

Raič (2019), Proposition 3.3's eikonal conclusion for a nonempty proper convex Euclidean
set: the Fréchet derivative of signed distance has norm one almost everywhere.

Raič (2019), defines the signed distance on printed pp. 2825--2826 and proves the almost-everywhere differentiability and eikonal conclusions in Proposition 3.3(2)--(3), printed p. 2844. The formal statement uses Fréchet derivatives on Euclidean space.

Lemma2.4.2

Statement uses 2

Statement dependency previews

Preview

Lemma 2.1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Tagsbentkusgaussian-geometrysigned-distanceparallel-frontierssource-raic-2019fidelity-explicit-boundary-conventions

Signed-distance fibers are parallel-set frontiers. Under the preceding hypotheses, for t>0, t=0, and t<0, respectively, \begin{aligned} \{x:\delta_A(x)=t\} &=\partial\{x:d(x,\overline A)\le t\},\\ \{x:\delta_A(x)=0\}&=\partial A,\\ \{x:\delta_A(x)=t\} &=\partial\{x\in A:B(x,-t)\subseteq A\}. \end{aligned} Here the outer parallel set is closed and the ball in the inner parallel set is open.

Lean code for Lemma2.4.2●3 theorems

theoremdefined in ProbabilityApproximation/ConvexGeometry/GaussianShell.lean

complete

theorem ProbabilityTheory.signedDistance_level_pos_eq_frontier_cthickening
  {d : ℕ} {s : Set (EuclideanSpace ℝ (Fin d))} (hne : s.Nonempty)
  (hs : Convexity.IsConvexSet ℝ s) {t : ℝ} (ht : 0 < t) :
  {x | ProbabilityTheory.setSignedDistance s x = t} =
    frontier (Metric.cthickening t (closure s))

theorem ProbabilityTheory.signedDistance_level_pos_eq_frontier_cthickening
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hne : s.Nonempty)
  (hs : Convexity.IsConvexSet ℝ s) {t : ℝ}
  (ht : 0 < t) :
  {x |
      ProbabilityTheory.setSignedDistance
          s x =
        t} =
    frontier
      (Metric.cthickening t (closure s))

A positive signed-distance level set is exactly the frontier of the corresponding closed
outer parallel set.  This is Raič (2019), Proposition 3.3's outer level-set identification.

theoremdefined in ProbabilityApproximation/ConvexGeometry/GaussianShell.lean

complete

theorem ProbabilityTheory.signedDistance_level_neg_eq_frontier_innerParallel
  {d : ℕ} {s : Set (EuclideanSpace ℝ (Fin d))} (hsne : s ≠ Set.univ)
  {t : ℝ} (ht : t < 0) :
  {x | ProbabilityTheory.setSignedDistance s x = t} =
    frontier (ProbabilityTheory.convexInnerParallel s (-t))

theorem ProbabilityTheory.signedDistance_level_neg_eq_frontier_innerParallel
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hsne : s ≠ Set.univ) {t : ℝ}
  (ht : t < 0) :
  {x |
      ProbabilityTheory.setSignedDistance
          s x =
        t} =
    frontier
      (ProbabilityTheory.convexInnerParallel
        s (-t))

A negative signed-distance level set is exactly the frontier of the corresponding inner
parallel set.  This is Raič (2019), Proposition 3.3's inner level-set identification.

theoremdefined in ProbabilityApproximation/ConvexGeometry/GaussianShell.lean

complete

theorem ProbabilityTheory.signedDistance_level_zero_eq_frontier {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} (hne : s.Nonempty)
  (hsne : s ≠ Set.univ) :
  {x | ProbabilityTheory.setSignedDistance s x = 0} = frontier s

theorem ProbabilityTheory.signedDistance_level_zero_eq_frontier
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hne : s.Nonempty)
  (hsne : s ≠ Set.univ) :
  {x |
      ProbabilityTheory.setSignedDistance
          s x =
        0} =
    frontier s

The zero signed-distance fiber is exactly the frontier of a nonempty proper set.

This is Proposition 3.3(4) of Raič (2019), printed p. 2844, with the positive and negative cases written separately to expose the exact outer-closure and open-ball conventions used by the setwise smoothing inequality.

Lemma2.4.3

Statement uses 2

Statement dependency previews

Preview

Lemma 2.1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Tagsbentkusgaussian-geometrysigned-distanceshellssource-raic-2019fidelity-exact-null-boundary-conventions

Outer and inner shells as signed-distance slabs. Let A\subsetneq\mathbb R^d be nonempty and convex, let \gamma_d=N(0,I_d), and let \varepsilon\ge0. The convex frontier is Gaussian-null, and \begin{aligned} \{x:d(x,\overline A)\le\varepsilon\}\setminus\overline A &=\delta_A^{-1}((0,\varepsilon]),\\ A\setminus\{x\in A:B(x,\varepsilon)\subseteq A\} &=A\cap\delta_A^{-1}((-\varepsilon,0]). \end{aligned} Consequently the omitted boundary has no effect on mass and \begin{aligned} \gamma_d\bigl(\{x:d(x,\overline A)\le\varepsilon\}\setminus A\bigr) &=\gamma_d\bigl(\delta_A^{-1}((0,\varepsilon])\bigr),\\ \gamma_d\bigl(A\setminus\{x\in A:B(x,\varepsilon)\subseteq A\}\bigr) &=\gamma_d\bigl(\delta_A^{-1}((-\varepsilon,0])\bigr). \end{aligned}

Lean code for Lemma2.4.3●5 theorems

theoremdefined in ProbabilityApproximation/ConvexGeometry/GaussianShell.lean

complete

theorem ProbabilityTheory.stdGaussian_frontier_eq_zero {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) :
  (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d)))
      (frontier s) =
    0

theorem ProbabilityTheory.stdGaussian_frontier_eq_zero
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) :
  (ProbabilityTheory.stdGaussian
        (EuclideanSpace ℝ (Fin d)))
      (frontier s) =
    0

The frontier of a convex Euclidean set has zero standard-Gaussian measure.

theoremdefined in ProbabilityApproximation/ConvexGeometry/GaussianShell.lean

complete

theorem ProbabilityTheory.outerShell_closed_eq_signedDistance_preimage_Ioc
  {d : ℕ} {s : Set (EuclideanSpace ℝ (Fin d))} (hne : s.Nonempty)
  {ε : ℝ} (hε : 0 ≤ ε) :
  Metric.cthickening ε (closure s) \ closure s =
    ProbabilityTheory.setSignedDistance s ⁻¹' Set.Ioc 0 ε

theorem ProbabilityTheory.outerShell_closed_eq_signedDistance_preimage_Ioc
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hne : s.Nonempty) {ε : ℝ}
  (hε : 0 ≤ ε) :
  Metric.cthickening ε (closure s) \
      closure s =
    ProbabilityTheory.setSignedDistance
        s ⁻¹'
      Set.Ioc 0 ε

For a nonempty set, the closed outer shell with its null boundary removed is exactly the
positive signed-distance slab `(0, ε]`.

theoremdefined in ProbabilityApproximation/ConvexGeometry/GaussianShell.lean

complete

theorem ProbabilityTheory.innerShell_eq_inter_signedDistance_preimage_Ioc
  {d : ℕ} {s : Set (EuclideanSpace ℝ (Fin d))} (hsne : s ≠ Set.univ)
  (ε : ℝ) :
  s \ ProbabilityTheory.convexInnerParallel s ε =
    s ∩ ProbabilityTheory.setSignedDistance s ⁻¹' Set.Ioc (-ε) 0

theorem ProbabilityTheory.innerShell_eq_inter_signedDistance_preimage_Ioc
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hsne : s ≠ Set.univ) (ε : ℝ) :
  s \
      ProbabilityTheory.convexInnerParallel
        s ε =
    s ∩
      ProbabilityTheory.setSignedDistance
          s ⁻¹'
        Set.Ioc (-ε) 0

For a proper set, the inner shell is exactly the part of the nonpositive signed-distance slab
which lies in the set.  The remaining points of the full slab are boundary points omitted by a
nonclosed set.

theoremdefined in ProbabilityApproximation/ConvexGeometry/GaussianShell.lean

complete

theorem ProbabilityTheory.stdGaussian_outer_shell_eq_signedDistance_slab {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} (hne : s.Nonempty)
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ} (hε : 0 ≤ ε) :
  (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d)))
      (Metric.cthickening ε (closure s) \ s) =
    (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d)))
      (ProbabilityTheory.setSignedDistance s ⁻¹' Set.Ioc 0 ε)

theorem ProbabilityTheory.stdGaussian_outer_shell_eq_signedDistance_slab
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hne : s.Nonempty)
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ}
  (hε : 0 ≤ ε) :
  (ProbabilityTheory.stdGaussian
        (EuclideanSpace ℝ (Fin d)))
      (Metric.cthickening ε (closure s) \
        s) =
    (ProbabilityTheory.stdGaussian
        (EuclideanSpace ℝ (Fin d)))
      (ProbabilityTheory.setSignedDistance
          s ⁻¹'
        Set.Ioc 0 ε)

The outer shell has exactly the standard-Gaussian mass of the positive signed-distance slab.
This is the set/measure input to Raič's coarea argument.

theoremdefined in ProbabilityApproximation/ConvexGeometry/GaussianShell.lean

complete

theorem ProbabilityTheory.stdGaussian_inner_shell_eq_signedDistance_slab {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} (hne : s.Nonempty)
  (hsne : s ≠ Set.univ) (hs : Convexity.IsConvexSet ℝ s) (ε : ℝ) :
  (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d)))
      (s \ ProbabilityTheory.convexInnerParallel s ε) =
    (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d)))
      (ProbabilityTheory.setSignedDistance s ⁻¹' Set.Ioc (-ε) 0)

theorem ProbabilityTheory.stdGaussian_inner_shell_eq_signedDistance_slab
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hne : s.Nonempty) (hsne : s ≠ Set.univ)
  (hs : Convexity.IsConvexSet ℝ s)
  (ε : ℝ) :
  (ProbabilityTheory.stdGaussian
        (EuclideanSpace ℝ (Fin d)))
      (s \
        ProbabilityTheory.convexInnerParallel
          s ε) =
    (ProbabilityTheory.stdGaussian
        (EuclideanSpace ℝ (Fin d)))
      (ProbabilityTheory.setSignedDistance
          s ⁻¹'
        Set.Ioc (-ε) 0)

The inner shell has exactly the standard-Gaussian mass of the nonpositive signed-distance
slab.  Boundary points added by passing from the shell to the full slab are Gaussian-null.

Raič (2019), introduces the signed-distance neighborhoods on printed pp. 2825--2826 and uses precisely these positive and negative slabs in the proof of Proposition 3.1, printed pp. 2844--2845, before applying the coarea formula. The formal identities retain equality boundaries and discharge the convex-frontier null set explicitly.

Theorem2.4.4

uses 0used by 1✓L∃∀N

Tagsbentkusgaussian-geometryaffine-slicingcoareasource-ball-1993source-raic-2019fidelity-normalized-affine-coarea

Normalized affine codimension-one slicing. Put \phi_d(x)=(2\pi)^{-d/2}e^{-\|x\|^2/2}. Then \gamma_d=\phi_d\,\lambda_d is standard Gaussian measure and \int\phi_d\,d\lambda_d=1. If v\ne0, p\in\mathbb R^d, and H_t=p+tv+v^\perp, then every measurable B\subseteq\mathbb R^d and every nonnegative measurable w satisfy \begin{aligned} \lambda_d(B) &=\|v\|\int_{\mathbb R}\mathcal H^{d-1}(B\cap H_t)\,dt,\\ \int_{\mathbb R^d}w\,d\lambda_d &=\|v\|\int_{\mathbb R}\int_{H_t}w\,d\mathcal H^{d-1}\,dt,\\ \gamma_d(B) &=\|v\|\int_{\mathbb R}\int_{B\cap H_t}\phi_d\,d\mathcal H^{d-1}\,dt. \end{aligned} The Hausdorff measure is normalized so that top-dimensional measure is Euclidean volume. Moreover, if u\in\mathbb R^{n+1} is a unit vector, then \int_{au+u^\perp}\phi_{n+1}(y)\,d\mathcal H^n(y) =\phi_1(a)\le1.

Lean code for Theorem2.4.4●7 theorems

theoremdefined in ProbabilityApproximation/ConvexGeometry/GaussianShell.lean

complete

theorem ProbabilityTheory.stdGaussian_eq_withDensity_standardGaussianDensityReal
  {d : ℕ} :
  ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d)) =
    MeasureTheory.volume.withDensity fun x =>
      ENNReal.ofReal (ProbabilityTheory.standardGaussianDensityReal x)

theorem ProbabilityTheory.stdGaussian_eq_withDensity_standardGaussianDensityReal
  {d : ℕ} :
  ProbabilityTheory.stdGaussian
      (EuclideanSpace ℝ (Fin d)) =
    MeasureTheory.volume.withDensity
      fun x =>
      ENNReal.ofReal
        (ProbabilityTheory.standardGaussianDensityReal
          x)

Standard Gaussian measure is Euclidean volume weighted by Ball's radial density.  This is the
measure-theoretic density bridge required before applying coarea to signed distance.

theoremdefined in ProbabilityApproximation/ConvexGeometry/GaussianShell.lean

complete

theorem ProbabilityTheory.lintegral_standardGaussianDensityReal_eq_one {d : ℕ} :
  ∫⁻ (x : EuclideanSpace ℝ (Fin d)),
      ENNReal.ofReal (ProbabilityTheory.standardGaussianDensityReal x) =
    1

theorem ProbabilityTheory.lintegral_standardGaussianDensityReal_eq_one
  {d : ℕ} :
  ∫⁻ (x : EuclideanSpace ℝ (Fin d)),
      ENNReal.ofReal
        (ProbabilityTheory.standardGaussianDensityReal
          x) =
    1

Ball's radial density is normalized to total mass one in every Euclidean dimension.

theoremdefined in ProbabilityApproximation/ConvexGeometry/GaussianShell.lean

complete

theorem ProbabilityTheory.euclideanVolume_eq_lintegral_codimOneSections {d : ℕ}
  (p v : EuclideanSpace ℝ (Fin d)) (hv : v ≠ 0)
  {t : Set (EuclideanSpace ℝ (Fin d))} (ht : MeasurableSet t) :
  MeasureTheory.volume t =
    ‖v‖ₑ *
      ∫⁻ (x : ℝ),
        (MeasureTheory.Measure.euclideanHausdorffMeasure (d - 1))
          (t ∩ ↑(AffineSubspace.mk' (x • v + p) (ℝ ∙ v)ᗮ))

theorem ProbabilityTheory.euclideanVolume_eq_lintegral_codimOneSections
  {d : ℕ} (p v : EuclideanSpace ℝ (Fin d))
  (hv : v ≠ 0)
  {t : Set (EuclideanSpace ℝ (Fin d))}
  (ht : MeasurableSet t) :
  MeasureTheory.volume t =
    ‖v‖ₑ *
      ∫⁻ (x : ℝ),
        (MeasureTheory.Measure.euclideanHausdorffMeasure
            (d - 1))
          (t ∩
            ↑(AffineSubspace.mk'
                (x • v + p) (ℝ ∙ v)ᗮ))

Exact codimension-one affine slicing of Euclidean volume.  This is the affine base case of
the coarea cluster: the parameter `x` runs along `v`, while the fiber is the perpendicular affine
hyperplane through `x • v + p`.  The normalization uses Mathlib's Euclidean Hausdorff measure, so
top-dimensional measure is exactly `volume` and no dimension-dependent scale factor is hidden.

theoremdefined in ProbabilityApproximation/ConvexGeometry/GaussianShell.lean

complete

theorem ProbabilityTheory.lintegral_eq_lintegral_codimOneSections {d : ℕ}
  (p : EuclideanSpace ℝ (Fin d)) {v : EuclideanSpace ℝ (Fin d)}
  (hv : v ≠ 0) (w : EuclideanSpace ℝ (Fin d) → ENNReal)
  (hw : Measurable w) :
  ∫⁻ (y : EuclideanSpace ℝ (Fin d)), w y =
    ‖v‖ₑ *
      ∫⁻ (x : ℝ),
        ∫⁻ (y : EuclideanSpace ℝ (Fin d)) in
          ↑(AffineSubspace.mk' (x • v + p) (ℝ ∙ v)ᗮ),
          w y ∂MeasureTheory.Measure.euclideanHausdorffMeasure (d - 1)

theorem ProbabilityTheory.lintegral_eq_lintegral_codimOneSections
  {d : ℕ} (p : EuclideanSpace ℝ (Fin d))
  {v : EuclideanSpace ℝ (Fin d)}
  (hv : v ≠ 0)
  (w : EuclideanSpace ℝ (Fin d) → ENNReal)
  (hw : Measurable w) :
  ∫⁻ (y : EuclideanSpace ℝ (Fin d)), w y =
    ‖v‖ₑ *
      ∫⁻ (x : ℝ),
        ∫⁻ (y :
          EuclideanSpace ℝ (Fin d)) in
          ↑(AffineSubspace.mk' (x • v + p)
              (ℝ ∙ v)ᗮ),
          w
            y ∂MeasureTheory.Measure.euclideanHausdorffMeasure
            (d - 1)

Weighted affine codimension-one coarea.  This strengthens the set-slicing identity to every
nonnegative measurable density by constructing the measurable family of Euclidean surface
measures on parallel fibers and integrating it with the Giry bind operation.

theoremdefined in ProbabilityApproximation/ConvexGeometry/GaussianShell.lean

complete

theorem ProbabilityTheory.stdGaussian_apply_eq_lintegral_codimOneSections
  {d : ℕ} (p : EuclideanSpace ℝ (Fin d)) {v : EuclideanSpace ℝ (Fin d)}
  (hv : v ≠ 0) {t : Set (EuclideanSpace ℝ (Fin d))}
  (ht : MeasurableSet t) :
  (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d))) t =
    ‖v‖ₑ *
      ∫⁻ (x : ℝ),
        ∫⁻ (y : EuclideanSpace ℝ (Fin d)) in
          t ∩ ↑(AffineSubspace.mk' (x • v + p) (ℝ ∙ v)ᗮ),
          ENNReal.ofReal
            (ProbabilityTheory.standardGaussianDensityReal
              y) ∂MeasureTheory.Measure.euclideanHausdorffMeasure
            (d - 1)

theorem ProbabilityTheory.stdGaussian_apply_eq_lintegral_codimOneSections
  {d : ℕ} (p : EuclideanSpace ℝ (Fin d))
  {v : EuclideanSpace ℝ (Fin d)}
  (hv : v ≠ 0)
  {t : Set (EuclideanSpace ℝ (Fin d))}
  (ht : MeasurableSet t) :
  (ProbabilityTheory.stdGaussian
        (EuclideanSpace ℝ (Fin d)))
      t =
    ‖v‖ₑ *
      ∫⁻ (x : ℝ),
        ∫⁻ (y :
          EuclideanSpace ℝ (Fin d)) in
          t ∩
            ↑(AffineSubspace.mk'
                (x • v + p) (ℝ ∙ v)ᗮ),
          ENNReal.ofReal
            (ProbabilityTheory.standardGaussianDensityReal
              y) ∂MeasureTheory.Measure.euclideanHausdorffMeasure
            (d - 1)

Standard Gaussian mass disintegrates exactly into Gaussian-weighted Euclidean surface
integrals over any family of parallel affine hyperplanes.

theoremdefined in ProbabilityApproximation/ConvexGeometry/GaussianShell.lean

complete

theorem ProbabilityTheory.standardGaussianDensity_affineHyperplane {n : ℕ}
  (u : EuclideanSpace ℝ (Fin (n + 1))) (hu : ‖u‖ = 1) (a : ℝ) :
  ∫⁻ (y : EuclideanSpace ℝ (Fin (n + 1))) in
      ↑(AffineSubspace.mk' (a • u) (ℝ ∙ u)ᗮ),
      ENNReal.ofReal
        (ProbabilityTheory.standardGaussianDensityReal
          y) ∂MeasureTheory.Measure.euclideanHausdorffMeasure n =
    ENNReal.ofReal (ProbabilityTheory.gaussianPDFReal 0 1 a)

theorem ProbabilityTheory.standardGaussianDensity_affineHyperplane
  {n : ℕ}
  (u : EuclideanSpace ℝ (Fin (n + 1)))
  (hu : ‖u‖ = 1) (a : ℝ) :
  ∫⁻ (y :
      EuclideanSpace ℝ (Fin (n + 1))) in
      ↑(AffineSubspace.mk' (a • u)
          (ℝ ∙ u)ᗮ),
      ENNReal.ofReal
        (ProbabilityTheory.standardGaussianDensityReal
          y) ∂MeasureTheory.Measure.euclideanHausdorffMeasure
        n =
    ENNReal.ofReal
      (ProbabilityTheory.gaussianPDFReal 0
        1 a)

The Gaussian surface integral over an affine hyperplane perpendicular to a unit vector is
the one-dimensional standard-Gaussian density at its signed offset.

theoremdefined in ProbabilityApproximation/ConvexGeometry/GaussianShell.lean

complete

theorem ProbabilityTheory.standardGaussianDensity_affineHyperplane_le_one
  {n : ℕ} (u : EuclideanSpace ℝ (Fin (n + 1))) (hu : ‖u‖ = 1) (a : ℝ) :
  ∫⁻ (y : EuclideanSpace ℝ (Fin (n + 1))) in
      ↑(AffineSubspace.mk' (a • u) (ℝ ∙ u)ᗮ),
      ENNReal.ofReal
        (ProbabilityTheory.standardGaussianDensityReal
          y) ∂MeasureTheory.Measure.euclideanHausdorffMeasure n ≤
    1

theorem ProbabilityTheory.standardGaussianDensity_affineHyperplane_le_one
  {n : ℕ}
  (u : EuclideanSpace ℝ (Fin (n + 1)))
  (hu : ‖u‖ = 1) (a : ℝ) :
  ∫⁻ (y :
      EuclideanSpace ℝ (Fin (n + 1))) in
      ↑(AffineSubspace.mk' (a • u)
          (ℝ ∙ u)ᗮ),
      ENNReal.ofReal
        (ProbabilityTheory.standardGaussianDensityReal
          y) ∂MeasureTheory.Measure.euclideanHausdorffMeasure
        n ≤
    1

Every affine hyperplane has standard-Gaussian surface content at most one.

Ball (1993) uses codimension-one projections and Gaussian surface integrals in the proof of Theorem 4, printed pp. 415--419. Raič (2019) states the general area/coarea input as Proposition 3.2 and Corollary 3.1, printed pp. 2843--2844, and applies it in Proposition 3.1, printed pp. 2843--2845. This node supplies the Mathlib-normalized affine specialization; the nonlinear coarea formula for signed distance is recorded in the next node.

Theorem2.4.5

uses 0

Used by 2

Reverse dependency previews

Preview

Theorem 2.4.6

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagsgeometric-measure-theoryarea-formulasource-raic-2019source-federer-1969fidelity-injective-weighted-specialization

Weighted area formula for an injective Lipschitz chart. Let U and V be finite-dimensional real inner-product spaces, put m=\dim U, and let \varphi:S\subseteq U\to V be Lipschitz and one-to-one on a measurable set S. For every nonnegative measurable weight g:V\to[0,\infty], \int_{\varphi(S)}g(y)\,d\mathcal H^m(y) =\int_S J_m(D\varphi|_S)(x)\,g(\varphi(x))\,dx. Here D\varphi|_S is the within derivative and J_m is its absolute m-dimensional Jacobian. In particular, if a Lipschitz inverse chart \varphi has a linear left inverse P on S, so that P(\varphi(x))=x, the same identity applies without separately assuming full rank: differentiating the composition makes D\varphi|_S injective almost everywhere.

Lean code for Theorem2.4.5●2 theorems

theoremdefined in ProbabilityApproximation/ConvexGeometry/ScalarCoarea.lean

complete

theorem ProbabilityTheory.lintegral_image_eq_lintegral_normDet_fderivWithin_mul_of_lipschitzOnWith.{u_1,
    u_2}
  {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U]
  [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V]
  [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace U]
  [BorelSpace U] [MeasurableSpace V] [BorelSpace V] {C : NNReal}
  {f : U → V} {s : Set U} (hs : MeasurableSet s)
  (hf : LipschitzOnWith C f s) (hfinj : Set.InjOn f s)
  (hf'inj :
    ∀ᵐ (x : U) ∂MeasureTheory.volume.restrict s,
      Function.Injective ⇑(fderivWithin ℝ f s x))
  (g : V → ENNReal) (hg : Measurable g) :
  ∫⁻ (y : V) in f '' s,
      g
        y ∂MeasureTheory.Measure.euclideanHausdorffMeasure
        (Module.finrank ℝ U) =
    ∫⁻ (x : U) in s,
      ENNReal.ofReal (↑(fderivWithin ℝ f s x)).normDet * g (f x)

theorem ProbabilityTheory.lintegral_image_eq_lintegral_normDet_fderivWithin_mul_of_lipschitzOnWith.{u_1,
    u_2}
  {U : Type u_1} {V : Type u_2}
  [NormedAddCommGroup U]
  [InnerProductSpace ℝ U]
  [FiniteDimensional ℝ U]
  [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace U] [BorelSpace U]
  [MeasurableSpace V] [BorelSpace V]
  {C : NNReal} {f : U → V} {s : Set U}
  (hs : MeasurableSet s)
  (hf : LipschitzOnWith C f s)
  (hfinj : Set.InjOn f s)
  (hf'inj :
    ∀ᵐ (x :
      U) ∂MeasureTheory.volume.restrict s,
      Function.Injective
        ⇑(fderivWithin ℝ f s x))
  (g : V → ENNReal) (hg : Measurable g) :
  ∫⁻ (y : V) in f '' s,
      g
        y ∂MeasureTheory.Measure.euclideanHausdorffMeasure
        (Module.finrank ℝ U) =
    ∫⁻ (x : U) in s,
      ENNReal.ofReal
          (↑(fderivWithin ℝ f s
                x)).normDet *
        g (f x)

Weighted lower-dimensional area formula for an injective Lipschitz parameterization whose
within derivative has full rank almost everywhere.  Rademacher's theorem removes the null
nondifferentiability set; Lipschitz Hausdorff distortion removes its image.

theoremdefined in ProbabilityApproximation/ConvexGeometry/ScalarCoarea.lean

complete

theorem ProbabilityTheory.lintegral_image_eq_lintegral_normDet_fderivWithin_mul_of_comp_eq_id.{u_1,
    u_2}
  {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U]
  [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V]
  [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace U]
  [BorelSpace U] [MeasurableSpace V] [BorelSpace V] {C : NNReal}
  {φ : U → V} {s : Set U} (hs : MeasurableSet s)
  (hφ : LipschitzOnWith C φ s) (hφinj : Set.InjOn φ s) (P : V →L[ℝ] U)
  (heq : Set.EqOn id (fun z => P (φ z)) s) (g : V → ENNReal)
  (hg : Measurable g) :
  ∫⁻ (y : V) in φ '' s,
      g
        y ∂MeasureTheory.Measure.euclideanHausdorffMeasure
        (Module.finrank ℝ U) =
    ∫⁻ (z : U) in s,
      ENNReal.ofReal (↑(fderivWithin ℝ φ s z)).normDet * g (φ z)

theorem ProbabilityTheory.lintegral_image_eq_lintegral_normDet_fderivWithin_mul_of_comp_eq_id.{u_1,
    u_2}
  {U : Type u_1} {V : Type u_2}
  [NormedAddCommGroup U]
  [InnerProductSpace ℝ U]
  [FiniteDimensional ℝ U]
  [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace U] [BorelSpace U]
  [MeasurableSpace V] [BorelSpace V]
  {C : NNReal} {φ : U → V} {s : Set U}
  (hs : MeasurableSet s)
  (hφ : LipschitzOnWith C φ s)
  (hφinj : Set.InjOn φ s) (P : V →L[ℝ] U)
  (heq : Set.EqOn id (fun z => P (φ z)) s)
  (g : V → ENNReal) (hg : Measurable g) :
  ∫⁻ (y : V) in φ '' s,
      g
        y ∂MeasureTheory.Measure.euclideanHausdorffMeasure
        (Module.finrank ℝ U) =
    ∫⁻ (z : U) in s,
      ENNReal.ofReal
          (↑(fderivWithin ℝ φ s
                z)).normDet *
        g (φ z)

Weighted lower-dimensional area formula for an injective Lipschitz right-inverse chart.  This
is the projection-chart interface used in Ball's convex-boundary argument.

This is the injective weighted specialization of Corollary 3.2.32 in Federer (1969). Raič (2019) records the area formula as Proposition 3.2, printed pp. 2843--2844, and uses it both for coarea and for the boundary projection estimate.

Theorem2.4.6

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 2.4.7

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagsgeometric-measure-theorycoareasource-raic-2019source-federer-1969fidelity-measurable-ennreal-weighted-formula

Weighted scalar coarea formula. Let d\in\mathbb N, let f:\mathbb R^d\to\mathbb R be globally Lipschitz, and let w:\mathbb R^d\to[0,\infty] be Borel measurable. Put J_f(x)=\|Df(x)\|, \qquad Q_{f,w}(t)=\int_{f^{-1}(\{t\})}w(x)\,d\mathcal H^{d-1}(x), where Df(x) is taken to be zero at points where f is not differentiable and d-1 is the natural-number predecessor. Then \int_{\mathbb R^d}J_f(x)w(x)\,dx =\int_{\mathbb R}Q_{f,w}(t)\,dt. For every a,b\in\mathbb R, the exact half-open slab form is \int_{f^{-1}((a,b])}J_f(x)w(x)\,dx =\int_{(a,b]}Q_{f,w}(t)\,dt. If \|Df(x)\|=1 for Lebesgue-almost every x, this reduces to \int_{f^{-1}((a,b])}w(x)\,dx =\int_{(a,b]}Q_{f,w}(t)\,dt.

Lean code for Theorem2.4.6●8 declarations

defdefined in ProbabilityApproximation/ConvexGeometry/ScalarCoarea.lean

complete

def ProbabilityTheory.scalarJacobian {d : ℕ}
  (f : EuclideanSpace ℝ (Fin d) → ℝ) (x : EuclideanSpace ℝ (Fin d)) :
  ENNReal

def ProbabilityTheory.scalarJacobian {d : ℕ}
  (f : EuclideanSpace ℝ (Fin d) → ℝ)
  (x : EuclideanSpace ℝ (Fin d)) : ENNReal

The scalar Jacobian of a map from Euclidean space to the real line.  At points where the map
is not differentiable, Mathlib's `fderiv` is definitionally zero.

defdefined in ProbabilityApproximation/ConvexGeometry/ScalarCoarea.lean

complete

def ProbabilityTheory.scalarCoareaFiber {d : ℕ}
  (f : EuclideanSpace ℝ (Fin d) → ℝ)
  (w : EuclideanSpace ℝ (Fin d) → ENNReal) (t : ℝ) : ENNReal

def ProbabilityTheory.scalarCoareaFiber
  {d : ℕ}
  (f : EuclideanSpace ℝ (Fin d) → ℝ)
  (w : EuclideanSpace ℝ (Fin d) → ENNReal)
  (t : ℝ) : ENNReal

The weighted Euclidean codimension-one content of one level fiber.

defdefined in ProbabilityApproximation/ConvexGeometry/ScalarCoarea.lean

complete

def ProbabilityTheory.ScalarCoareaFormula {d : ℕ}
  (f : EuclideanSpace ℝ (Fin d) → ℝ) : Prop

def ProbabilityTheory.ScalarCoareaFormula
  {d : ℕ}
  (f : EuclideanSpace ℝ (Fin d) → ℝ) :
  Prop

Federer's weighted scalar coarea identity, packaged as a reusable property of a scalar map.

theoremdefined in ProbabilityApproximation/ConvexGeometry/ScalarCoarea.lean

complete

theorem ProbabilityTheory.LipschitzWith.scalarCoareaFormula {d : ℕ} {C : NNReal}
  {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : LipschitzWith C f) :
  ProbabilityTheory.ScalarCoareaFormula f

theorem ProbabilityTheory.LipschitzWith.scalarCoareaFormula
  {d : ℕ} {C : NNReal}
  {f : EuclideanSpace ℝ (Fin d) → ℝ}
  (hf : LipschitzWith C f) :
  ProbabilityTheory.ScalarCoareaFormula f

Every globally Lipschitz scalar map on a finite-dimensional Euclidean space satisfies
Federer's weighted scalar coarea formula.

theoremdefined in ProbabilityApproximation/ConvexGeometry/ScalarCoarea.lean

complete

theorem ProbabilityTheory.ScalarCoareaFormula.setLIntegral_slab {d : ℕ}
  {C : NNReal} {f : EuclideanSpace ℝ (Fin d) → ℝ}
  (hcoarea : ProbabilityTheory.ScalarCoareaFormula f)
  (hf : LipschitzWith C f) (w : EuclideanSpace ℝ (Fin d) → ENNReal)
  (hw : Measurable w) (a b : ℝ) :
  ∫⁻ (x : EuclideanSpace ℝ (Fin d)) in f ⁻¹' Set.Ioc a b,
      ProbabilityTheory.scalarJacobian f x * w x =
    ∫⁻ (t : ℝ) in Set.Ioc a b, ProbabilityTheory.scalarCoareaFiber f w t

theorem ProbabilityTheory.ScalarCoareaFormula.setLIntegral_slab
  {d : ℕ} {C : NNReal}
  {f : EuclideanSpace ℝ (Fin d) → ℝ}
  (hcoarea :
    ProbabilityTheory.ScalarCoareaFormula
      f)
  (hf : LipschitzWith C f)
  (w : EuclideanSpace ℝ (Fin d) → ENNReal)
  (hw : Measurable w) (a b : ℝ) :
  ∫⁻ (x : EuclideanSpace ℝ (Fin d)) in
      f ⁻¹' Set.Ioc a b,
      ProbabilityTheory.scalarJacobian f
          x *
        w x =
    ∫⁻ (t : ℝ) in Set.Ioc a b,
      ProbabilityTheory.scalarCoareaFiber
        f w t

Federer's weighted scalar coarea identity implies its exact half-open slab form.

theoremdefined in ProbabilityApproximation/ConvexGeometry/ScalarCoarea.lean

complete

theorem ProbabilityTheory.ScalarCoareaFormula.setLIntegral_slab_of_ae_norm_fderiv_eq_one
  {d : ℕ} {C : NNReal} {f : EuclideanSpace ℝ (Fin d) → ℝ}
  (hcoarea : ProbabilityTheory.ScalarCoareaFormula f)
  (hf : LipschitzWith C f) (w : EuclideanSpace ℝ (Fin d) → ENNReal)
  (hw : Measurable w) (a b : ℝ)
  (hjac : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), ‖fderiv ℝ f x‖ = 1) :
  ∫⁻ (x : EuclideanSpace ℝ (Fin d)) in f ⁻¹' Set.Ioc a b, w x =
    ∫⁻ (t : ℝ) in Set.Ioc a b, ProbabilityTheory.scalarCoareaFiber f w t

theorem ProbabilityTheory.ScalarCoareaFormula.setLIntegral_slab_of_ae_norm_fderiv_eq_one
  {d : ℕ} {C : NNReal}
  {f : EuclideanSpace ℝ (Fin d) → ℝ}
  (hcoarea :
    ProbabilityTheory.ScalarCoareaFormula
      f)
  (hf : LipschitzWith C f)
  (w : EuclideanSpace ℝ (Fin d) → ENNReal)
  (hw : Measurable w) (a b : ℝ)
  (hjac :
    ∀ᵐ (x : EuclideanSpace ℝ (Fin d)),
      ‖fderiv ℝ f x‖ = 1) :
  ∫⁻ (x : EuclideanSpace ℝ (Fin d)) in
      f ⁻¹' Set.Ioc a b, w x =
    ∫⁻ (t : ℝ) in Set.Ioc a b,
      ProbabilityTheory.scalarCoareaFiber
        f w t

For a Lipschitz scalar map with almost-everywhere unit derivative norm, scalar coarea reduces
on a slab to unweighted volume disintegration over its level fibers.

theoremdefined in ProbabilityApproximation/ConvexGeometry/ScalarCoarea.lean

complete

theorem ProbabilityTheory.LipschitzWith.scalarCoarea_setLIntegral_slab {d : ℕ}
  {C : NNReal} {f : EuclideanSpace ℝ (Fin d) → ℝ}
  (hf : LipschitzWith C f) (w : EuclideanSpace ℝ (Fin d) → ENNReal)
  (hw : Measurable w) (a b : ℝ) :
  ∫⁻ (x : EuclideanSpace ℝ (Fin d)) in f ⁻¹' Set.Ioc a b,
      ProbabilityTheory.scalarJacobian f x * w x =
    ∫⁻ (t : ℝ) in Set.Ioc a b, ProbabilityTheory.scalarCoareaFiber f w t

theorem ProbabilityTheory.LipschitzWith.scalarCoarea_setLIntegral_slab
  {d : ℕ} {C : NNReal}
  {f : EuclideanSpace ℝ (Fin d) → ℝ}
  (hf : LipschitzWith C f)
  (w : EuclideanSpace ℝ (Fin d) → ENNReal)
  (hw : Measurable w) (a b : ℝ) :
  ∫⁻ (x : EuclideanSpace ℝ (Fin d)) in
      f ⁻¹' Set.Ioc a b,
      ProbabilityTheory.scalarJacobian f
          x *
        w x =
    ∫⁻ (t : ℝ) in Set.Ioc a b,
      ProbabilityTheory.scalarCoareaFiber
        f w t

Direct weighted slab form of scalar coarea for a globally Lipschitz map.

theoremdefined in ProbabilityApproximation/ConvexGeometry/ScalarCoarea.lean

complete

theorem ProbabilityTheory.LipschitzWith.setLIntegral_slab_of_ae_norm_fderiv_eq_one
  {d : ℕ} {C : NNReal} {f : EuclideanSpace ℝ (Fin d) → ℝ}
  (hf : LipschitzWith C f) (w : EuclideanSpace ℝ (Fin d) → ENNReal)
  (hw : Measurable w) (a b : ℝ)
  (hjac : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), ‖fderiv ℝ f x‖ = 1) :
  ∫⁻ (x : EuclideanSpace ℝ (Fin d)) in f ⁻¹' Set.Ioc a b, w x =
    ∫⁻ (t : ℝ) in Set.Ioc a b, ProbabilityTheory.scalarCoareaFiber f w t

theorem ProbabilityTheory.LipschitzWith.setLIntegral_slab_of_ae_norm_fderiv_eq_one
  {d : ℕ} {C : NNReal}
  {f : EuclideanSpace ℝ (Fin d) → ℝ}
  (hf : LipschitzWith C f)
  (w : EuclideanSpace ℝ (Fin d) → ENNReal)
  (hw : Measurable w) (a b : ℝ)
  (hjac :
    ∀ᵐ (x : EuclideanSpace ℝ (Fin d)),
      ‖fderiv ℝ f x‖ = 1) :
  ∫⁻ (x : EuclideanSpace ℝ (Fin d)) in
      f ⁻¹' Set.Ioc a b, w x =
    ∫⁻ (t : ℝ) in Set.Ioc a b,
      ProbabilityTheory.scalarCoareaFiber
        f w t

Direct unit-gradient slab disintegration for a globally Lipschitz scalar map.

Corollary 3.2.32 of Federer (1969) supplies the area/coarea theorem. Raič (2019) states the measurable-fiber theorem as Proposition 3.2, printed pp. 2843--2844, and its scalar coarea specialization as Corollary 3.1, printed p. 2844. Raič combines it with the almost-everywhere unit gradient of signed distance in Proposition 3.3 and the proof of Proposition 3.1, printed pp. 2844--2845. The formal result uses nonnegative extended-valued weights, includes the exact (a,b] convention, and also proves the dimension-zero endpoint under the displayed predecessor convention.

Theorem2.4.7

Statement uses 3

Statement dependency previews

Preview

Lemma 2.4.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Tagsbentkusgaussian-geometrysigned-distancecoareaperimeter-reductionsource-raic-2019fidelity-exact-half-open-profile-identities

Signed-distance coarea identities for Gaussian shell profiles. Let A\subsetneq\mathbb R^d be nonempty and convex, put \phi_d(x)=(2\pi)^{-d/2}e^{-\|x\|^2/2}, \qquad P_\gamma(C)=\int_{\partial C}\phi_d(x)\,d\mathcal H^{d-1}(x), where \mathcal H^{d-1} is normalized so that top-dimensional Hausdorff measure is Euclidean volume. For t>0 and t<0, respectively, define p_A^+(t)=P_\gamma\!\left(\{x:d(x,\overline A)\le t\}\right), \qquad p_A^-(t)=P_\gamma\!\left(\{x:B(x,-t)\subseteq A\}\right), with open balls in the inner parallel set. If \delta_A is signed distance, then \begin{aligned} p_A^+(t)&=\int_{\{x:\delta_A(x)=t\}}\phi_d(x)\,d\mathcal H^{d-1}(x) && (t>0),\\ p_A^-(t)&=\int_{\{x:\delta_A(x)=t\}}\phi_d(x)\,d\mathcal H^{d-1}(x) && (t<0). \end{aligned} Consequently, for every \varepsilon\ge0, the exact half-open disintegrations are \begin{aligned} \gamma_d\!\left(\{x:d(x,\overline A)\le\varepsilon\}\setminus A\right) &=\int_{(0,\varepsilon]}p_A^+(t)\,dt,\\ \gamma_d\!\left(A\setminus\{x:B(x,\varepsilon)\subseteq A\}\right) &=\int_{(-\varepsilon,0]}p_A^-(t)\,dt. \end{aligned} In particular, if every convex C\subseteq\mathbb R^d satisfies P_\gamma(C)\le K_d for K_d=4d^{1/4}, then each of these two shell masses is at most K_d\varepsilon.

Lean code for Theorem2.4.7●9 declarations

defdefined in ProbabilityApproximation/ConvexGeometry/GaussianShell.lean

complete

def ProbabilityTheory.standardGaussianBoundaryContent {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d))) : ENNReal

def ProbabilityTheory.standardGaussianBoundaryContent
  {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d))) :
  ENNReal

The Gaussian-weighted codimension-one Hausdorff content of a frontier.  Ball's Theorem 4 is
the bound `standardGaussianBoundaryContent s ≤ 4 * d^(1/4)` for convex bodies in dimension at
least two.

defdefined in ProbabilityApproximation/ConvexGeometry/GaussianShell.lean

complete

def ProbabilityTheory.outerGaussianBoundaryProfile {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d))) (t : ℝ) : ENNReal

def ProbabilityTheory.outerGaussianBoundaryProfile
  {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d)))
  (t : ℝ) : ENNReal

The outer parallel-frontier profile occurring in Raič's coarea formula.

defdefined in ProbabilityApproximation/ConvexGeometry/GaussianShell.lean

complete

def ProbabilityTheory.innerGaussianBoundaryProfile {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d))) (t : ℝ) : ENNReal

def ProbabilityTheory.innerGaussianBoundaryProfile
  {d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d)))
  (t : ℝ) : ENNReal

The inner parallel-frontier profile occurring in Raič's coarea formula.

theoremdefined in ProbabilityApproximation/ConvexGeometry/GaussianShell.lean

complete

theorem ProbabilityTheory.outerGaussianBoundaryProfile_eq_levelLIntegral {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} (hne : s.Nonempty)
  (hs : Convexity.IsConvexSet ℝ s) {t : ℝ} (ht : 0 < t) :
  ProbabilityTheory.outerGaussianBoundaryProfile s t =
    ∫⁻ (x : EuclideanSpace ℝ (Fin d)) in
      {x | ProbabilityTheory.setSignedDistance s x = t},
      ENNReal.ofReal
        (ProbabilityTheory.standardGaussianDensityReal
          x) ∂MeasureTheory.Measure.euclideanHausdorffMeasure (d - 1)

theorem ProbabilityTheory.outerGaussianBoundaryProfile_eq_levelLIntegral
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hne : s.Nonempty)
  (hs : Convexity.IsConvexSet ℝ s) {t : ℝ}
  (ht : 0 < t) :
  ProbabilityTheory.outerGaussianBoundaryProfile
      s t =
    ∫⁻ (x : EuclideanSpace ℝ (Fin d)) in
      {x |
        ProbabilityTheory.setSignedDistance
            s x =
          t},
      ENNReal.ofReal
        (ProbabilityTheory.standardGaussianDensityReal
          x) ∂MeasureTheory.Measure.euclideanHausdorffMeasure
        (d - 1)

At a positive level, the outer boundary profile is the Gaussian-weighted Hausdorff integral
over the corresponding signed-distance fiber.

theoremdefined in ProbabilityApproximation/ConvexGeometry/GaussianShell.lean

complete

theorem ProbabilityTheory.innerGaussianBoundaryProfile_eq_levelLIntegral {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} (hsne : s ≠ Set.univ) {t : ℝ}
  (ht : t < 0) :
  ProbabilityTheory.innerGaussianBoundaryProfile s t =
    ∫⁻ (x : EuclideanSpace ℝ (Fin d)) in
      {x | ProbabilityTheory.setSignedDistance s x = t},
      ENNReal.ofReal
        (ProbabilityTheory.standardGaussianDensityReal
          x) ∂MeasureTheory.Measure.euclideanHausdorffMeasure (d - 1)

theorem ProbabilityTheory.innerGaussianBoundaryProfile_eq_levelLIntegral
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hsne : s ≠ Set.univ) {t : ℝ}
  (ht : t < 0) :
  ProbabilityTheory.innerGaussianBoundaryProfile
      s t =
    ∫⁻ (x : EuclideanSpace ℝ (Fin d)) in
      {x |
        ProbabilityTheory.setSignedDistance
            s x =
          t},
      ENNReal.ofReal
        (ProbabilityTheory.standardGaussianDensityReal
          x) ∂MeasureTheory.Measure.euclideanHausdorffMeasure
        (d - 1)

At a negative level, the inner boundary profile is the Gaussian-weighted Hausdorff integral
over the corresponding signed-distance fiber.

theoremdefined in ProbabilityApproximation/ConvexGeometry/GaussianShellCoarea.lean

complete

theorem ProbabilityTheory.stdGaussian_outer_shell_eq_lintegral_outerGaussianBoundaryProfile
  {d : ℕ} {s : Set (EuclideanSpace ℝ (Fin d))} (hne : s.Nonempty)
  (hsne : s ≠ Set.univ) (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ}
  (hε : 0 ≤ ε) :
  (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d)))
      (Metric.cthickening ε (closure s) \ s) =
    ∫⁻ (t : ℝ) in Set.Ioc 0 ε,
      ProbabilityTheory.outerGaussianBoundaryProfile s t

theorem ProbabilityTheory.stdGaussian_outer_shell_eq_lintegral_outerGaussianBoundaryProfile
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hne : s.Nonempty) (hsne : s ≠ Set.univ)
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ}
  (hε : 0 ≤ ε) :
  (ProbabilityTheory.stdGaussian
        (EuclideanSpace ℝ (Fin d)))
      (Metric.cthickening ε (closure s) \
        s) =
    ∫⁻ (t : ℝ) in Set.Ioc 0 ε,
      ProbabilityTheory.outerGaussianBoundaryProfile
        s t

The outer Gaussian shell is the scalar-coarea integral of the outer parallel-frontier
profile.  This is Raič's positive signed-distance disintegration with Mathlib's normalized
Euclidean Hausdorff measure.

theoremdefined in ProbabilityApproximation/ConvexGeometry/GaussianShellCoarea.lean

complete

theorem ProbabilityTheory.stdGaussian_inner_shell_eq_lintegral_innerGaussianBoundaryProfile
  {d : ℕ} {s : Set (EuclideanSpace ℝ (Fin d))} (hne : s.Nonempty)
  (hsne : s ≠ Set.univ) (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ}
  (_hε : 0 ≤ ε) :
  (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d)))
      (s \ ProbabilityTheory.convexInnerParallel s ε) =
    ∫⁻ (t : ℝ) in Set.Ioc (-ε) 0,
      ProbabilityTheory.innerGaussianBoundaryProfile s t

theorem ProbabilityTheory.stdGaussian_inner_shell_eq_lintegral_innerGaussianBoundaryProfile
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hne : s.Nonempty) (hsne : s ≠ Set.univ)
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ}
  (_hε : 0 ≤ ε) :
  (ProbabilityTheory.stdGaussian
        (EuclideanSpace ℝ (Fin d)))
      (s \
        ProbabilityTheory.convexInnerParallel
          s ε) =
    ∫⁻ (t : ℝ) in Set.Ioc (-ε) 0,
      ProbabilityTheory.innerGaussianBoundaryProfile
        s t

The inner Gaussian shell is the scalar-coarea integral of the negative parallel-frontier
profile.  The integration variable retains the signed-distance convention `t ∈ (-ε, 0]`.

defdefined in ProbabilityApproximation/ConvexGeometry/GaussianShell.lean

complete

def ProbabilityTheory.ballGaussianPerimeterConstant (d : ℕ) : ℝ

def ProbabilityTheory.ballGaussianPerimeterConstant
  (d : ℕ) : ℝ

Ball's dimension-dependent Gaussian-perimeter constant.

theoremdefined in ProbabilityApproximation/ConvexGeometry/GaussianShellCoarea.lean

complete

theorem ProbabilityTheory.stdGaussian_shell_pair_le_ball_of_boundaryContent
  {d : ℕ} {s : Set (EuclideanSpace ℝ (Fin d))} (hne : s.Nonempty)
  (hsne : s ≠ Set.univ) (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ}
  (hε : 0 ≤ ε)
  (hboundary :
    ∀ (t : Set (EuclideanSpace ℝ (Fin d))),
      Convexity.IsConvexSet ℝ t →
        ProbabilityTheory.standardGaussianBoundaryContent t ≤
          ENNReal.ofReal
            (ProbabilityTheory.ballGaussianPerimeterConstant d)) :
  (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d))).real
        (Metric.cthickening ε (closure s) \ s) ≤
      ProbabilityTheory.ballGaussianPerimeterConstant d * ε ∧
    (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d))).real
        (s \ ProbabilityTheory.convexInnerParallel s ε) ≤
      ProbabilityTheory.ballGaussianPerimeterConstant d * ε

theorem ProbabilityTheory.stdGaussian_shell_pair_le_ball_of_boundaryContent
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hne : s.Nonempty) (hsne : s ≠ Set.univ)
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ}
  (hε : 0 ≤ ε)
  (hboundary :
    ∀
      (t :
        Set (EuclideanSpace ℝ (Fin d))),
      Convexity.IsConvexSet ℝ t →
        ProbabilityTheory.standardGaussianBoundaryContent
            t ≤
          ENNReal.ofReal
            (ProbabilityTheory.ballGaussianPerimeterConstant
              d)) :
  (ProbabilityTheory.stdGaussian
            (EuclideanSpace ℝ
              (Fin d))).real
        (Metric.cthickening ε
            (closure s) \
          s) ≤
      ProbabilityTheory.ballGaussianPerimeterConstant
          d *
        ε ∧
    (ProbabilityTheory.stdGaussian
            (EuclideanSpace ℝ
              (Fin d))).real
        (s \
          ProbabilityTheory.convexInnerParallel
            s ε) ≤
      ProbabilityTheory.ballGaussianPerimeterConstant
          d *
        ε

A uniform Gaussian boundary-content estimate for convex sets implies both Gaussian shell
bounds with the same constant.  This theorem is the final coarea composition used after Ball's
perimeter theorem; it contains no convex-boundary geometry of its own.

Raič (2019), Proposition 3.1 defines the boundary and shell suprema and derives both profile disintegrations, printed pp. 2843--2845. Corollary 3.1 gives the scalar coarea formula, and Proposition 3.3 identifies \|\nabla\delta_A\|=1 almost everywhere and \{\delta_A=t\}=\partial A^t, both printed p. 2844. The two displayed outer and inner equalities occur in the proof of Proposition 3.1 on printed p. 2845. The node specializes Raič's continuous density to \phi_d, retains the precise equality-boundary conventions, and records the direct perimeter-to-shell implication.