volume_euclideanSpace_eq_dirac — Mathlib

English

In the empty index case, the volume on Euclidean space equals the Dirac measure at 0.

Русский

В случае пустого индекса объём на Евклидовом пространстве равен мере-dirac в нуле.

LaTeX

$$$\\mathrm{volume}(\\mathrm{EuclideanSpace}_\\mathbb{R} \\text{ with empty indices}) = \\mathrm{dirac}_0$.$$

Lean4

theorem volume_euclideanSpace_eq_dirac [IsEmpty ι] : (volume : Measure (EuclideanSpace ℝ ι)) = Measure.dirac 0 := by
  rw [← ((EuclideanSpace.volume_preserving_measurableEquiv ι).symm).map_eq, volume_pi_eq_dirac 0,
    map_dirac (MeasurableEquiv.measurable _), EuclideanSpace.coe_measurableEquiv_symm, WithLp.toLp_zero]

Похожие утверждения