2.5. Ball's Gaussian perimeter theorem🔗

Theorem2.5.1

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 2.5.3

Loading preview

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

✓L∃∀N

Tagsbentkusgaussian-geometryspherehausdorff-measurerotationsource-ball-1993fidelity-exact-intrinsic-ambient-normalization

Intrinsic Hausdorff measure on the Euclidean unit sphere. Let S^{d-1}=\{x\in\mathbb R^d:\|x\|=1\}, let \iota:S^{d-1}\hookrightarrow\mathbb R^d be inclusion, and let \mathcal H^{d-1}_S and \mathcal H^{d-1}_E denote Euclidean Hausdorff measure on the sphere as a metric space and on the ambient space, respectively. Then \iota_\#\mathcal H^{d-1}_S =\mathcal H^{d-1}_E\!\restriction S^{d-1}. Thus, for every nonnegative Borel function F:\mathbb R^d\to[0,\infty], \int_{S^{d-1}}F(\theta)\,d\mathcal H^{d-1}_S(\theta) =\int_{S^{d-1}}F(x)\,d\mathcal H^{d-1}_E(x). If d\ge1 and \kappa_d=\lambda_d(B(0,1)), then \mathcal H^{d-1}_S(S^{d-1})=d\kappa_d. This measure is finite, is nonzero when d\ge1, and every linear isometry U:\mathbb R^d\to\mathbb R^d preserves it: (U|_{S^{d-1}})_\#\mathcal H^{d-1}_S=\mathcal H^{d-1}_S.

Lean code for Theorem2.5.1●10 declarations

defdefined in ProbabilityApproximation/ConvexGeometry/BallSphereHausdorff.lean

complete

def ProbabilityTheory.standardSphereHausdorffMeasure (d : ℕ) :
  MeasureTheory.Measure ↑(Metric.sphere 0 1)

def ProbabilityTheory.standardSphereHausdorffMeasure
  (d : ℕ) :
  MeasureTheory.Measure
    ↑(Metric.sphere 0 1)

Intrinsic codimension-one Euclidean Hausdorff measure on the standard unit sphere.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallSphereHausdorff.lean

complete

theorem ProbabilityTheory.map_subtype_standardSphereHausdorffMeasure (d : ℕ) :
  MeasureTheory.Measure.map Subtype.val
      (ProbabilityTheory.standardSphereHausdorffMeasure d) =
    (MeasureTheory.Measure.euclideanHausdorffMeasure (d - 1)).restrict
      (Metric.sphere 0 1)

theorem ProbabilityTheory.map_subtype_standardSphereHausdorffMeasure
  (d : ℕ) :
  MeasureTheory.Measure.map Subtype.val
      (ProbabilityTheory.standardSphereHausdorffMeasure
        d) =
    (MeasureTheory.Measure.euclideanHausdorffMeasure
          (d - 1)).restrict
      (Metric.sphere 0 1)

The intrinsic sphere measure, pushed through subtype inclusion, is ambient Hausdorff measure
restricted to the unit sphere.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallSphereHausdorff.lean

complete

theorem ProbabilityTheory.lintegral_standardSphereHausdorffMeasure_eq_ambient
  {d : ℕ} (F : EuclideanSpace ℝ (Fin d) → ENNReal) (hF : Measurable F) :
  ∫⁻ (θ : ↑(Metric.sphere 0 1)),
      F ↑θ ∂ProbabilityTheory.standardSphereHausdorffMeasure d =
    ∫⁻ (x : EuclideanSpace ℝ (Fin d)) in Metric.sphere 0 1,
      F x ∂MeasureTheory.Measure.euclideanHausdorffMeasure (d - 1)

theorem ProbabilityTheory.lintegral_standardSphereHausdorffMeasure_eq_ambient
  {d : ℕ}
  (F : EuclideanSpace ℝ (Fin d) → ENNReal)
  (hF : Measurable F) :
  ∫⁻ (θ : ↑(Metric.sphere 0 1)),
      F
        ↑θ ∂ProbabilityTheory.standardSphereHausdorffMeasure
        d =
    ∫⁻ (x : EuclideanSpace ℝ (Fin d)) in
      Metric.sphere 0 1,
      F
        x ∂MeasureTheory.Measure.euclideanHausdorffMeasure
        (d - 1)

Intrinsic and ambient-restricted nonnegative sphere integrals agree.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallSphereHausdorff.lean

complete

theorem ProbabilityTheory.standardSphereHausdorffMeasure_apply_univ_eq_ambient
  (d : ℕ) :
  (ProbabilityTheory.standardSphereHausdorffMeasure d) Set.univ =
    (MeasureTheory.Measure.euclideanHausdorffMeasure (d - 1))
      (Metric.sphere 0 1)

theorem ProbabilityTheory.standardSphereHausdorffMeasure_apply_univ_eq_ambient
  (d : ℕ) :
  (ProbabilityTheory.standardSphereHausdorffMeasure
        d)
      Set.univ =
    (MeasureTheory.Measure.euclideanHausdorffMeasure
        (d - 1))
      (Metric.sphere 0 1)

Intrinsic total mass equals the ambient codimension-one Hausdorff mass of the unit sphere.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallSphereHausdorff.lean

complete

theorem ProbabilityTheory.standardSphereHausdorffMeasure_apply_univ (d : ℕ)
  (hd : d ≠ 0) :
  (ProbabilityTheory.standardSphereHausdorffMeasure d) Set.univ =
    ENNReal.ofReal (↑d * MeasureTheory.volume.real (Metric.ball 0 1))

theorem ProbabilityTheory.standardSphereHausdorffMeasure_apply_univ
  (d : ℕ) (hd : d ≠ 0) :
  (ProbabilityTheory.standardSphereHausdorffMeasure
        d)
      Set.univ =
    ENNReal.ofReal
      (↑d *
        MeasureTheory.volume.real
          (Metric.ball 0 1))

Intrinsic codimension-one Hausdorff mass of the Euclidean unit sphere is exactly dimension
times the volume of the Euclidean unit ball.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallSphereHausdorff.lean

complete

theorem ProbabilityTheory.euclideanHausdorffMeasure_unitSphere (d : ℕ)
  (hd : d ≠ 0) :
  (MeasureTheory.Measure.euclideanHausdorffMeasure (d - 1)) Set.univ =
    ENNReal.ofReal (↑d * MeasureTheory.volume.real (Metric.ball 0 1))

theorem ProbabilityTheory.euclideanHausdorffMeasure_unitSphere
  (d : ℕ) (hd : d ≠ 0) :
  (MeasureTheory.Measure.euclideanHausdorffMeasure
        (d - 1))
      Set.univ =
    ENNReal.ofReal
      (↑d *
        MeasureTheory.volume.real
          (Metric.ball 0 1))

Raw intrinsic-Hausdorff form of the exact Euclidean unit-sphere surface-area identity.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallSphereHausdorff.lean

complete

theorem ProbabilityTheory.isFiniteMeasure_standardSphereHausdorffMeasure
  (d : ℕ) :
  MeasureTheory.IsFiniteMeasure
    (ProbabilityTheory.standardSphereHausdorffMeasure d)

theorem ProbabilityTheory.isFiniteMeasure_standardSphereHausdorffMeasure
  (d : ℕ) :
  MeasureTheory.IsFiniteMeasure
    (ProbabilityTheory.standardSphereHausdorffMeasure
      d)

Intrinsic unit-sphere Hausdorff measure is finite in every Euclidean dimension.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallSphereHausdorff.lean

complete

theorem ProbabilityTheory.standardSphereHausdorffMeasure_ne_zero (d : ℕ)
  (hd : d ≠ 0) : ProbabilityTheory.standardSphereHausdorffMeasure d ≠ 0

theorem ProbabilityTheory.standardSphereHausdorffMeasure_ne_zero
  (d : ℕ) (hd : d ≠ 0) :
  ProbabilityTheory.standardSphereHausdorffMeasure
      d ≠
    0

Intrinsic unit-sphere Hausdorff measure is nonzero in every positive dimension.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallSphereHausdorff.lean

complete

theorem ProbabilityTheory.standardSphereHausdorffMeasure_apply_univ_ne_zero
  (d : ℕ) (hd : d ≠ 0) :
  (ProbabilityTheory.standardSphereHausdorffMeasure d) Set.univ ≠ 0

theorem ProbabilityTheory.standardSphereHausdorffMeasure_apply_univ_ne_zero
  (d : ℕ) (hd : d ≠ 0) :
  (ProbabilityTheory.standardSphereHausdorffMeasure
        d)
      Set.univ ≠
    0

The total intrinsic Hausdorff mass of a positive-dimensional unit sphere is nonzero.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallSphereMoments.lean

complete

theorem ProbabilityTheory.measurePreserving_linearIsometryEquivUnitSphere_euclideanHausdorffMeasure.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [MeasurableSpace E] [BorelSpace E] (e : E ≃ₗᵢ[ℝ] E) (k : ℕ) :
  MeasureTheory.MeasurePreserving
    (⇑(ProbabilityTheory.linearIsometryEquivUnitSphere e))
    (MeasureTheory.Measure.euclideanHausdorffMeasure k)
    (MeasureTheory.Measure.euclideanHausdorffMeasure k)

theorem ProbabilityTheory.measurePreserving_linearIsometryEquivUnitSphere_euclideanHausdorffMeasure.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (e : E ≃ₗᵢ[ℝ] E) (k : ℕ) :
  MeasureTheory.MeasurePreserving
    (⇑(ProbabilityTheory.linearIsometryEquivUnitSphere
        e))
    (MeasureTheory.Measure.euclideanHausdorffMeasure
      k)
    (MeasureTheory.Measure.euclideanHausdorffMeasure
      k)

Intrinsic Euclidean Hausdorff measure on the unit sphere is preserved by every ambient
linear isometry.  Unlike the normalized `Measure.toSphere` result below, this theorem needs no
comparison between the two sphere-measure constructions.

Ball (1993), equation (1) and the centered-ball evaluation immediately following it, printed pp. 411--412, use codimension-one Hausdorff measure and the factor r^{d-1}d\kappa_d, which fixes the displayed surface-area normalization. Lemma 3 introduces rotation-invariant probability on the sphere, printed p. 414, and Theorem 4, equations (2)--(3), printed pp. 415--416, passes between spherical averaging and Hausdorff surface projection. The intrinsic-to-ambient pushforward identity makes that normalization explicit; the rotation statement is valid more generally for every Hausdorff dimension on any real inner-product space.

Theorem2.5.2

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 2.5.3

Loading preview

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

✓L∃∀N

Tagsbentkusgaussian-geometryperimeterprojectionsource-ball-1993fidelity-explicit-graph-charts

Projection Jacobians and supporting-normal charts. Let d\ge2 and u,\theta\in S^{d-1}. The orthogonal projection P_{u,\theta}:u^\perp\to\theta^\perp satisfies J_{d-1}P_{u,\theta}=|\langle\theta,u\rangle|. If C\subseteq\mathbb R^d is a compact convex body, every x\in\partial C admits an outward supporting unit normal u, meaning \langle y-x,u\rangle\le0\quad\text{for every }y\in C. For fixed \theta, the boundary points with \langle\theta,u\rangle\ne0 are the countable union of the two families \langle\theta,u\rangle\ge a, \qquad \langle\theta,u\rangle\le-a, \qquad a>0. On each such patch, projection onto \theta^\perp is one-to-one and its inverse \psi is Lipschitz. At every differentiability point of \psi with unit normal u to its image tangent hyperplane, |\langle\theta,u\rangle|\,J_{d-1}D\psi=1.

Lean code for Theorem2.5.2●11 declarations

theoremdefined in ProbabilityApproximation/ConvexGeometry/SupportingNormal.lean

complete

theorem ProbabilityTheory.exists_unit_supportingNormal {d : ℕ}
  {C : Set (EuclideanSpace ℝ (Fin d))} (hC : Convexity.IsConvexSet ℝ C)
  (hclosed : IsClosed C) (hinterior : (interior C).Nonempty)
  {x : EuclideanSpace ℝ (Fin d)} (hx : x ∈ frontier C) :
  ∃ u, ‖u‖ = 1 ∧ ∀ y ∈ C, inner ℝ (y - x) u ≤ 0

theorem ProbabilityTheory.exists_unit_supportingNormal
  {d : ℕ}
  {C : Set (EuclideanSpace ℝ (Fin d))}
  (hC : Convexity.IsConvexSet ℝ C)
  (hclosed : IsClosed C)
  (hinterior : (interior C).Nonempty)
  {x : EuclideanSpace ℝ (Fin d)}
  (hx : x ∈ frontier C) :
  ∃ u,
    ‖u‖ = 1 ∧
      ∀ y ∈ C, inner ℝ (y - x) u ≤ 0

Every boundary point of a closed convex set with nonempty ambient interior has a unit outward
supporting normal.

defdefined in ProbabilityApproximation/ConvexGeometry/BallProjectionJacobian.lean

complete

def ProbabilityTheory.hyperplaneOrthogonalProjection {d : ℕ}
  (u θ : EuclideanSpace ℝ (Fin d)) : ↥(ℝ ∙ u)ᗮ →ₗ[ℝ] ↥(ℝ ∙ θ)ᗮ

def ProbabilityTheory.hyperplaneOrthogonalProjection
  {d : ℕ}
  (u θ : EuclideanSpace ℝ (Fin d)) :
  ↥(ℝ ∙ u)ᗮ →ₗ[ℝ] ↥(ℝ ∙ θ)ᗮ

Orthogonal projection from the hyperplane normal to `u` onto the hyperplane normal to `θ`.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallProjectionJacobian.lean

complete

theorem ProbabilityTheory.normDet_hyperplaneOrthogonalProjection {d : ℕ}
  {u θ : EuclideanSpace ℝ (Fin d)} (hu : ‖u‖ = 1) (hθ : ‖θ‖ = 1) :
  (ProbabilityTheory.hyperplaneOrthogonalProjection u θ).normDet =
    |inner ℝ θ u|

theorem ProbabilityTheory.normDet_hyperplaneOrthogonalProjection
  {d : ℕ} {u θ : EuclideanSpace ℝ (Fin d)}
  (hu : ‖u‖ = 1) (hθ : ‖θ‖ = 1) :
  (ProbabilityTheory.hyperplaneOrthogonalProjection
        u θ).normDet =
    |inner ℝ θ u|

The absolute Jacobian of orthogonal projection from `u⊥` to `θ⊥` is the absolute scalar
product of their unit normals.  This is the projection factor in Ball (1993), equations (2)--(3),
p. 416.

defdefined in ProbabilityApproximation/ConvexGeometry/BallProjectionArea.lean

complete

def ProbabilityTheory.supportingNormalPairs {d : ℕ}
  (C : Set (EuclideanSpace ℝ (Fin d))) :
  Set (EuclideanSpace ℝ (Fin d) × EuclideanSpace ℝ (Fin d))

def ProbabilityTheory.supportingNormalPairs
  {d : ℕ}
  (C : Set (EuclideanSpace ℝ (Fin d))) :
  Set
    (EuclideanSpace ℝ (Fin d) ×
      EuclideanSpace ℝ (Fin d))

Boundary points paired with outward supporting unit normals.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallProjectionArea.lean

complete

theorem ProbabilityTheory.transverseSupportingNormalPoints_eq_iUnion_patches
  {d : ℕ} (C : Set (EuclideanSpace ℝ (Fin d)))
  (θ : EuclideanSpace ℝ (Fin d)) :
  ProbabilityTheory.transverseSupportingNormalPoints C θ =
    (⋃ n,
        ProbabilityTheory.positiveSupportingNormalPatch C θ
          (1 / (↑n + 1))) ∪
      ⋃ n,
        ProbabilityTheory.negativeSupportingNormalPatch C θ
          (1 / (↑n + 1))

theorem ProbabilityTheory.transverseSupportingNormalPoints_eq_iUnion_patches
  {d : ℕ}
  (C : Set (EuclideanSpace ℝ (Fin d)))
  (θ : EuclideanSpace ℝ (Fin d)) :
  ProbabilityTheory.transverseSupportingNormalPoints
      C θ =
    (⋃ n,
        ProbabilityTheory.positiveSupportingNormalPatch
          C θ (1 / (↑n + 1))) ∪
      ⋃ n,
        ProbabilityTheory.negativeSupportingNormalPatch
          C θ (1 / (↑n + 1))

The transverse part of a convex boundary is a countable union of strict-sign compact
projection patches.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallProjectionArea.lean

complete

theorem ProbabilityTheory.injOn_orthogonalProjectionOnto_positiveSupportingNormalPatch
  {d : ℕ} {C : Set (EuclideanSpace ℝ (Fin d))} (hclosed : IsClosed C)
  (θ : EuclideanSpace ℝ (Fin d)) {a : ℝ} (ha : 0 < a) :
  Set.InjOn (⇑(ℝ ∙ θ)ᗮ.orthogonalProjectionOnto)
    (ProbabilityTheory.positiveSupportingNormalPatch C θ a)

theorem ProbabilityTheory.injOn_orthogonalProjectionOnto_positiveSupportingNormalPatch
  {d : ℕ}
  {C : Set (EuclideanSpace ℝ (Fin d))}
  (hclosed : IsClosed C)
  (θ : EuclideanSpace ℝ (Fin d)) {a : ℝ}
  (ha : 0 < a) :
  Set.InjOn
    (⇑(ℝ ∙ θ)ᗮ.orthogonalProjectionOnto)
    (ProbabilityTheory.positiveSupportingNormalPatch
      C θ a)

Projection in direction `θ` is injective on every strictly positive supporting-normal
patch.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallProjectionArea.lean

complete

theorem ProbabilityTheory.injOn_orthogonalProjectionOnto_negativeSupportingNormalPatch
  {d : ℕ} {C : Set (EuclideanSpace ℝ (Fin d))} (hclosed : IsClosed C)
  (θ : EuclideanSpace ℝ (Fin d)) {a : ℝ} (ha : 0 < a) :
  Set.InjOn (⇑(ℝ ∙ θ)ᗮ.orthogonalProjectionOnto)
    (ProbabilityTheory.negativeSupportingNormalPatch C θ a)

theorem ProbabilityTheory.injOn_orthogonalProjectionOnto_negativeSupportingNormalPatch
  {d : ℕ}
  {C : Set (EuclideanSpace ℝ (Fin d))}
  (hclosed : IsClosed C)
  (θ : EuclideanSpace ℝ (Fin d)) {a : ℝ}
  (ha : 0 < a) :
  Set.InjOn
    (⇑(ℝ ∙ θ)ᗮ.orthogonalProjectionOnto)
    (ProbabilityTheory.negativeSupportingNormalPatch
      C θ a)

Projection in direction `θ` is injective on every strictly negative supporting-normal
patch.

defdefined in ProbabilityApproximation/ConvexGeometry/BallProjectionArea.lean

complete

def ProbabilityTheory.orthogonalProjectionPatchInverse {d : ℕ}
  (θ : EuclideanSpace ℝ (Fin d)) (s : Set (EuclideanSpace ℝ (Fin d)))
  (z : ↥(ℝ ∙ θ)ᗮ) : EuclideanSpace ℝ (Fin d)

def ProbabilityTheory.orthogonalProjectionPatchInverse
  {d : ℕ} (θ : EuclideanSpace ℝ (Fin d))
  (s : Set (EuclideanSpace ℝ (Fin d)))
  (z : ↥(ℝ ∙ θ)ᗮ) :
  EuclideanSpace ℝ (Fin d)

A total inverse to orthogonal projection on a specified source set.  Outside the projection
image it takes the harmless value zero; all geometric statements restrict it to the image.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallProjectionArea.lean

complete

theorem ProbabilityTheory.exists_unit_normal_fderivWithin_patchInverse_normDet_mul_eq_one
  {d : ℕ} (hd : 2 ≤ d) {θ : EuclideanSpace ℝ (Fin d)} (hθ : ‖θ‖ = 1)
  {s : Set (EuclideanSpace ℝ (Fin d))} {z : ↥(ℝ ∙ θ)ᗮ}
  (hz : z ∈ ⇑(ℝ ∙ θ)ᗮ.orthogonalProjectionOnto '' s)
  (hunique :
    UniqueDiffWithinAt ℝ (⇑(ℝ ∙ θ)ᗮ.orthogonalProjectionOnto '' s) z)
  (hdiff :
    DifferentiableWithinAt ℝ
      (ProbabilityTheory.orthogonalProjectionPatchInverse θ s)
      (⇑(ℝ ∙ θ)ᗮ.orthogonalProjectionOnto '' s) z) :
  ∃ u,
    ‖u‖ = 1 ∧
      (↑(fderivWithin ℝ
                (ProbabilityTheory.orthogonalProjectionPatchInverse θ s)
                (⇑(ℝ ∙ θ)ᗮ.orthogonalProjectionOnto '' s) z)).range =
          (ℝ ∙ u)ᗮ ∧
        |inner ℝ θ u| *
            (↑(fderivWithin ℝ
                  (ProbabilityTheory.orthogonalProjectionPatchInverse θ
                    s)
                  (⇑(ℝ ∙ θ)ᗮ.orthogonalProjectionOnto '' s)
                  z)).normDet =
          1

theorem ProbabilityTheory.exists_unit_normal_fderivWithin_patchInverse_normDet_mul_eq_one
  {d : ℕ} (hd : 2 ≤ d)
  {θ : EuclideanSpace ℝ (Fin d)}
  (hθ : ‖θ‖ = 1)
  {s : Set (EuclideanSpace ℝ (Fin d))}
  {z : ↥(ℝ ∙ θ)ᗮ}
  (hz :
    z ∈
      ⇑(ℝ ∙
                θ)ᗮ.orthogonalProjectionOnto ''
        s)
  (hunique :
    UniqueDiffWithinAt ℝ
      (⇑(ℝ ∙
                θ)ᗮ.orthogonalProjectionOnto ''
        s)
      z)
  (hdiff :
    DifferentiableWithinAt ℝ
      (ProbabilityTheory.orthogonalProjectionPatchInverse
        θ s)
      (⇑(ℝ ∙
                θ)ᗮ.orthogonalProjectionOnto ''
        s)
      z) :
  ∃ u,
    ‖u‖ = 1 ∧
      (↑(fderivWithin ℝ
                (ProbabilityTheory.orthogonalProjectionPatchInverse
                  θ s)
                (⇑(ℝ ∙
                          θ)ᗮ.orthogonalProjectionOnto ''
                  s)
                z)).range =
          (ℝ ∙ u)ᗮ ∧
        |inner ℝ θ u| *
            (↑(fderivWithin ℝ
                  (ProbabilityTheory.orthogonalProjectionPatchInverse
                    θ s)
                  (⇑(ℝ ∙
                            θ)ᗮ.orthogonalProjectionOnto ''
                    s)
                  z)).normDet =
          1

The inverse graph derivative has a unit normal whose projection factor exactly cancels its
surface Jacobian.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallProjectionArea.lean

complete

theorem ProbabilityTheory.lipschitzOnWith_orthogonalProjectionPatchInverse_positivePatch
  {d : ℕ} {C : Set (EuclideanSpace ℝ (Fin d))} (hclosed : IsClosed C)
  {θ : EuclideanSpace ℝ (Fin d)} (hθ : ‖θ‖ = 1) {a : ℝ} (ha : 0 < a) :
  LipschitzOnWith (1 + a⁻¹).toNNReal
    (ProbabilityTheory.orthogonalProjectionPatchInverse θ
      (ProbabilityTheory.positiveSupportingNormalPatch C θ a))
    (⇑(ℝ ∙ θ)ᗮ.orthogonalProjectionOnto ''
      ProbabilityTheory.positiveSupportingNormalPatch C θ a)

theorem ProbabilityTheory.lipschitzOnWith_orthogonalProjectionPatchInverse_positivePatch
  {d : ℕ}
  {C : Set (EuclideanSpace ℝ (Fin d))}
  (hclosed : IsClosed C)
  {θ : EuclideanSpace ℝ (Fin d)}
  (hθ : ‖θ‖ = 1) {a : ℝ} (ha : 0 < a) :
  LipschitzOnWith (1 + a⁻¹).toNNReal
    (ProbabilityTheory.orthogonalProjectionPatchInverse
      θ
      (ProbabilityTheory.positiveSupportingNormalPatch
        C θ a))
    (⇑(ℝ ∙ θ)ᗮ.orthogonalProjectionOnto ''
      ProbabilityTheory.positiveSupportingNormalPatch
        C θ a)

The inverse chart of a positive normal patch is Lipschitz on its projection image.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallProjectionArea.lean

complete

theorem ProbabilityTheory.lipschitzOnWith_orthogonalProjectionPatchInverse_negativePatch
  {d : ℕ} {C : Set (EuclideanSpace ℝ (Fin d))} (hclosed : IsClosed C)
  {θ : EuclideanSpace ℝ (Fin d)} (hθ : ‖θ‖ = 1) {a : ℝ} (ha : 0 < a) :
  LipschitzOnWith (1 + a⁻¹).toNNReal
    (ProbabilityTheory.orthogonalProjectionPatchInverse θ
      (ProbabilityTheory.negativeSupportingNormalPatch C θ a))
    (⇑(ℝ ∙ θ)ᗮ.orthogonalProjectionOnto ''
      ProbabilityTheory.negativeSupportingNormalPatch C θ a)

theorem ProbabilityTheory.lipschitzOnWith_orthogonalProjectionPatchInverse_negativePatch
  {d : ℕ}
  {C : Set (EuclideanSpace ℝ (Fin d))}
  (hclosed : IsClosed C)
  {θ : EuclideanSpace ℝ (Fin d)}
  (hθ : ‖θ‖ = 1) {a : ℝ} (ha : 0 < a) :
  LipschitzOnWith (1 + a⁻¹).toNNReal
    (ProbabilityTheory.orthogonalProjectionPatchInverse
      θ
      (ProbabilityTheory.negativeSupportingNormalPatch
        C θ a))
    (⇑(ℝ ∙ θ)ᗮ.orthogonalProjectionOnto ''
      ProbabilityTheory.negativeSupportingNormalPatch
        C θ a)

The inverse chart of a negative normal patch is Lipschitz on its projection image.

This is the projection identity and graph decomposition in Ball (1993), equations (2)--(3) and the paragraph immediately following them, printed p. 416, in the proof of Theorem 4. The strict positive and negative patches make the inverse charts and their Jacobian cancellation explicit. Composing these charts with the preceding weighted area formula gives the surface-projection identity used in Ball's argument.

Theorem2.5.3

Statement uses 2

Statement dependency previews

Preview

Theorem 2.5.1

Loading preview

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

used by 1✓L∃∀N

Tagsbentkusgaussian-geometrysphereprojectioncauchy-formulasource-ball-1993fidelity-exact-weighted-two-hemisphere-formula

Weighted Cauchy projection formula for the Euclidean sphere. Let d\ge2, let v\in S^{d-1}, write P_v:\mathbb R^d\to v^\perp for orthogonal projection, and let g:v^\perp\to[0,\infty] be Borel measurable. With intrinsic codimension-one Hausdorff measure on S^{d-1} and Euclidean volume on v^\perp, \int_{S^{d-1}}g(P_v\theta)|\langle\theta,v\rangle| \,d\mathcal H^{d-1}(\theta) =2\int_{B_{v^\perp}(0,1)}g(z)\,dz. Equivalently, the same left-hand integral may be written over the unit sphere as an ambient subset with ambient \mathcal H^{d-1}. The factor 2 is exact: the two strict hemispheres each project one-to-one onto the open unit ball, while the equator has zero integrand.

Lean code for Theorem2.5.3●2 theorems

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallCauchyProjection.lean

complete

theorem ProbabilityTheory.lintegral_unitSphere_orthogonalProjection_mul_absInner_ambient
  {d : ℕ} (hd : 2 ≤ d) {v : EuclideanSpace ℝ (Fin d)} (hv : ‖v‖ = 1)
  (g : ↥(ℝ ∙ v)ᗮ → ENNReal) (hg : Measurable g) :
  ∫⁻ (x : EuclideanSpace ℝ (Fin d)) in Metric.sphere 0 1,
      g ((ℝ ∙ v)ᗮ.orthogonalProjectionOnto x) *
        ENNReal.ofReal
          |inner ℝ x
              v| ∂MeasureTheory.Measure.euclideanHausdorffMeasure
        (d - 1) =
    2 * ∫⁻ (z : ↥(ℝ ∙ v)ᗮ) in Metric.ball 0 1, g z

theorem ProbabilityTheory.lintegral_unitSphere_orthogonalProjection_mul_absInner_ambient
  {d : ℕ} (hd : 2 ≤ d)
  {v : EuclideanSpace ℝ (Fin d)}
  (hv : ‖v‖ = 1) (g : ↥(ℝ ∙ v)ᗮ → ENNReal)
  (hg : Measurable g) :
  ∫⁻ (x : EuclideanSpace ℝ (Fin d)) in
      Metric.sphere 0 1,
      g
          ((ℝ ∙
                  v)ᗮ.orthogonalProjectionOnto
            x) *
        ENNReal.ofReal
          |inner ℝ x
              v| ∂MeasureTheory.Measure.euclideanHausdorffMeasure
        (d - 1) =
    2 *
      ∫⁻ (z : ↥(ℝ ∙ v)ᗮ) in
        Metric.ball 0 1, g z

Ambient-set form of the Cauchy projection formula for the Euclidean unit sphere.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallCauchyProjection.lean

complete

theorem ProbabilityTheory.lintegral_unitSphere_orthogonalProjection_mul_absInner
  {d : ℕ} (hd : 2 ≤ d) {v : EuclideanSpace ℝ (Fin d)} (hv : ‖v‖ = 1)
  (g : ↥(ℝ ∙ v)ᗮ → ENNReal) (hg : Measurable g) :
  ∫⁻ (θ : ↑(Metric.sphere 0 1)),
      g ((ℝ ∙ v)ᗮ.orthogonalProjectionOnto ↑θ) *
        ENNReal.ofReal
          |inner ℝ (↑θ)
              v| ∂ProbabilityTheory.standardSphereHausdorffMeasure d =
    2 * ∫⁻ (z : ↥(ℝ ∙ v)ᗮ) in Metric.ball 0 1, g z

theorem ProbabilityTheory.lintegral_unitSphere_orthogonalProjection_mul_absInner
  {d : ℕ} (hd : 2 ≤ d)
  {v : EuclideanSpace ℝ (Fin d)}
  (hv : ‖v‖ = 1) (g : ↥(ℝ ∙ v)ᗮ → ENNReal)
  (hg : Measurable g) :
  ∫⁻ (θ : ↑(Metric.sphere 0 1)),
      g
          ((ℝ ∙
                  v)ᗮ.orthogonalProjectionOnto
            ↑θ) *
        ENNReal.ofReal
          |inner ℝ (↑θ)
              v| ∂ProbabilityTheory.standardSphereHausdorffMeasure
        d =
    2 *
      ∫⁻ (z : ↥(ℝ ∙ v)ᗮ) in
        Metric.ball 0 1, g z

Cauchy's projection formula for intrinsic codimension-one Hausdorff measure on the unit
sphere, written with an arbitrary nonnegative measurable weight on the projected unit ball.

Ball (1993), Theorem 4 constructs the projection measure in equation (2), then observes that almost every line in a fixed direction meets a convex boundary at most twice, printed pp. 415--416. The infinitesimal surface-projection factor |\langle\theta,v\rangle| is equation (3), printed p. 416. Applied to the Euclidean ball, the two projection charts give the exact weighted Cauchy formula above, including its intrinsic-Hausdorff and ambient-restriction forms.

Theorem2.5.4

uses 0used by 1✓L∃∀N

Tagsbentkusgaussian-geometryperimetersphere-averagesource-ball-1993fidelity-exact-normalized-moments

Spherical projection average. Let \sigma_{d-1} be rotation-invariant probability measure on S^{d-1}. For d\ge1 and u\in\mathbb R^d, \int_{S^{d-1}}\langle\theta,u\rangle^2\,d\sigma_{d-1}(\theta) =\frac{\|u\|^2}{d}, and hence \int_{S^{d-1}}|\langle\theta,u\rangle|\,d\sigma_{d-1}(\theta) \le\frac{\|u\|}{\sqrt d}. The measure is invariant under every linear isometry of \mathbb R^d.

Lean code for Theorem2.5.4●5 declarations

defdefined in ProbabilityApproximation/ConvexGeometry/BallSphereMeasure.lean

complete

def ProbabilityTheory.standardSphereProbability (d : ℕ) (hd : d ≠ 0) :
  MeasureTheory.ProbabilityMeasure ↑(Metric.sphere 0 1)

def ProbabilityTheory.standardSphereProbability
  (d : ℕ) (hd : d ≠ 0) :
  MeasureTheory.ProbabilityMeasure
    ↑(Metric.sphere 0 1)

Rotation-invariant surface measure normalized to total mass one.  The proof `d ≠ 0`
provides the point required by `FiniteMeasure.normalize`; proof irrelevance makes the resulting
measure independent of its particular witness.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallSphereMoments.lean

complete

theorem ProbabilityTheory.map_linearIsometryEquivUnitSphere_standardSphereProbability
  {d : ℕ} (hd : d ≠ 0)
  (e : EuclideanSpace ℝ (Fin d) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin d)) :
  MeasureTheory.Measure.map
      ⇑(ProbabilityTheory.linearIsometryEquivUnitSphere e)
      ↑(ProbabilityTheory.standardSphereProbability d hd) =
    ↑(ProbabilityTheory.standardSphereProbability d hd)

theorem ProbabilityTheory.map_linearIsometryEquivUnitSphere_standardSphereProbability
  {d : ℕ} (hd : d ≠ 0)
  (e :
    EuclideanSpace ℝ (Fin d) ≃ₗᵢ[ℝ]
      EuclideanSpace ℝ (Fin d)) :
  MeasureTheory.Measure.map
      ⇑(ProbabilityTheory.linearIsometryEquivUnitSphere
          e)
      ↑(ProbabilityTheory.standardSphereProbability
          d hd) =
    ↑(ProbabilityTheory.standardSphereProbability
        d hd)

The normalized unit-sphere probability is invariant under linear isometry equivalences.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallSphereMoments.lean

complete

theorem ProbabilityTheory.measurePreserving_linearIsometryEquivUnitSphere_standardSphereProbability
  {d : ℕ} (hd : d ≠ 0)
  (e : EuclideanSpace ℝ (Fin d) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin d)) :
  MeasureTheory.MeasurePreserving
    ⇑(ProbabilityTheory.linearIsometryEquivUnitSphere e)
    ↑(ProbabilityTheory.standardSphereProbability d hd)
    ↑(ProbabilityTheory.standardSphereProbability d hd)

theorem ProbabilityTheory.measurePreserving_linearIsometryEquivUnitSphere_standardSphereProbability
  {d : ℕ} (hd : d ≠ 0)
  (e :
    EuclideanSpace ℝ (Fin d) ≃ₗᵢ[ℝ]
      EuclideanSpace ℝ (Fin d)) :
  MeasureTheory.MeasurePreserving
    ⇑(ProbabilityTheory.linearIsometryEquivUnitSphere
        e)
    ↑(ProbabilityTheory.standardSphereProbability
        d hd)
    ↑(ProbabilityTheory.standardSphereProbability
        d hd)

The sphere restriction of a Euclidean linear isometry is measure-preserving for the
normalized surface probability.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallSphereMoments.lean

complete

theorem ProbabilityTheory.integral_inner_sq_standardSphereProbability {d : ℕ}
  (hd : d ≠ 0) (u : EuclideanSpace ℝ (Fin d)) :
  ∫ (θ : ↑(Metric.sphere 0 1)),
      inner ℝ (↑θ) u ^
        2 ∂↑(ProbabilityTheory.standardSphereProbability d hd) =
    ‖u‖ ^ 2 / ↑d

theorem ProbabilityTheory.integral_inner_sq_standardSphereProbability
  {d : ℕ} (hd : d ≠ 0)
  (u : EuclideanSpace ℝ (Fin d)) :
  ∫ (θ : ↑(Metric.sphere 0 1)),
      inner ℝ (↑θ) u ^
        2 ∂↑(ProbabilityTheory.standardSphereProbability
          d hd) =
    ‖u‖ ^ 2 / ↑d

The exact covariance of rotation-invariant probability on the Euclidean unit sphere.  This is
the spherical second-moment identity used in Ball (1993), p. 416.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallSphereMoments.lean

complete

theorem ProbabilityTheory.integral_abs_inner_standardSphereProbability_le
  {d : ℕ} (hd : d ≠ 0) (u : EuclideanSpace ℝ (Fin d)) :
  ∫ (θ : ↑(Metric.sphere 0 1)),
      |inner ℝ (↑θ)
          u| ∂↑(ProbabilityTheory.standardSphereProbability d hd) ≤
    ‖u‖ / √↑d

theorem ProbabilityTheory.integral_abs_inner_standardSphereProbability_le
  {d : ℕ} (hd : d ≠ 0)
  (u : EuclideanSpace ℝ (Fin d)) :
  ∫ (θ : ↑(Metric.sphere 0 1)),
      |inner ℝ (↑θ)
          u| ∂↑(ProbabilityTheory.standardSphereProbability
          d hd) ≤
    ‖u‖ / √↑d

The spherical first absolute moment is bounded by the square root of the second moment.  In
Ball's projection average this contributes the factor `d⁻¹ᐟ²`.

Ball (1993), averages the projection inequality over S^{d-1} immediately before equation (4), printed p. 416, in the proof of Theorem 4. The displayed second moment is the rotation-invariant covariance calculation underlying Ball's d^{-1/2} factor; Cauchy--Schwarz gives the absolute first-moment inequality.

Theorem2.5.5

uses 1used by 1✓L∃∀N

Tagsbentkusgaussian-geometryperimeterrearrangementsource-ball-1993fidelity-applied-continuous-g-equals-identity

Ball's spherical rearrangement inequality in the applied form. Let d\ge1, let \sigma_{d-1} be rotation-invariant probability measure on S^{d-1}, and let F:\mathbb R\to\mathbb R be continuous and nondecreasing on [0,\infty). If u,v\in S^{d-1} are orthogonal, 0\le\alpha\le\pi/2, and w_\alpha=\cos(\alpha)u+\sin(\alpha)v, then \int_{S^{d-1}}F(|\langle\theta,u\rangle|) |\langle\theta,v\rangle|\,d\sigma_{d-1}(\theta) \le \int_{S^{d-1}}F(|\langle\theta,u\rangle|) |\langle\theta,w_\alpha\rangle|\,d\sigma_{d-1}(\theta).

Lean code for Theorem2.5.5●2 theorems

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallSphericalRearrangement.lean

complete

theorem ProbabilityTheory.ballSphericalRearrangement_absInner_of_measure {d : ℕ}
  (μ : MeasureTheory.Measure ↑(Metric.sphere 0 1))
  [MeasureTheory.IsFiniteMeasure μ]
  (hμ :
    ∀ (e : EuclideanSpace ℝ (Fin d) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin d)),
      MeasureTheory.MeasurePreserving
        (⇑(ProbabilityTheory.linearIsometryEquivUnitSphere e)) μ μ)
  {F : ℝ → ℝ} (hF : Continuous F) (hFmono : MonotoneOn F (Set.Ici 0))
  {u v : EuclideanSpace ℝ (Fin d)} (hu : ‖u‖ = 1) (hv : ‖v‖ = 1)
  (huv : inner ℝ u v = 0) {α : ℝ} (hα : α ∈ Set.Icc 0 (Real.pi / 2)) :
  ∫ (θ : ↑(Metric.sphere 0 1)),
      F |inner ℝ (↑θ) u| * |inner ℝ (↑θ) v| ∂μ ≤
    ∫ (θ : ↑(Metric.sphere 0 1)),
      F |inner ℝ (↑θ) u| *
        |inner ℝ (↑θ) (Real.cos α • u + Real.sin α • v)| ∂μ

theorem ProbabilityTheory.ballSphericalRearrangement_absInner_of_measure
  {d : ℕ}
  (μ :
    MeasureTheory.Measure
      ↑(Metric.sphere 0 1))
  [MeasureTheory.IsFiniteMeasure μ]
  (hμ :
    ∀
      (e :
        EuclideanSpace ℝ (Fin d) ≃ₗᵢ[ℝ]
          EuclideanSpace ℝ (Fin d)),
      MeasureTheory.MeasurePreserving
        (⇑(ProbabilityTheory.linearIsometryEquivUnitSphere
            e))
        μ μ)
  {F : ℝ → ℝ} (hF : Continuous F)
  (hFmono : MonotoneOn F (Set.Ici 0))
  {u v : EuclideanSpace ℝ (Fin d)}
  (hu : ‖u‖ = 1) (hv : ‖v‖ = 1)
  (huv : inner ℝ u v = 0) {α : ℝ}
  (hα : α ∈ Set.Icc 0 (Real.pi / 2)) :
  ∫ (θ : ↑(Metric.sphere 0 1)),
      F |inner ℝ (↑θ) u| *
        |inner ℝ (↑θ) v| ∂μ ≤
    ∫ (θ : ↑(Metric.sphere 0 1)),
      F |inner ℝ (↑θ) u| *
        |inner ℝ (↑θ)
            (Real.cos α • u +
              Real.sin α • v)| ∂μ

**Ball's spherical rearrangement inequality for a finite rotation-invariant measure,
applied form (`G(t) = t`).**

Let `u,v` be orthogonal unit directions.  For every continuous function `F` that is
nondecreasing on the nonnegative real axis, the spherical correlation with the second direction
is smallest at the orthogonal angle.  This is the exact specialization of Ball (1993), Lemma 3,
used in the proof of his Gaussian perimeter theorem.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallSphericalRearrangement.lean

complete

theorem ProbabilityTheory.ballSphericalRearrangement_absInner {d : ℕ}
  (hd : d ≠ 0) {F : ℝ → ℝ} (hF : Continuous F)
  (hFmono : MonotoneOn F (Set.Ici 0)) {u v : EuclideanSpace ℝ (Fin d)}
  (hu : ‖u‖ = 1) (hv : ‖v‖ = 1) (huv : inner ℝ u v = 0) {α : ℝ}
  (hα : α ∈ Set.Icc 0 (Real.pi / 2)) :
  ∫ (θ : ↑(Metric.sphere 0 1)),
      F |inner ℝ (↑θ) u| *
        |inner ℝ (↑θ)
            v| ∂↑(ProbabilityTheory.standardSphereProbability d hd) ≤
    ∫ (θ : ↑(Metric.sphere 0 1)),
      F |inner ℝ (↑θ) u| *
        |inner ℝ (↑θ)
            (Real.cos α • u +
              Real.sin α •
                v)| ∂↑(ProbabilityTheory.standardSphereProbability d hd)

theorem ProbabilityTheory.ballSphericalRearrangement_absInner
  {d : ℕ} (hd : d ≠ 0) {F : ℝ → ℝ}
  (hF : Continuous F)
  (hFmono : MonotoneOn F (Set.Ici 0))
  {u v : EuclideanSpace ℝ (Fin d)}
  (hu : ‖u‖ = 1) (hv : ‖v‖ = 1)
  (huv : inner ℝ u v = 0) {α : ℝ}
  (hα : α ∈ Set.Icc 0 (Real.pi / 2)) :
  ∫ (θ : ↑(Metric.sphere 0 1)),
      F |inner ℝ (↑θ) u| *
        |inner ℝ (↑θ)
            v| ∂↑(ProbabilityTheory.standardSphereProbability
          d hd) ≤
    ∫ (θ : ↑(Metric.sphere 0 1)),
      F |inner ℝ (↑θ) u| *
        |inner ℝ (↑θ)
            (Real.cos α • u +
              Real.sin α •
                v)| ∂↑(ProbabilityTheory.standardSphereProbability
          d hd)

**Ball's spherical rearrangement inequality, applied form (`G(t) = t`).**

This is the rotation-invariant probability specialization of
`ballSphericalRearrangement_absInner_of_measure`.

Ball (1993), Lemma 3 and its circle-fiber proof, printed pp. 414--415, treats two arbitrary nondecreasing functions on [0,1]. The result recorded here is the exact continuous G(t)=t specialization used in Theorem 4: on printed p. 416, immediately after equation (3), Ball takes F(t)=f(r\sqrt{1-t^2}), which is nondecreasing because the radial density f is nonincreasing, and concludes that the spherical integral is minimized when the position and normal directions are perpendicular.

Lemma2.5.6

uses 0used by 1✓L∃∀N

Tagsbentkusgaussian-geometryperimeterradial-estimatesource-ball-1993fidelity-exact-one-over-pi

Radial Gaussian peak and Gamma bound. For every integer n\ge3 and every t\ge0, e^{-t^2/2}t^{n-2} \le e^{-(n-2)/2}(n-2)^{(n-2)/2}. Moreover, \frac{e^{-(n-2)/2}(n-2)^{(n-2)/2}} {2^{n/2-1}\Gamma((n-1)/2)\sqrt\pi} \le\frac1\pi.

Lean code for Lemma2.5.6●2 theorems

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallRadialGammaBound.lean

complete

theorem ProbabilityTheory.exp_neg_half_mul_rpow_le_peak {n : ℕ} (hn : 3 ≤ n)
  {t : ℝ} (ht : 0 ≤ t) :
  Real.exp (-t ^ 2 / 2) * t ^ (↑n - 2) ≤
    Real.exp (-((↑n - 2) / 2)) * (↑n - 2) ^ ((↑n - 2) / 2)

theorem ProbabilityTheory.exp_neg_half_mul_rpow_le_peak
  {n : ℕ} (hn : 3 ≤ n) {t : ℝ}
  (ht : 0 ≤ t) :
  Real.exp (-t ^ 2 / 2) * t ^ (↑n - 2) ≤
    Real.exp (-((↑n - 2) / 2)) *
      (↑n - 2) ^ ((↑n - 2) / 2)

The radial factor `exp (-t²/2) t^(n-2)` attains its maximum at `t = √(n-2)`.

The right-hand side is the value at the maximizer.  This is the estimate immediately preceding
the normalized Gamma bound on Ball (1993), printed p. 419.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallRadialGammaBound.lean

complete

theorem ProbabilityTheory.ball_radial_gamma_peak_le {n : ℕ} (hn : 3 ≤ n) :
  Real.exp (-((↑n - 2) / 2)) * (↑n - 2) ^ ((↑n - 2) / 2) /
      (2 ^ (↑n / 2 - 1) * Real.Gamma ((↑n - 1) / 2) * √Real.pi) ≤
    1 / Real.pi

theorem ProbabilityTheory.ball_radial_gamma_peak_le
  {n : ℕ} (hn : 3 ≤ n) :
  Real.exp (-((↑n - 2) / 2)) *
        (↑n - 2) ^ ((↑n - 2) / 2) /
      (2 ^ (↑n / 2 - 1) *
          Real.Gamma ((↑n - 1) / 2) *
        √Real.pi) ≤
    1 / Real.pi

Ball's normalized radial peak is at most `1 / π` in every dimension `n ≥ 3`.

This is the Stirling/Gamma estimate displayed in the last paragraph of Ball (1993), printed
p. 419.

These are the one-dimensional maximum and the normalized Gamma estimate in the last paragraph of Ball (1993), printed p. 419, completing the analytic estimate in the proof of Theorem 4. The second inequality retains Ball's exact 1/\pi constant in every dimension n\ge3.

Theorem2.5.7

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 2.5.8

Loading preview

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

✓L∃∀N

Tagsbentkusgaussian-geometryperimeterradial-majorantsource-ball-1993fidelity-exact-construction-projection-and-mass

Ball's radial projection majorant. For n\ge2, put a_n=(\sqrt{2\pi})^{-n},\qquad h_n(t)=a_n\int_0^{\pi/2} (n-1-t^2\sin^2\theta)\sin^{n-2}\theta\, e^{-t^2\sin^2\theta/2}\,d\theta, \qquad f_n(t)=\max\{h_n(t),0\}. Then f_n is continuous on \mathbb R, nonnegative everywhere, nonincreasing on [0,\infty), and t\ge\sqrt{2n}\quad\Longrightarrow\quad f_n(t)=0. For a radial function q:\mathbb R\to\mathbb R, define its spherical projection by (T_nq)(r)=\frac2\pi\int_0^{\pi/2}q(r\sin\theta) \sin^{n-1}\theta\,d\theta. For every r\in\mathbb R, the signed auxiliary function has the exact projection identity and its positive part gives the Gaussian majorization (T_nh_n)(r)=a_ne^{-r^2/2} \le (T_nf_n)(r). Finally, set c_n=\left(2^{n/2-1}\Gamma\!\left(\frac{n-1}{2}\right)\sqrt\pi\right)^{-1}, \qquad p_n=(n-1)\,\operatorname{vol}_{n-1}(B_{n-1}(0,1)). The polar normalization is exact, p_na_n=c_n, and the one-dimensional and Euclidean mass bounds are \frac{c_n}{a_n}\int_{(0,\infty)}f_n(t)t^{n-2}\,dt \le 2n^{1/4}, \qquad \int_{\mathbb R^{n-1}}f_n(\|x\|)\,dx \le 2n^{1/4}. The same nonnegative-integral bound holds on every finite-dimensional real inner-product space of dimension n-1.

Lean code for Theorem2.5.7●18 declarations

defdefined in ProbabilityApproximation/ConvexGeometry/BallRadialMajorant.lean

complete

def ProbabilityTheory.ballGaussianNormalization (n : ℕ) : ℝ

def ProbabilityTheory.ballGaussianNormalization
  (n : ℕ) : ℝ

The normalization of the `n`-dimensional standard Gaussian density.

defdefined in ProbabilityApproximation/ConvexGeometry/BallRadialMajorant.lean

complete

def ProbabilityTheory.ballRadialAuxIntegrand (n : ℕ) (t θ : ℝ) : ℝ

def ProbabilityTheory.ballRadialAuxIntegrand
  (n : ℕ) (t θ : ℝ) : ℝ

The integrand in Ball's formula (6) for the signed radial function `h`.

defdefined in ProbabilityApproximation/ConvexGeometry/BallRadialMajorant.lean

complete

def ProbabilityTheory.ballRadialAux (n : ℕ) (t : ℝ) : ℝ

def ProbabilityTheory.ballRadialAux (n : ℕ)
  (t : ℝ) : ℝ

Ball's signed radial density `h`, equation (6) on printed p. 417.

defdefined in ProbabilityApproximation/ConvexGeometry/BallRadialMajorant.lean

complete

def ProbabilityTheory.ballRadialMajorant (n : ℕ) (t : ℝ) : ℝ

def ProbabilityTheory.ballRadialMajorant
  (n : ℕ) (t : ℝ) : ℝ

Ball's nonnegative radial projection majorant `f = h+`.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallRadialMajorant.lean

complete

theorem ProbabilityTheory.continuous_ballRadialMajorant (n : ℕ) :
  Continuous (ProbabilityTheory.ballRadialMajorant n)

theorem ProbabilityTheory.continuous_ballRadialMajorant
  (n : ℕ) :
  Continuous
    (ProbabilityTheory.ballRadialMajorant
      n)

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallRadialMajorant.lean

complete

theorem ProbabilityTheory.ballRadialMajorant_nonneg (n : ℕ) (t : ℝ) :
  0 ≤ ProbabilityTheory.ballRadialMajorant n t

theorem ProbabilityTheory.ballRadialMajorant_nonneg
  (n : ℕ) (t : ℝ) :
  0 ≤
    ProbabilityTheory.ballRadialMajorant n
      t

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallRadialMajorant.lean

complete

theorem ProbabilityTheory.ballRadialMajorant_eq_zero_of_sqrt_two_mul_le {n : ℕ}
  (hn : 2 ≤ n) {t : ℝ} (ht : √(2 * ↑n) ≤ t) :
  ProbabilityTheory.ballRadialMajorant n t = 0

theorem ProbabilityTheory.ballRadialMajorant_eq_zero_of_sqrt_two_mul_le
  {n : ℕ} (hn : 2 ≤ n) {t : ℝ}
  (ht : √(2 * ↑n) ≤ t) :
  ProbabilityTheory.ballRadialMajorant n
      t =
    0

Ball's nonnegative radial majorant vanishes beyond `sqrt (2n)`.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallRadialMajorant.lean

complete

theorem ProbabilityTheory.antitoneOn_ballRadialMajorant {n : ℕ} (hn : 2 ≤ n) :
  AntitoneOn (ProbabilityTheory.ballRadialMajorant n) (Set.Ici 0)

theorem ProbabilityTheory.antitoneOn_ballRadialMajorant
  {n : ℕ} (hn : 2 ≤ n) :
  AntitoneOn
    (ProbabilityTheory.ballRadialMajorant
      n)
    (Set.Ici 0)

The positive part `f = h+` is nonincreasing on `[0, ∞)`, as required in Ball's
rearrangement step between equations (3) and (4).

defdefined in ProbabilityApproximation/ConvexGeometry/BallRadialMajorant.lean

complete

def ProbabilityTheory.ballRadialProjectionTransform (n : ℕ) (f : ℝ → ℝ)
  (r : ℝ) : ℝ

def ProbabilityTheory.ballRadialProjectionTransform
  (n : ℕ) (f : ℝ → ℝ) (r : ℝ) : ℝ

Ball's spherical projection transform for a radial density in dimension `n - 1`.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallRadialMajorant.lean

complete

theorem ProbabilityTheory.ballRadialAux_projection_eq_standardGaussian {n : ℕ}
  (hn : 2 ≤ n) (r : ℝ) :
  ProbabilityTheory.ballRadialProjectionTransform n
      (ProbabilityTheory.ballRadialAux n) r =
    ProbabilityTheory.ballGaussianNormalization n *
      Real.exp (-r ^ 2 / 2)

theorem ProbabilityTheory.ballRadialAux_projection_eq_standardGaussian
  {n : ℕ} (hn : 2 ≤ n) (r : ℝ) :
  ProbabilityTheory.ballRadialProjectionTransform
      n
      (ProbabilityTheory.ballRadialAux n)
      r =
    ProbabilityTheory.ballGaussianNormalization
        n *
      Real.exp (-r ^ 2 / 2)

Ball's signed radial density projects exactly to the standard Gaussian radial density.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallRadialMajorant.lean

complete

theorem ProbabilityTheory.standardGaussianDensityReal_le_ballRadialMajorant_projection
  {n : ℕ} (hn : 2 ≤ n) (r : ℝ) :
  ProbabilityTheory.ballGaussianNormalization n *
      Real.exp (-r ^ 2 / 2) ≤
    ProbabilityTheory.ballRadialProjectionTransform n
      (ProbabilityTheory.ballRadialMajorant n) r

theorem ProbabilityTheory.standardGaussianDensityReal_le_ballRadialMajorant_projection
  {n : ℕ} (hn : 2 ≤ n) (r : ℝ) :
  ProbabilityTheory.ballGaussianNormalization
        n *
      Real.exp (-r ^ 2 / 2) ≤
    ProbabilityTheory.ballRadialProjectionTransform
      n
      (ProbabilityTheory.ballRadialMajorant
        n)
      r

The positive part of Ball's signed density has spherical projection at least the standard
Gaussian radial density.

defdefined in ProbabilityApproximation/ConvexGeometry/BallRadialMass.lean

complete

def ProbabilityTheory.ballRadialMassCoefficient (n : ℕ) : ℝ

def ProbabilityTheory.ballRadialMassCoefficient
  (n : ℕ) : ℝ

The explicit coefficient converting Ball's one-dimensional radial integral into
`(n - 1)`-dimensional Euclidean mass.

defdefined in ProbabilityApproximation/ConvexGeometry/BallRadialMass.lean

complete

def ProbabilityTheory.ballRadialPolarFactor (n : ℕ) : ℝ

def ProbabilityTheory.ballRadialPolarFactor
  (n : ℕ) : ℝ

The polar-coordinate surface factor in dimension `n - 1`.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallRadialMass.lean

complete

theorem ProbabilityTheory.ballRadialPolarFactor_mul_normalization {n : ℕ}
  (hn : 2 ≤ n) :
  ProbabilityTheory.ballRadialPolarFactor n *
      ProbabilityTheory.ballGaussianNormalization n =
    ProbabilityTheory.ballRadialMassCoefficient n

theorem ProbabilityTheory.ballRadialPolarFactor_mul_normalization
  {n : ℕ} (hn : 2 ≤ n) :
  ProbabilityTheory.ballRadialPolarFactor
        n *
      ProbabilityTheory.ballGaussianNormalization
        n =
    ProbabilityTheory.ballRadialMassCoefficient
      n

The explicit Gamma coefficient is exactly the Haar polar-coordinate factor times the
`n`-dimensional Gaussian normalization.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallRadialMass.lean

complete

theorem ProbabilityTheory.integral_ballRadialMajorant_rpow_le {n : ℕ}
  (hn : 2 ≤ n) :
  ProbabilityTheory.ballRadialMassCoefficient n /
        ProbabilityTheory.ballGaussianNormalization n *
      ∫ (t : ℝ) in Set.Ioi 0,
        ProbabilityTheory.ballRadialMajorant n t * t ^ (n - 2) ≤
    2 * ↑n ^ (1 / 4)

theorem ProbabilityTheory.integral_ballRadialMajorant_rpow_le
  {n : ℕ} (hn : 2 ≤ n) :
  ProbabilityTheory.ballRadialMassCoefficient
          n /
        ProbabilityTheory.ballGaussianNormalization
          n *
      ∫ (t : ℝ) in Set.Ioi 0,
        ProbabilityTheory.ballRadialMajorant
            n t *
          t ^ (n - 2) ≤
    2 * ↑n ^ (1 / 4)

Ball's radial majorant has mass at most `2 n^(1/4)` after the exact polar-coordinate
normalization.  This is the one-dimensional estimate on printed pp. 418--419.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallRadialMass.lean

complete

theorem ProbabilityTheory.integral_ballRadialMajorant_norm_le {n : ℕ}
  (hn : 2 ≤ n) :
  ∫ (x : EuclideanSpace ℝ (Fin (n - 1))),
      ProbabilityTheory.ballRadialMajorant n ‖x‖ ≤
    2 * ↑n ^ (1 / 4)

theorem ProbabilityTheory.integral_ballRadialMajorant_norm_le
  {n : ℕ} (hn : 2 ≤ n) :
  ∫ (x : EuclideanSpace ℝ (Fin (n - 1))),
      ProbabilityTheory.ballRadialMajorant
        n ‖x‖ ≤
    2 * ↑n ^ (1 / 4)

The Euclidean integral of Ball's radial majorant on `R^(n-1)` is at most `2 n^(1/4)`.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallRadialMass.lean

complete

theorem ProbabilityTheory.lintegral_ballRadialMajorant_norm_le {n : ℕ}
  (hn : 2 ≤ n) :
  ∫⁻ (x : EuclideanSpace ℝ (Fin (n - 1))),
      ENNReal.ofReal (ProbabilityTheory.ballRadialMajorant n ‖x‖) ≤
    ENNReal.ofReal (2 * ↑n ^ (1 / 4))

theorem ProbabilityTheory.lintegral_ballRadialMajorant_norm_le
  {n : ℕ} (hn : 2 ≤ n) :
  ∫⁻ (x : EuclideanSpace ℝ (Fin (n - 1))),
      ENNReal.ofReal
        (ProbabilityTheory.ballRadialMajorant
          n ‖x‖) ≤
    ENNReal.ofReal (2 * ↑n ^ (1 / 4))

ENNReal form of the Euclidean mass bound, used by the projection-area argument.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallRadialMass.lean

complete

theorem ProbabilityTheory.lintegral_ballRadialMajorant_norm_le_of_finrank.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {n : ℕ}
  (hn : 2 ≤ n) (hrank : Module.finrank ℝ E = n - 1) :
  ∫⁻ (x : E),
      ENNReal.ofReal (ProbabilityTheory.ballRadialMajorant n ‖x‖) ≤
    ENNReal.ofReal (2 * ↑n ^ (1 / 4))

theorem ProbabilityTheory.lintegral_ballRadialMajorant_norm_le_of_finrank.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] {n : ℕ}
  (hn : 2 ≤ n)
  (hrank : Module.finrank ℝ E = n - 1) :
  ∫⁻ (x : E),
      ENNReal.ofReal
        (ProbabilityTheory.ballRadialMajorant
          n ‖x‖) ≤
    ENNReal.ofReal (2 * ↑n ^ (1 / 4))

Coordinate-free form of the radial mass bound for any finite-dimensional real inner-product
space of dimension `n - 1`.

Ball (1993), reduces Theorem 4 to the projection majorization in equation (4), defines the signed inverse transform by equations (5)--(6), and takes its positive part, printed p. 417. The power-series calculation following equation (7), also on printed p. 417, proves the required monotonicity; the zero-location estimate and polar mass identity are on printed p. 418. The two-part integral estimate and normalized Gamma peak close \mu(\mathbb R^{n-1})\le2n^{1/4} on printed pp. 418--419. The formal result separates the construction, the exact signed projection, the positive-part majorization, the compact positive-radius support, and both normalized forms of the mass estimate.

Theorem2.5.8

Statement uses 4

Statement dependency previews

Preview

Theorem 2.5.1

Loading preview

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

used by 1✓L∃∀N

Tagsbentkusgaussian-geometryperimeterspherical-projectionsource-ball-1993fidelity-exact-pointwise-vector-form

Spherical majorization of Gaussian density times a normal magnitude. Let d\ge2, let x,N\in\mathbb R^d, and write P_\theta for orthogonal projection onto \theta^\perp. If f_d is Ball's radial majorant, \phi_d is standard Gaussian density, and \mathcal H^{d-1}_S is intrinsic Hausdorff measure on S^{d-1}, then \phi_d(x)\|N\| \le \frac{1}{\mathcal H^{d-1}_S(S^{d-1})} \int_{S^{d-1}} f_d(\|P_\theta x\|) |\langle\theta,N\rangle|\,d\mathcal H^{d-1}_S(\theta). The statement also includes the exact orthogonal-direction identity with Ball's one-dimensional transform and the monotone spherical rearrangement inequality that extends it to an arbitrary normal direction. No normalization assumption is made on N.

Lean code for Theorem2.5.8●6 declarations

defdefined in ProbabilityApproximation/ConvexGeometry/BallSphericalProjection.lean

complete

def ProbabilityTheory.ballSphericalRadialProfile (f : ℝ → ℝ) (r s : ℝ) : ℝ

def ProbabilityTheory.ballSphericalRadialProfile
  (f : ℝ → ℝ) (r s : ℝ) : ℝ

The one-dimensional profile obtained by radially projecting a point of radius `r`
onto the hyperplane perpendicular to a sphere direction with axial coordinate `s`.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallSphericalProjection.lean

complete

theorem ProbabilityTheory.normalizedHausdorff_lintegral_ballSphericalRadialProfile_absInner_orthogonal
  {d : ℕ} (hd : 2 ≤ d) {u v : EuclideanSpace ℝ (Fin d)} (hu : ‖u‖ = 1)
  (hv : ‖v‖ = 1) (huv : inner ℝ u v = 0) {f : ℝ → ℝ} (hF : Continuous f)
  (hf : ∀ (x : ℝ), 0 ≤ f x) (r : ℝ) :
  ((ProbabilityTheory.standardSphereHausdorffMeasure d) Set.univ)⁻¹ *
      ∫⁻ (θ : ↑(Metric.sphere 0 1)),
        ENNReal.ofReal
            (ProbabilityTheory.ballSphericalRadialProfile f r
              |inner ℝ (↑θ) u|) *
          ENNReal.ofReal
            |inner ℝ (↑θ)
                v| ∂ProbabilityTheory.standardSphereHausdorffMeasure d =
    ENNReal.ofReal
      (ProbabilityTheory.ballRadialProjectionTransform d f r)

theorem ProbabilityTheory.normalizedHausdorff_lintegral_ballSphericalRadialProfile_absInner_orthogonal
  {d : ℕ} (hd : 2 ≤ d)
  {u v : EuclideanSpace ℝ (Fin d)}
  (hu : ‖u‖ = 1) (hv : ‖v‖ = 1)
  (huv : inner ℝ u v = 0) {f : ℝ → ℝ}
  (hF : Continuous f)
  (hf : ∀ (x : ℝ), 0 ≤ f x) (r : ℝ) :
  ((ProbabilityTheory.standardSphereHausdorffMeasure
            d)
          Set.univ)⁻¹ *
      ∫⁻ (θ : ↑(Metric.sphere 0 1)),
        ENNReal.ofReal
            (ProbabilityTheory.ballSphericalRadialProfile
              f r |inner ℝ (↑θ) u|) *
          ENNReal.ofReal
            |inner ℝ (↑θ)
                v| ∂ProbabilityTheory.standardSphereHausdorffMeasure
          d =
    ENNReal.ofReal
      (ProbabilityTheory.ballRadialProjectionTransform
        d f r)

The normalized intrinsic-Hausdorff spherical projection in two orthogonal directions is
exactly Ball's one-dimensional radial projection transform.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallSphericalProjection.lean

complete

theorem ProbabilityTheory.lintegral_ballSphericalRearrangement_radialProfile
  {d : ℕ} {f : ℝ → ℝ} (hF : Continuous f)
  (hfanti : AntitoneOn f (Set.Ici 0)) (hf : ∀ (x : ℝ), 0 ≤ f x) {r : ℝ}
  (hr : 0 ≤ r) {u v : EuclideanSpace ℝ (Fin d)} (hu : ‖u‖ = 1)
  (hv : ‖v‖ = 1) (huv : inner ℝ u v = 0) {α : ℝ}
  (hα : α ∈ Set.Icc 0 (Real.pi / 2)) :
  ∫⁻ (θ : ↑(Metric.sphere 0 1)),
      ENNReal.ofReal
          (ProbabilityTheory.ballSphericalRadialProfile f r
            |inner ℝ (↑θ) u|) *
        ENNReal.ofReal
          |inner ℝ (↑θ)
              v| ∂ProbabilityTheory.standardSphereHausdorffMeasure d ≤
    ∫⁻ (θ : ↑(Metric.sphere 0 1)),
      ENNReal.ofReal
          (ProbabilityTheory.ballSphericalRadialProfile f r
            |inner ℝ (↑θ) u|) *
        ENNReal.ofReal
          |inner ℝ (↑θ)
              (Real.cos α • u +
                Real.sin α •
                  v)| ∂ProbabilityTheory.standardSphereHausdorffMeasure
        d

theorem ProbabilityTheory.lintegral_ballSphericalRearrangement_radialProfile
  {d : ℕ} {f : ℝ → ℝ} (hF : Continuous f)
  (hfanti : AntitoneOn f (Set.Ici 0))
  (hf : ∀ (x : ℝ), 0 ≤ f x) {r : ℝ}
  (hr : 0 ≤ r)
  {u v : EuclideanSpace ℝ (Fin d)}
  (hu : ‖u‖ = 1) (hv : ‖v‖ = 1)
  (huv : inner ℝ u v = 0) {α : ℝ}
  (hα : α ∈ Set.Icc 0 (Real.pi / 2)) :
  ∫⁻ (θ : ↑(Metric.sphere 0 1)),
      ENNReal.ofReal
          (ProbabilityTheory.ballSphericalRadialProfile
            f r |inner ℝ (↑θ) u|) *
        ENNReal.ofReal
          |inner ℝ (↑θ)
              v| ∂ProbabilityTheory.standardSphereHausdorffMeasure
        d ≤
    ∫⁻ (θ : ↑(Metric.sphere 0 1)),
      ENNReal.ofReal
          (ProbabilityTheory.ballSphericalRadialProfile
            f r |inner ℝ (↑θ) u|) *
        ENNReal.ofReal
          |inner ℝ (↑θ)
              (Real.cos α • u +
                Real.sin α •
                  v)| ∂ProbabilityTheory.standardSphereHausdorffMeasure
        d

ENNReal form of Ball's rearrangement inequality for intrinsic sphere Hausdorff measure.
The nonnegative form composes directly with Cauchy's projection formula.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallSphericalProjection.lean

complete

theorem ProbabilityTheory.ofReal_ballRadialProjectionTransform_le_normalizedHausdorff_lintegral
  {d : ℕ} (hd : 2 ≤ d) {f : ℝ → ℝ} (hF : Continuous f)
  (hfanti : AntitoneOn f (Set.Ici 0)) (hf : ∀ (x : ℝ), 0 ≤ f x) {r : ℝ}
  (hr : 0 ≤ r) {u w : EuclideanSpace ℝ (Fin d)} (hu : ‖u‖ = 1)
  (hw : ‖w‖ = 1) :
  ENNReal.ofReal
      (ProbabilityTheory.ballRadialProjectionTransform d f r) ≤
    ((ProbabilityTheory.standardSphereHausdorffMeasure d) Set.univ)⁻¹ *
      ∫⁻ (θ : ↑(Metric.sphere 0 1)),
        ENNReal.ofReal
            (ProbabilityTheory.ballSphericalRadialProfile f r
              |inner ℝ (↑θ) u|) *
          ENNReal.ofReal
            |inner ℝ (↑θ)
                w| ∂ProbabilityTheory.standardSphereHausdorffMeasure d

theorem ProbabilityTheory.ofReal_ballRadialProjectionTransform_le_normalizedHausdorff_lintegral
  {d : ℕ} (hd : 2 ≤ d) {f : ℝ → ℝ}
  (hF : Continuous f)
  (hfanti : AntitoneOn f (Set.Ici 0))
  (hf : ∀ (x : ℝ), 0 ≤ f x) {r : ℝ}
  (hr : 0 ≤ r)
  {u w : EuclideanSpace ℝ (Fin d)}
  (hu : ‖u‖ = 1) (hw : ‖w‖ = 1) :
  ENNReal.ofReal
      (ProbabilityTheory.ballRadialProjectionTransform
        d f r) ≤
    ((ProbabilityTheory.standardSphereHausdorffMeasure
            d)
          Set.univ)⁻¹ *
      ∫⁻ (θ : ↑(Metric.sphere 0 1)),
        ENNReal.ofReal
            (ProbabilityTheory.ballSphericalRadialProfile
              f r |inner ℝ (↑θ) u|) *
          ENNReal.ofReal
            |inner ℝ (↑θ)
                w| ∂ProbabilityTheory.standardSphereHausdorffMeasure
          d

Ball's radial projection transform is bounded by the normalized intrinsic-Hausdorff
spherical average in every unit direction.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallSphericalProjection.lean

complete

theorem ProbabilityTheory.ofReal_ballGaussianRadialDensity_le_normalizedHausdorff_lintegral
  {d : ℕ} (hd : 2 ≤ d) {r : ℝ} (hr : 0 ≤ r)
  {u w : EuclideanSpace ℝ (Fin d)} (hu : ‖u‖ = 1) (hw : ‖w‖ = 1) :
  ENNReal.ofReal
      (ProbabilityTheory.ballGaussianNormalization d *
        Real.exp (-r ^ 2 / 2)) ≤
    ((ProbabilityTheory.standardSphereHausdorffMeasure d) Set.univ)⁻¹ *
      ∫⁻ (θ : ↑(Metric.sphere 0 1)),
        ENNReal.ofReal
            (ProbabilityTheory.ballSphericalRadialProfile
              (ProbabilityTheory.ballRadialMajorant d) r
              |inner ℝ (↑θ) u|) *
          ENNReal.ofReal
            |inner ℝ (↑θ)
                w| ∂ProbabilityTheory.standardSphereHausdorffMeasure d

theorem ProbabilityTheory.ofReal_ballGaussianRadialDensity_le_normalizedHausdorff_lintegral
  {d : ℕ} (hd : 2 ≤ d) {r : ℝ}
  (hr : 0 ≤ r)
  {u w : EuclideanSpace ℝ (Fin d)}
  (hu : ‖u‖ = 1) (hw : ‖w‖ = 1) :
  ENNReal.ofReal
      (ProbabilityTheory.ballGaussianNormalization
          d *
        Real.exp (-r ^ 2 / 2)) ≤
    ((ProbabilityTheory.standardSphereHausdorffMeasure
            d)
          Set.univ)⁻¹ *
      ∫⁻ (θ : ↑(Metric.sphere 0 1)),
        ENNReal.ofReal
            (ProbabilityTheory.ballSphericalRadialProfile
              (ProbabilityTheory.ballRadialMajorant
                d)
              r |inner ℝ (↑θ) u|) *
          ENNReal.ofReal
            |inner ℝ (↑θ)
                w| ∂ProbabilityTheory.standardSphereHausdorffMeasure
          d

Ball's radial majorant makes the normalized spherical average dominate the radial standard
Gaussian density.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallSphericalProjection.lean

complete

theorem ProbabilityTheory.standardGaussianDensityReal_mul_norm_le_sphere_ballRadialMajorant_absInner
  {d : ℕ} (hd : 2 ≤ d) (x N : EuclideanSpace ℝ (Fin d)) :
  ENNReal.ofReal
      (ProbabilityTheory.standardGaussianDensityReal x * ‖N‖) ≤
    ((ProbabilityTheory.standardSphereHausdorffMeasure d) Set.univ)⁻¹ *
      ∫⁻ (θ : ↑(Metric.sphere 0 1)),
        ENNReal.ofReal
            (ProbabilityTheory.ballRadialMajorant d
              ‖(ℝ ∙ ↑θ)ᗮ.orthogonalProjectionOnto x‖) *
          ENNReal.ofReal
            |inner ℝ (↑θ)
                N| ∂ProbabilityTheory.standardSphereHausdorffMeasure d

theorem ProbabilityTheory.standardGaussianDensityReal_mul_norm_le_sphere_ballRadialMajorant_absInner
  {d : ℕ} (hd : 2 ≤ d)
  (x N : EuclideanSpace ℝ (Fin d)) :
  ENNReal.ofReal
      (ProbabilityTheory.standardGaussianDensityReal
          x *
        ‖N‖) ≤
    ((ProbabilityTheory.standardSphereHausdorffMeasure
            d)
          Set.univ)⁻¹ *
      ∫⁻ (θ : ↑(Metric.sphere 0 1)),
        ENNReal.ofReal
            (ProbabilityTheory.ballRadialMajorant
              d
              ‖(ℝ ∙
                        ↑θ)ᗮ.orthogonalProjectionOnto
                  x‖) *
          ENNReal.ofReal
            |inner ℝ (↑θ)
                N| ∂ProbabilityTheory.standardSphereHausdorffMeasure
          d

Ball's spherical projection inequality in the pointwise vector form used by the boundary
chart area formula.  The vector `N` need not be normalized: its norm is absorbed into the
absolute normal component under the spherical integral.

Ball (1993), derives the spherical density inequality in equation (3), applies Lemma 3 to reduce arbitrary position and normal directions to the orthogonal case, and rewrites that case as equation (4), printed pp. 416--417. Equations (5)--(7) construct the monotone radial majorant used here, printed pp. 417--418. The formal statement packages these steps in the pointwise vector form required by the boundary area formula.

Theorem2.5.9

Statement uses 2

Statement dependency previews

Preview

Theorem 2.5.2

Loading preview

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

used by 1✓L∃∀N

Tagsbentkusgaussian-geometryperimeterboundary-projectionsource-ball-1993fidelity-exact-normal-free-chart-form

Weighted boundary projection area and the factor-two line multiplicity. Let d\ge2, let C\subseteq\mathbb R^d be a compact convex body with nonempty interior, and let \theta\in S^{d-1}. There is a finite disjoint family of Lipschitz graph charts \varphi_j:T_j\to\partial C. For every nonnegative measurable w:\theta^\perp\to[0,\infty], \sum_j\int_{T_j} J_{d-1}(P_\theta\circ D\varphi_j(z))\, w(P_\theta\varphi_j(z))\,dz \le 2\int_{\theta^\perp}w(y)\,dy. The chart Jacobian is the normal-free representative of |\langle\theta,n_C\rangle|\,d\mathcal H^{d-1}. In particular, with Ball's radial majorant f_d, \sum_j\int_{T_j} J_{d-1}(P_\theta\circ D\varphi_j(z))\, f_d(\|P_\theta\varphi_j(z)\|)\,dz \le 4d^{1/4}.

Lean code for Theorem2.5.9●13 declarations

defdefined in ProbabilityApproximation/ConvexGeometry/BallProjectionArea.lean

complete

def ProbabilityTheory.ballBoundaryCoordinateDirection {d : ℕ} (i : Fin d) :
  EuclideanSpace ℝ (Fin d)

def ProbabilityTheory.ballBoundaryCoordinateDirection
  {d : ℕ} (i : Fin d) :
  EuclideanSpace ℝ (Fin d)

The standard coordinate direction used to choose finitely many boundary graph charts.

defdefined in ProbabilityApproximation/ConvexGeometry/BallProjectionArea.lean

complete

def ProbabilityTheory.ballBoundaryCoordinatePiece {d : ℕ}
  (C : Set (EuclideanSpace ℝ (Fin d))) (j : Fin d × Bool) :
  Set (EuclideanSpace ℝ (Fin d))

def ProbabilityTheory.ballBoundaryCoordinatePiece
  {d : ℕ}
  (C : Set (EuclideanSpace ℝ (Fin d)))
  (j : Fin d × Bool) :
  Set (EuclideanSpace ℝ (Fin d))

Disjointification of the finite coordinate graph cover in lexicographic chart order.

defdefined in ProbabilityApproximation/ConvexGeometry/BallProjectionArea.lean

complete

def ProbabilityTheory.ballBoundaryCoordinateChartDomain {d : ℕ}
  (C : Set (EuclideanSpace ℝ (Fin d))) (j : Fin d × Bool) :
  Set ↥(ℝ ∙ ProbabilityTheory.ballBoundaryCoordinateDirection j.1)ᗮ

def ProbabilityTheory.ballBoundaryCoordinateChartDomain
  {d : ℕ}
  (C : Set (EuclideanSpace ℝ (Fin d)))
  (j : Fin d × Bool) :
  Set
    ↥(ℝ ∙
          ProbabilityTheory.ballBoundaryCoordinateDirection
            j.1)ᗮ

The orthogonal-projection image serving as the source of one disjoint boundary chart.

defdefined in ProbabilityApproximation/ConvexGeometry/BallProjectionArea.lean

complete

def ProbabilityTheory.ballBoundaryCoordinateChart {d : ℕ}
  (C : Set (EuclideanSpace ℝ (Fin d))) (j : Fin d × Bool) :
  ↥(ℝ ∙ ProbabilityTheory.ballBoundaryCoordinateDirection j.1)ᗮ →
    EuclideanSpace ℝ (Fin d)

def ProbabilityTheory.ballBoundaryCoordinateChart
  {d : ℕ}
  (C : Set (EuclideanSpace ℝ (Fin d)))
  (j : Fin d × Bool) :
  ↥(ℝ ∙
          ProbabilityTheory.ballBoundaryCoordinateDirection
            j.1)ᗮ →
    EuclideanSpace ℝ (Fin d)

The inverse orthogonal-projection parameterization of one disjoint boundary chart.

defdefined in ProbabilityApproximation/ConvexGeometry/BallProjectionArea.lean

complete

def ProbabilityTheory.ballBoundaryCoordinateProjectedChart {d : ℕ}
  (C : Set (EuclideanSpace ℝ (Fin d))) (j : Fin d × Bool)
  (θ : EuclideanSpace ℝ (Fin d)) :
  ↥(ℝ ∙ ProbabilityTheory.ballBoundaryCoordinateDirection j.1)ᗮ →
    ↥(ℝ ∙ θ)ᗮ

def ProbabilityTheory.ballBoundaryCoordinateProjectedChart
  {d : ℕ}
  (C : Set (EuclideanSpace ℝ (Fin d)))
  (j : Fin d × Bool)
  (θ : EuclideanSpace ℝ (Fin d)) :
  ↥(ℝ ∙
          ProbabilityTheory.ballBoundaryCoordinateDirection
            j.1)ᗮ →
    ↥(ℝ ∙ θ)ᗮ

One disjoint boundary chart followed by orthogonal projection in an arbitrary direction.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallProjectionArea.lean

complete

theorem ProbabilityTheory.lintegral_ballBoundaryCoordinatePiece_eq_chart {d : ℕ}
  (hd : 2 ≤ d) {C : Set (EuclideanSpace ℝ (Fin d))}
  (hcompact : IsCompact C) (j : Fin d × Bool)
  (g : EuclideanSpace ℝ (Fin d) → ENNReal) (hg : Measurable g) :
  ∫⁻ (x : EuclideanSpace ℝ (Fin d)) in
      ProbabilityTheory.ballBoundaryCoordinatePiece C j,
      g x ∂MeasureTheory.Measure.euclideanHausdorffMeasure (d - 1) =
    ∫⁻ (z :
      ↥(ℝ ∙ ProbabilityTheory.ballBoundaryCoordinateDirection j.1)ᗮ) in
      ProbabilityTheory.ballBoundaryCoordinateChartDomain C j,
      ENNReal.ofReal
          (↑(fderivWithin ℝ
                (ProbabilityTheory.ballBoundaryCoordinateChart C j)
                (ProbabilityTheory.ballBoundaryCoordinateChartDomain C
                  j)
                z)).normDet *
        g (ProbabilityTheory.ballBoundaryCoordinateChart C j z)

theorem ProbabilityTheory.lintegral_ballBoundaryCoordinatePiece_eq_chart
  {d : ℕ} (hd : 2 ≤ d)
  {C : Set (EuclideanSpace ℝ (Fin d))}
  (hcompact : IsCompact C)
  (j : Fin d × Bool)
  (g : EuclideanSpace ℝ (Fin d) → ENNReal)
  (hg : Measurable g) :
  ∫⁻ (x : EuclideanSpace ℝ (Fin d)) in
      ProbabilityTheory.ballBoundaryCoordinatePiece
        C j,
      g
        x ∂MeasureTheory.Measure.euclideanHausdorffMeasure
        (d - 1) =
    ∫⁻ (z :
      ↥(ℝ ∙
            ProbabilityTheory.ballBoundaryCoordinateDirection
              j.1)ᗮ) in
      ProbabilityTheory.ballBoundaryCoordinateChartDomain
        C j,
      ENNReal.ofReal
          (↑(fderivWithin ℝ
                (ProbabilityTheory.ballBoundaryCoordinateChart
                  C j)
                (ProbabilityTheory.ballBoundaryCoordinateChartDomain
                  C j)
                z)).normDet *
        g
          (ProbabilityTheory.ballBoundaryCoordinateChart
            C j z)

Weighted area formula for one member of the disjoint finite boundary-chart cover.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallProjectionArea.lean

complete

theorem ProbabilityTheory.ae_exists_unit_normal_ballBoundaryCoordinateChart
  {d : ℕ} (hd : 2 ≤ d) {C : Set (EuclideanSpace ℝ (Fin d))}
  (hcompact : IsCompact C) (j : Fin d × Bool) :
  ∀ᵐ (z :
    ↥(ℝ ∙
          ProbabilityTheory.ballBoundaryCoordinateDirection
            j.1)ᗮ) ∂MeasureTheory.volume.restrict
      (ProbabilityTheory.ballBoundaryCoordinateChartDomain C j),
    ∃ u,
      ‖u‖ = 1 ∧
        (↑(fderivWithin ℝ
                  (ProbabilityTheory.ballBoundaryCoordinateChart C j)
                  (ProbabilityTheory.ballBoundaryCoordinateChartDomain C
                    j)
                  z)).range =
            (ℝ ∙ u)ᗮ ∧
          |inner ℝ
                    (ProbabilityTheory.ballBoundaryCoordinateDirection
                      j.1)
                    u| *
                (↑(fderivWithin ℝ
                      (ProbabilityTheory.ballBoundaryCoordinateChart C
                        j)
                      (ProbabilityTheory.ballBoundaryCoordinateChartDomain
                        C j)
                      z)).normDet =
              1 ∧
            ∀ (θ : EuclideanSpace ℝ (Fin d)),
              ‖θ‖ = 1 →
                (↑(ℝ ∙ θ)ᗮ.orthogonalProjectionOnto ∘ₗ
                      ↑(fderivWithin ℝ
                          (ProbabilityTheory.ballBoundaryCoordinateChart
                            C j)
                          (ProbabilityTheory.ballBoundaryCoordinateChartDomain
                            C j)
                          z)).normDet =
                  |inner ℝ θ u| *
                    (↑(fderivWithin ℝ
                          (ProbabilityTheory.ballBoundaryCoordinateChart
                            C j)
                          (ProbabilityTheory.ballBoundaryCoordinateChartDomain
                            C j)
                          z)).normDet

theorem ProbabilityTheory.ae_exists_unit_normal_ballBoundaryCoordinateChart
  {d : ℕ} (hd : 2 ≤ d)
  {C : Set (EuclideanSpace ℝ (Fin d))}
  (hcompact : IsCompact C)
  (j : Fin d × Bool) :
  ∀ᵐ (z :
    ↥(ℝ ∙
          ProbabilityTheory.ballBoundaryCoordinateDirection
            j.1)ᗮ) ∂MeasureTheory.volume.restrict
      (ProbabilityTheory.ballBoundaryCoordinateChartDomain
        C j),
    ∃ u,
      ‖u‖ = 1 ∧
        (↑(fderivWithin ℝ
                  (ProbabilityTheory.ballBoundaryCoordinateChart
                    C j)
                  (ProbabilityTheory.ballBoundaryCoordinateChartDomain
                    C j)
                  z)).range =
            (ℝ ∙ u)ᗮ ∧
          |inner ℝ
                    (ProbabilityTheory.ballBoundaryCoordinateDirection
                      j.1)
                    u| *
                (↑(fderivWithin ℝ
                      (ProbabilityTheory.ballBoundaryCoordinateChart
                        C j)
                      (ProbabilityTheory.ballBoundaryCoordinateChartDomain
                        C j)
                      z)).normDet =
              1 ∧
            ∀
              (θ :
                EuclideanSpace ℝ (Fin d)),
              ‖θ‖ = 1 →
                (↑(ℝ ∙
                              θ)ᗮ.orthogonalProjectionOnto ∘ₗ
                      ↑(fderivWithin ℝ
                          (ProbabilityTheory.ballBoundaryCoordinateChart
                            C j)
                          (ProbabilityTheory.ballBoundaryCoordinateChartDomain
                            C j)
                          z)).normDet =
                  |inner ℝ θ u| *
                    (↑(fderivWithin ℝ
                          (ProbabilityTheory.ballBoundaryCoordinateChart
                            C j)
                          (ProbabilityTheory.ballBoundaryCoordinateChartDomain
                            C j)
                          z)).normDet

Almost every point of a disjoint coordinate chart has a unit tangent normal.  Its normal
components in every projection direction are represented without choosing a measurable normal:
they are exactly the corresponding projected derivative Jacobians divided by the chart surface
Jacobian.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallProjectionArea.lean

complete

theorem ProbabilityTheory.exists_ballBoundaryCoordinateProjectedChart_multiplicity_partition
  {d : ℕ} (hd : 2 ≤ d) {C : Set (EuclideanSpace ℝ (Fin d))}
  (hcompact : IsCompact C) (j : Fin d × Bool)
  {θ : EuclideanSpace ℝ (Fin d)} (hθ : ‖θ‖ = 1)
  (w : ↥(ℝ ∙ θ)ᗮ → ENNReal) (hw : Measurable w) :
  ∃ p,
    (Pairwise fun m n => Disjoint (p m) (p n)) ∧
      (∀ (n : ℕ), MeasurableSet (p n)) ∧
        (∀ (n : ℕ),
            p n ⊆
              ProbabilityTheory.ballBoundaryCoordinateChartDomain C j) ∧
          (∀ (n : ℕ),
              Set.InjOn
                (ProbabilityTheory.ballBoundaryCoordinateProjectedChart
                  C j θ)
                (p n)) ∧
            (∀ (n : ℕ),
                MeasurableSet
                  (ProbabilityTheory.ballBoundaryCoordinateProjectedChart
                      C j θ ''
                    p n)) ∧
              (∀ᵐ (z :
                  ↥(ℝ ∙
                        ProbabilityTheory.ballBoundaryCoordinateDirection
                          j.1)ᗮ) ∂MeasureTheory.volume.restrict
                    (ProbabilityTheory.ballBoundaryCoordinateChartDomain
                      C j),
                  ENNReal.ofReal
                        (↑(ℝ ∙ θ)ᗮ.orthogonalProjectionOnto ∘ₗ
                            ↑(fderivWithin ℝ
                                (ProbabilityTheory.ballBoundaryCoordinateChart
                                  C j)
                                (ProbabilityTheory.ballBoundaryCoordinateChartDomain
                                  C j)
                                z)).normDet ≠
                      0 ↔
                    z ∈ ⋃ n, p n) ∧
                ∫⁻ (z :
                    ↥(ℝ ∙
                          ProbabilityTheory.ballBoundaryCoordinateDirection
                            j.1)ᗮ) in
                    ProbabilityTheory.ballBoundaryCoordinateChartDomain
                      C j,
                    ENNReal.ofReal
                        (↑(ℝ ∙ θ)ᗮ.orthogonalProjectionOnto ∘ₗ
                            ↑(fderivWithin ℝ
                                (ProbabilityTheory.ballBoundaryCoordinateChart
                                  C j)
                                (ProbabilityTheory.ballBoundaryCoordinateChartDomain
                                  C j)
                                z)).normDet *
                      w
                        (ProbabilityTheory.ballBoundaryCoordinateProjectedChart
                          C j θ z) =
                  ∫⁻ (y : ↥(ℝ ∙ θ)ᗮ),
                    ∑' (n : ℕ),
                      (ProbabilityTheory.ballBoundaryCoordinateProjectedChart
                              C j θ ''
                            p n).indicator
                        w y

theorem ProbabilityTheory.exists_ballBoundaryCoordinateProjectedChart_multiplicity_partition
  {d : ℕ} (hd : 2 ≤ d)
  {C : Set (EuclideanSpace ℝ (Fin d))}
  (hcompact : IsCompact C)
  (j : Fin d × Bool)
  {θ : EuclideanSpace ℝ (Fin d)}
  (hθ : ‖θ‖ = 1) (w : ↥(ℝ ∙ θ)ᗮ → ENNReal)
  (hw : Measurable w) :
  ∃ p,
    (Pairwise fun m n =>
        Disjoint (p m) (p n)) ∧
      (∀ (n : ℕ), MeasurableSet (p n)) ∧
        (∀ (n : ℕ),
            p n ⊆
              ProbabilityTheory.ballBoundaryCoordinateChartDomain
                C j) ∧
          (∀ (n : ℕ),
              Set.InjOn
                (ProbabilityTheory.ballBoundaryCoordinateProjectedChart
                  C j θ)
                (p n)) ∧
            (∀ (n : ℕ),
                MeasurableSet
                  (ProbabilityTheory.ballBoundaryCoordinateProjectedChart
                      C j θ ''
                    p n)) ∧
              (∀ᵐ (z :
                  ↥(ℝ ∙
                        ProbabilityTheory.ballBoundaryCoordinateDirection
                          j.1)ᗮ) ∂MeasureTheory.volume.restrict
                    (ProbabilityTheory.ballBoundaryCoordinateChartDomain
                      C j),
                  ENNReal.ofReal
                        (↑(ℝ ∙
                                    θ)ᗮ.orthogonalProjectionOnto ∘ₗ
                            ↑(fderivWithin
                                ℝ
                                (ProbabilityTheory.ballBoundaryCoordinateChart
                                  C j)
                                (ProbabilityTheory.ballBoundaryCoordinateChartDomain
                                  C j)
                                z)).normDet ≠
                      0 ↔
                    z ∈ ⋃ n, p n) ∧
                ∫⁻ (z :
                    ↥(ℝ ∙
                          ProbabilityTheory.ballBoundaryCoordinateDirection
                            j.1)ᗮ) in
                    ProbabilityTheory.ballBoundaryCoordinateChartDomain
                      C j,
                    ENNReal.ofReal
                        (↑(ℝ ∙
                                    θ)ᗮ.orthogonalProjectionOnto ∘ₗ
                            ↑(fderivWithin
                                ℝ
                                (ProbabilityTheory.ballBoundaryCoordinateChart
                                  C j)
                                (ProbabilityTheory.ballBoundaryCoordinateChartDomain
                                  C j)
                                z)).normDet *
                      w
                        (ProbabilityTheory.ballBoundaryCoordinateProjectedChart
                          C j θ z) =
                  ∫⁻ (y : ↥(ℝ ∙ θ)ᗮ),
                    ∑' (n : ℕ),
                      (ProbabilityTheory.ballBoundaryCoordinateProjectedChart
                              C j θ ''
                            p n).indicator
                        w y

Equal-rank area-with-multiplicity for one projected boundary chart, with the Jacobian written
as the projection composed with the original chart derivative.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallProjectionArea.lean

complete

theorem ProbabilityTheory.lintegral_frontier_eq_tsum_ballBoundaryCoordinateCharts
  {d : ℕ} (hd : 2 ≤ d) {C : Set (EuclideanSpace ℝ (Fin d))}
  (hC : Convexity.IsConvexSet ℝ C) (hcompact : IsCompact C)
  (hinterior : (interior C).Nonempty)
  (g : EuclideanSpace ℝ (Fin d) → ENNReal) (hg : Measurable g) :
  ∫⁻ (x : EuclideanSpace ℝ (Fin d)) in frontier C,
      g x ∂MeasureTheory.Measure.euclideanHausdorffMeasure (d - 1) =
    ∑' (j : Fin d × Bool),
      ∫⁻ (z :
        ↥(ℝ ∙
              ProbabilityTheory.ballBoundaryCoordinateDirection
                j.1)ᗮ) in
        ProbabilityTheory.ballBoundaryCoordinateChartDomain C j,
        ENNReal.ofReal
            (↑(fderivWithin ℝ
                  (ProbabilityTheory.ballBoundaryCoordinateChart C j)
                  (ProbabilityTheory.ballBoundaryCoordinateChartDomain C
                    j)
                  z)).normDet *
          g (ProbabilityTheory.ballBoundaryCoordinateChart C j z)

theorem ProbabilityTheory.lintegral_frontier_eq_tsum_ballBoundaryCoordinateCharts
  {d : ℕ} (hd : 2 ≤ d)
  {C : Set (EuclideanSpace ℝ (Fin d))}
  (hC : Convexity.IsConvexSet ℝ C)
  (hcompact : IsCompact C)
  (hinterior : (interior C).Nonempty)
  (g : EuclideanSpace ℝ (Fin d) → ENNReal)
  (hg : Measurable g) :
  ∫⁻ (x : EuclideanSpace ℝ (Fin d)) in
      frontier C,
      g
        x ∂MeasureTheory.Measure.euclideanHausdorffMeasure
        (d - 1) =
    ∑' (j : Fin d × Bool),
      ∫⁻ (z :
        ↥(ℝ ∙
              ProbabilityTheory.ballBoundaryCoordinateDirection
                j.1)ᗮ) in
        ProbabilityTheory.ballBoundaryCoordinateChartDomain
          C j,
        ENNReal.ofReal
            (↑(fderivWithin ℝ
                  (ProbabilityTheory.ballBoundaryCoordinateChart
                    C j)
                  (ProbabilityTheory.ballBoundaryCoordinateChartDomain
                    C j)
                  z)).normDet *
          g
            (ProbabilityTheory.ballBoundaryCoordinateChart
              C j z)

A compact full-dimensional convex boundary is the finite disjoint sum of its weighted
coordinate-chart area formulas.  The Jacobian field replaces any measurable choice of unit
normal in the subsequent spherical averaging argument.

defdefined in ProbabilityApproximation/ConvexGeometry/BallProjectionArea.lean

complete

def ProbabilityTheory.ballBoundaryProjectionFiber {d : ℕ}
  (C : Set (EuclideanSpace ℝ (Fin d))) (θ : EuclideanSpace ℝ (Fin d))
  (z : ↥(ℝ ∙ θ)ᗮ) : Set (EuclideanSpace ℝ (Fin d))

def ProbabilityTheory.ballBoundaryProjectionFiber
  {d : ℕ}
  (C : Set (EuclideanSpace ℝ (Fin d)))
  (θ : EuclideanSpace ℝ (Fin d))
  (z : ↥(ℝ ∙ θ)ᗮ) :
  Set (EuclideanSpace ℝ (Fin d))

The points of a convex boundary lying over one orthogonal-projection value.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallProjectionArea.lean

complete

theorem ProbabilityTheory.ae_encard_ballBoundaryProjectionFiber_le_two {d : ℕ}
  {C : Set (EuclideanSpace ℝ (Fin d))} (hC : Convexity.IsConvexSet ℝ C)
  (hcompact : IsCompact C) (hinterior : (interior C).Nonempty)
  (θ : EuclideanSpace ℝ (Fin d)) :
  ∀ᵐ (z : ↥(ℝ ∙ θ)ᗮ),
    (ProbabilityTheory.ballBoundaryProjectionFiber C θ z).encard ≤ 2

theorem ProbabilityTheory.ae_encard_ballBoundaryProjectionFiber_le_two
  {d : ℕ}
  {C : Set (EuclideanSpace ℝ (Fin d))}
  (hC : Convexity.IsConvexSet ℝ C)
  (hcompact : IsCompact C)
  (hinterior : (interior C).Nonempty)
  (θ : EuclideanSpace ℝ (Fin d)) :
  ∀ᵐ (z : ↥(ℝ ∙ θ)ᗮ),
    (ProbabilityTheory.ballBoundaryProjectionFiber
          C θ z).encard ≤
      2

For almost every projection value, a compact full-dimensional convex boundary has at most
two points in the corresponding projection fiber.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallProjectionArea.lean

complete

theorem ProbabilityTheory.tsum_lintegral_ballBoundaryCoordinateProjectedChart_le_two_mul
  {d : ℕ} (hd : 2 ≤ d) {C : Set (EuclideanSpace ℝ (Fin d))}
  (hC : Convexity.IsConvexSet ℝ C) (hcompact : IsCompact C)
  (hinterior : (interior C).Nonempty) {θ : EuclideanSpace ℝ (Fin d)}
  (hθ : ‖θ‖ = 1) (w : ↥(ℝ ∙ θ)ᗮ → ENNReal) (hw : Measurable w) :
  ∑' (j : Fin d × Bool),
      ∫⁻ (z :
        ↥(ℝ ∙
              ProbabilityTheory.ballBoundaryCoordinateDirection
                j.1)ᗮ) in
        ProbabilityTheory.ballBoundaryCoordinateChartDomain C j,
        ENNReal.ofReal
            (↑(ℝ ∙ θ)ᗮ.orthogonalProjectionOnto ∘ₗ
                ↑(fderivWithin ℝ
                    (ProbabilityTheory.ballBoundaryCoordinateChart C j)
                    (ProbabilityTheory.ballBoundaryCoordinateChartDomain
                      C j)
                    z)).normDet *
          w
            (ProbabilityTheory.ballBoundaryCoordinateProjectedChart C j
              θ z) ≤
    2 * ∫⁻ (y : ↥(ℝ ∙ θ)ᗮ), w y

theorem ProbabilityTheory.tsum_lintegral_ballBoundaryCoordinateProjectedChart_le_two_mul
  {d : ℕ} (hd : 2 ≤ d)
  {C : Set (EuclideanSpace ℝ (Fin d))}
  (hC : Convexity.IsConvexSet ℝ C)
  (hcompact : IsCompact C)
  (hinterior : (interior C).Nonempty)
  {θ : EuclideanSpace ℝ (Fin d)}
  (hθ : ‖θ‖ = 1) (w : ↥(ℝ ∙ θ)ᗮ → ENNReal)
  (hw : Measurable w) :
  ∑' (j : Fin d × Bool),
      ∫⁻ (z :
        ↥(ℝ ∙
              ProbabilityTheory.ballBoundaryCoordinateDirection
                j.1)ᗮ) in
        ProbabilityTheory.ballBoundaryCoordinateChartDomain
          C j,
        ENNReal.ofReal
            (↑(ℝ ∙
                        θ)ᗮ.orthogonalProjectionOnto ∘ₗ
                ↑(fderivWithin ℝ
                    (ProbabilityTheory.ballBoundaryCoordinateChart
                      C j)
                    (ProbabilityTheory.ballBoundaryCoordinateChartDomain
                      C j)
                    z)).normDet *
          w
            (ProbabilityTheory.ballBoundaryCoordinateProjectedChart
              C j θ z) ≤
    2 * ∫⁻ (y : ↥(ℝ ∙ θ)ᗮ), w y

Summing the projected Jacobians of all disjoint boundary charts costs at most two copies of
the target weight.  The factor two is the exact convex-line multiplicity; it is independent of
the number of coordinate charts.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallProjectionArea.lean

complete

theorem ProbabilityTheory.tsum_lintegral_ballBoundaryCoordinateProjectedChart_ballRadialMajorant_le
  {d : ℕ} (hd : 2 ≤ d) {C : Set (EuclideanSpace ℝ (Fin d))}
  (hC : Convexity.IsConvexSet ℝ C) (hcompact : IsCompact C)
  (hinterior : (interior C).Nonempty) {θ : EuclideanSpace ℝ (Fin d)}
  (hθ : ‖θ‖ = 1) :
  ∑' (j : Fin d × Bool),
      ∫⁻ (z :
        ↥(ℝ ∙
              ProbabilityTheory.ballBoundaryCoordinateDirection
                j.1)ᗮ) in
        ProbabilityTheory.ballBoundaryCoordinateChartDomain C j,
        ENNReal.ofReal
            (↑(ℝ ∙ θ)ᗮ.orthogonalProjectionOnto ∘ₗ
                ↑(fderivWithin ℝ
                    (ProbabilityTheory.ballBoundaryCoordinateChart C j)
                    (ProbabilityTheory.ballBoundaryCoordinateChartDomain
                      C j)
                    z)).normDet *
          ENNReal.ofReal
            (ProbabilityTheory.ballRadialMajorant d
              ‖ProbabilityTheory.ballBoundaryCoordinateProjectedChart C
                  j θ z‖) ≤
    ENNReal.ofReal (4 * ↑d ^ (1 / 4))

theorem ProbabilityTheory.tsum_lintegral_ballBoundaryCoordinateProjectedChart_ballRadialMajorant_le
  {d : ℕ} (hd : 2 ≤ d)
  {C : Set (EuclideanSpace ℝ (Fin d))}
  (hC : Convexity.IsConvexSet ℝ C)
  (hcompact : IsCompact C)
  (hinterior : (interior C).Nonempty)
  {θ : EuclideanSpace ℝ (Fin d)}
  (hθ : ‖θ‖ = 1) :
  ∑' (j : Fin d × Bool),
      ∫⁻ (z :
        ↥(ℝ ∙
              ProbabilityTheory.ballBoundaryCoordinateDirection
                j.1)ᗮ) in
        ProbabilityTheory.ballBoundaryCoordinateChartDomain
          C j,
        ENNReal.ofReal
            (↑(ℝ ∙
                        θ)ᗮ.orthogonalProjectionOnto ∘ₗ
                ↑(fderivWithin ℝ
                    (ProbabilityTheory.ballBoundaryCoordinateChart
                      C j)
                    (ProbabilityTheory.ballBoundaryCoordinateChartDomain
                      C j)
                    z)).normDet *
          ENNReal.ofReal
            (ProbabilityTheory.ballRadialMajorant
              d
              ‖ProbabilityTheory.ballBoundaryCoordinateProjectedChart
                  C j θ z‖) ≤
    ENNReal.ofReal (4 * ↑d ^ (1 / 4))

Fixed-direction projection bound with Ball's radial majorant and exact final constant.

Ball (1993), introduces the projected comparison measure in equation (2), printed p. 415, and observes that almost every line in a fixed direction meets the boundary of a convex body at most twice, yielding the factor 2, printed p. 416 in the proof of Theorem 4. The radial mass estimate \mu(\mathbb R^{d-1})\le2d^{1/4} is completed on printed pp. 418--419. The formal statement expresses the same projection argument through a finite disjoint chart cover and the equal-rank area formula, avoiding any measurable choice of an outward normal.

Theorem2.5.10

Statement uses 3

Statement dependency previews

Preview

Theorem 2.4.4

Loading preview

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

used by 1✓L∃∀N

Tagsbentkusgaussian-geometryperimetersource-ball-1993fidelity-domain-completed-exact-constant

Ball's Gaussian perimeter theorem. Let d\ge2 and let C\subseteq\mathbb R^d be convex. With P_\gamma(C)=\int_{\partial C}(2\pi)^{-d/2}e^{-\|x\|^2/2}\, d\mathcal H^{d-1}(x), \qquad K_d=4d^{1/4}, one has P_\gamma(C)\le K_d. The conclusion holds without assuming that C is closed, bounded, or full-dimensional. For a compact convex body with nonempty interior it follows from the spherical density and boundary projection estimates above; closure, increasing compact truncation, affine slicing, and the empty-interior case complete the domain.

Lean code for Theorem2.5.10●6 theorems

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallGaussianPerimeter.lean

complete

theorem ProbabilityTheory.standardGaussianBoundaryContent_le_one_of_interior_eq_empty
  {d : ℕ} {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) (hempty : interior s = ∅) :
  ProbabilityTheory.standardGaussianBoundaryContent s ≤ 1

theorem ProbabilityTheory.standardGaussianBoundaryContent_le_one_of_interior_eq_empty
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s)
  (hempty : interior s = ∅) :
  ProbabilityTheory.standardGaussianBoundaryContent
      s ≤
    1

A convex set with empty ambient interior has Gaussian boundary content at most one.  This
includes the empty set and every lower-dimensional, unbounded, or nonclosed convex set.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallGaussianPerimeter.lean

complete

theorem ProbabilityTheory.standardGaussianBoundaryContent_le_of_isBounded_case
  {d : ℕ} {s : Set (EuclideanSpace ℝ (Fin d))} {K : ENNReal}
  (hs : Convexity.IsConvexSet ℝ s) (hne : (interior s).Nonempty)
  (hbounded :
    ∀ (t : Set (EuclideanSpace ℝ (Fin d))),
      Convexity.IsConvexSet ℝ t →
        (interior t).Nonempty →
          Bornology.IsBounded t →
            ProbabilityTheory.standardGaussianBoundaryContent t ≤ K) :
  ProbabilityTheory.standardGaussianBoundaryContent s ≤ K

theorem ProbabilityTheory.standardGaussianBoundaryContent_le_of_isBounded_case
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  {K : ENNReal}
  (hs : Convexity.IsConvexSet ℝ s)
  (hne : (interior s).Nonempty)
  (hbounded :
    ∀
      (t :
        Set (EuclideanSpace ℝ (Fin d))),
      Convexity.IsConvexSet ℝ t →
        (interior t).Nonempty →
          Bornology.IsBounded t →
            ProbabilityTheory.standardGaussianBoundaryContent
                t ≤
              K) :
  ProbabilityTheory.standardGaussianBoundaryContent
      s ≤
    K

It is enough to prove a uniform Gaussian boundary-content estimate for bounded convex sets
with nonempty interior.  Intersect an arbitrary convex set with an increasing sequence of balls
centred at an interior point.  Inside each ball the original frontier is contained in the
frontier of the bounded truncation, and the original frontier is the directed union of these
pieces.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallGaussianPerimeter.lean

complete

theorem ProbabilityTheory.standardGaussianBoundaryContent_le_of_convexBody_case_all
  {d : ℕ} {s : Set (EuclideanSpace ℝ (Fin d))} {K : ENNReal}
  (hs : Convexity.IsConvexSet ℝ s) (hK : 1 ≤ K)
  (hbody :
    ∀ (t : Set (EuclideanSpace ℝ (Fin d))),
      Convexity.IsConvexSet ℝ t →
        (interior t).Nonempty →
          IsCompact t →
            ProbabilityTheory.standardGaussianBoundaryContent t ≤ K) :
  ProbabilityTheory.standardGaussianBoundaryContent s ≤ K

theorem ProbabilityTheory.standardGaussianBoundaryContent_le_of_convexBody_case_all
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  {K : ENNReal}
  (hs : Convexity.IsConvexSet ℝ s)
  (hK : 1 ≤ K)
  (hbody :
    ∀
      (t :
        Set (EuclideanSpace ℝ (Fin d))),
      Convexity.IsConvexSet ℝ t →
        (interior t).Nonempty →
          IsCompact t →
            ProbabilityTheory.standardGaussianBoundaryContent
                t ≤
              K) :
  ProbabilityTheory.standardGaussianBoundaryContent
      s ≤
    K

Domain completion for Ball's theorem.  If a constant `K ≥ 1` bounds Gaussian boundary
content on convex bodies, then it bounds every convex set.  Empty-interior sets use the exact
lower-dimensional estimate; full-dimensional sets use truncation and closure.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallGaussianPerimeter.lean

complete

theorem ProbabilityTheory.standardGaussianBoundaryContent_le_ballGaussianPerimeterConstant_of_convexBody_case
  {d : ℕ} (hd : 2 ≤ d) {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s)
  (hbody :
    ∀ (t : Set (EuclideanSpace ℝ (Fin d))),
      Convexity.IsConvexSet ℝ t →
        (interior t).Nonempty →
          IsCompact t →
            ProbabilityTheory.standardGaussianBoundaryContent t ≤
              ENNReal.ofReal
                (ProbabilityTheory.ballGaussianPerimeterConstant d)) :
  ProbabilityTheory.standardGaussianBoundaryContent s ≤
    ENNReal.ofReal (ProbabilityTheory.ballGaussianPerimeterConstant d)

theorem ProbabilityTheory.standardGaussianBoundaryContent_le_ballGaussianPerimeterConstant_of_convexBody_case
  {d : ℕ} (hd : 2 ≤ d)
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s)
  (hbody :
    ∀
      (t :
        Set (EuclideanSpace ℝ (Fin d))),
      Convexity.IsConvexSet ℝ t →
        (interior t).Nonempty →
          IsCompact t →
            ProbabilityTheory.standardGaussianBoundaryContent
                t ≤
              ENNReal.ofReal
                (ProbabilityTheory.ballGaussianPerimeterConstant
                  d)) :
  ProbabilityTheory.standardGaussianBoundaryContent
      s ≤
    ENNReal.ofReal
      (ProbabilityTheory.ballGaussianPerimeterConstant
        d)

Ball's Gaussian boundary-content theorem reduces, without changing the public constant or
the domain, to the compact full-dimensional convex-body projection theorem in dimension at least
two.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallGaussianPerimeter.lean

complete

theorem ProbabilityTheory.standardGaussianBoundaryContent_le_ballGaussianPerimeterConstant_compactBody
  {d : ℕ} (hd : 2 ≤ d) {C : Set (EuclideanSpace ℝ (Fin d))}
  (hC : Convexity.IsConvexSet ℝ C) (hcompact : IsCompact C)
  (hinterior : (interior C).Nonempty) :
  ProbabilityTheory.standardGaussianBoundaryContent C ≤
    ENNReal.ofReal (ProbabilityTheory.ballGaussianPerimeterConstant d)

theorem ProbabilityTheory.standardGaussianBoundaryContent_le_ballGaussianPerimeterConstant_compactBody
  {d : ℕ} (hd : 2 ≤ d)
  {C : Set (EuclideanSpace ℝ (Fin d))}
  (hC : Convexity.IsConvexSet ℝ C)
  (hcompact : IsCompact C)
  (hinterior : (interior C).Nonempty) :
  ProbabilityTheory.standardGaussianBoundaryContent
      C ≤
    ENNReal.ofReal
      (ProbabilityTheory.ballGaussianPerimeterConstant
        d)

Ball's Gaussian perimeter estimate for the compact full-dimensional source domain of the
projection argument.

theoremdefined in ProbabilityApproximation/ConvexGeometry/BallGaussianPerimeter.lean

complete

theorem ProbabilityTheory.standardGaussianBoundaryContent_le_ballGaussianPerimeterConstant
  {d : ℕ} (hd : 2 ≤ d) {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) :
  ProbabilityTheory.standardGaussianBoundaryContent s ≤
    ENNReal.ofReal (ProbabilityTheory.ballGaussianPerimeterConstant d)

theorem ProbabilityTheory.standardGaussianBoundaryContent_le_ballGaussianPerimeterConstant
  {d : ℕ} (hd : 2 ≤ d)
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) :
  ProbabilityTheory.standardGaussianBoundaryContent
      s ≤
    ENNReal.ofReal
      (ProbabilityTheory.ballGaussianPerimeterConstant
        d)

Ball's boundary-content theorem for every convex set in dimension at least two.

This is Ball (1993), Theorem 4, printed pp. 415--419, with its explicit constant 4d^{1/4}. Ball states the theorem for convex bodies. The formal theorem retains that source theorem as the compact full-dimensional core and extends it to every convex set by the exact boundary-content reductions described in the statement; the codimension-one case uses normalized affine slicing, while higher-codimension boundaries have zero \mathcal H^{d-1} measure.

Theorem2.5.11

Statement uses 2

Statement dependency previews

Preview

Theorem 2.4.7

Loading preview

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

used by 1✓L∃∀N

Tagsbentkusgaussian-geometryperimetershellssource-ball-1993source-raic-2019fidelity-explicit-constant-all-dimensions

Explicit Gaussian shell bounds for convex sets. Let d\in\mathbb N, let A\subseteq\mathbb R^d be convex, and let \varepsilon\ge0. Put K_d=4d^{1/4} and let \gamma_d be standard Gaussian measure. Then \gamma_d\!\left(\{x:d(x,\overline A)\le\varepsilon\}\setminus A\right) \le K_d\varepsilon, and, with open balls in the inner core, \gamma_d\!\left(A\setminus \{x:B(x,\varepsilon)\subseteq A\}\right) \le K_d\varepsilon. These statements include dimensions zero and one as well as empty, full, unbounded, and lower-dimensional convex sets.

Lean code for Theorem2.5.11●3 theorems

theoremdefined in ProbabilityApproximation/ConvexGeometry/GaussianShellCoarea.lean

complete

theorem ProbabilityTheory.stdGaussian_shell_pair_le_ball_of_boundaryContent_all
  {d : ℕ} {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ} (hε : 0 ≤ ε)
  (hboundary :
    2 ≤ d →
      ∀ (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_all
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ}
  (hε : 0 ≤ ε)
  (hboundary :
    2 ≤ d →
      ∀
        (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 dimension-at-least-two Gaussian boundary-content estimate for convex sets implies the
Bentkus shell bound for every convex set, including the empty set, the whole space, and dimensions
zero and one.

theoremdefined in ProbabilityApproximation/ConvexGeometry/GaussianShellCoarea.lean

complete

theorem ProbabilityTheory.stdGaussian_shell_pair_le_ball_of_convexBody_boundaryContent
  {d : ℕ} {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ} (hε : 0 ≤ ε)
  (hbody :
    2 ≤ d →
      ∀ (t : Set (EuclideanSpace ℝ (Fin d))),
        Convexity.IsConvexSet ℝ t →
          (interior t).Nonempty →
            IsCompact 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_convexBody_boundaryContent
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ}
  (hε : 0 ≤ ε)
  (hbody :
    2 ≤ d →
      ∀
        (t :
          Set (EuclideanSpace ℝ (Fin d))),
        Convexity.IsConvexSet ℝ t →
          (interior t).Nonempty →
            IsCompact 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 compact full-dimensional convex-body boundary-content estimate in dimensions at least two
implies the Bentkus shell bound for every convex set and every finite dimension.

theoremdefined in ProbabilityApproximation/ConvexGeometry/GaussianShellCoarea.lean

complete

theorem ProbabilityTheory.stdGaussian_shell_pair_le_ball {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))} (hs : Convexity.IsConvexSet ℝ s)
  {ε : ℝ} (hε : 0 ≤ ε) :
  (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
  {d : ℕ}
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ}
  (hε : 0 ≤ ε) :
  (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 *
        ε

Ball's explicit outer and inner Gaussian shell bounds for every finite-dimensional convex set.
The constant is `4 * d ^ (1 / 4)`, including the empty set, the whole space, unbounded and
lower-dimensional convex sets, and dimensions zero and one.

Ball (1993), Theorem 4, printed pp. 415--419, supplies the boundary-content constant in dimensions at least two. Raič (2019), Proposition 3.1 and its proof, printed pp. 2843--2845, derive the outer and inner shell integrals from Gaussian boundary content by signed-distance coarea. Bentkus (2004), uses the resulting O(d^{1/4}\varepsilon) estimate as equation (1.4), printed p. 401. The formal theorem keeps the exact half-open boundary conventions and supplies the elementary zero- and one-dimensional endpoints.