Theorems · Theorem · measure theory

EuclideanGeometry.euclideanHausdorffMeasure_eq_lintegral

∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
  [inst_2 : MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] [inst_5 : MetricSpace P]
  [inst_6 : MeasurableSpace P] [inst_7 : BorelSpace P] [inst_8 : NormedAddTorsor V P] (p : P) {v : V},
  v ≠ 0 →
    ∀ {t : Set P},
      MeasurableSet t →
        (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ V)) t =
          ‖v‖ₑ *
            ∫⁻ (x : ℝ),
              (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ V - 1))
                (t ∩ ↑(AffineSubspace.mk' (x • v +ᵥ p) (ℝ ∙ v)ᗮ))

The $n$-dimensional volume of an object in an $n$-dimensional space is equal to the integral of the volume of $(n-1)$-dimensional orthogonal cross-section along a line defined by a direction vector. This is a special case of AffineSubspace.euclideanHausdorffMeasure_eq_lintegral with a one-dimensional subspace.

Defined in

Mathlib.Geometry.Euclidean.Volume.Measure

Cited by

0 results in Mathlib

Foundations

Depth 286 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceMeasurableSpaceBorelSpaceFiniteDimensionalMetricSpaceMeasurableSpaceBorelSpaceNormedAddTorsor