Theorems · Definition · measure theory

Submodule.measurableEquivProd

{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] →
                  [BorelSpace P] → [NormedAddTorsor V P] → (s : Submodule ℝ V) → P → P ≃ᵐ ↥s × ↥sᗮ

A measurable equivalence between an affine space and its orthogonal decomposition by a base point and a direction. We show that this is measure preserving between μHE[finrank ℝ V] and volume at Submodule.measurePreserving_measurableEquivProd. This is similar to Submodule.orthogonalDecomposition as a MeasurableEquiv, but as the right-hand side is not with L²-norm, this is not an isometry.

Defined in

Mathlib.Geometry.Euclidean.Volume.Measure

Cited by

5 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMeasurableSpaceBorelSpaceFiniteDimensionalMetricSpaceMeasurableSpaceBorelSpaceNormedAddTorsor