5.7. Mathlib candidates: invariant geometry and integration🔗

The orthogonal group, invariant measures on Stiefel manifolds and spheres, the matrix polar formula, the codimension-one specialization, singular value decomposition, and Haar measure on the unit group of a finite-dimensional algebra and on a semidirect product.

The orthogonal group and the Stiefel manifold

Theorem5.7.1

uses 1

Used by 3

Reverse dependency previews

Preview

Theorem 5.7.2

Loading preview

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

✓L∃∀N

The orthogonal group is a compact group, and the Stiefel manifold carries an invariant measure. Mathlib has the orthogonal group only as linear algebra — Matrix.orthogonalGroup is a submonoid of matrices with no topology, no compactness and no measure — but it does have the unitary group of a C*-algebra as a topological group whenever the star operation is continuous, and it identifies the elements of unitary (E →L[𝕜] E) with the linear isometry equivalences of E. That is the orthogonal group in coordinate-free form, and what is missing from it is supplied here: the adjoint is continuous because it is an isometry, so the group is topological; a unitary has operator norm at most one, so the group is bounded; it is closed, and in finite dimensions the operator space is proper, so it is compact by Heine--Borel; hence it carries a Haar measure, which is a probability measure because the group is compact.

Lean code for Theorem5.7.1●21 declarations

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalGroup.lean

complete

theorem ContinuousLinearMap.instContinuousStar.{u_1, u_2} {𝕜 : Type u_1}
  {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E]
  [InnerProductSpace 𝕜 E] [CompleteSpace E] : ContinuousStar (E →L[𝕜] E)

theorem ContinuousLinearMap.instContinuousStar.{u_1,
    u_2}
  {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E]
  [InnerProductSpace 𝕜 E]
  [CompleteSpace E] :
  ContinuousStar (E →L[𝕜] E)

The adjoint is continuous: it is an isometric equivalence of the operator space with itself.
Together with Mathlib's `IsTopologicalGroup (unitary R)` for a topological star monoid `R`, this is
what makes the unitary group of `E →L[𝕜] E` a topological group.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalGroup.lean

complete

theorem ContinuousLinearMap.norm_le_one_of_mem_unitary.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  {u : E →L[ℝ] E} (hu : u ∈ unitary (E →L[ℝ] E)) : ‖u‖ ≤ 1

theorem ContinuousLinearMap.norm_le_one_of_mem_unitary.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] {u : E →L[ℝ] E}
  (hu : u ∈ unitary (E →L[ℝ] E)) : ‖u‖ ≤ 1

A unitary operator has operator norm at most one — exactly one unless the space is trivial, but
the inequality is what boundedness of the unitary group needs.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalGroup.lean

complete

theorem ContinuousLinearMap.isCompact_unitary.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] : IsCompact ↑(unitary (E →L[ℝ] E))

theorem ContinuousLinearMap.isCompact_unitary.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] :
  IsCompact ↑(unitary (E →L[ℝ] E))

**The orthogonal group of a finite-dimensional real inner product space is compact.** It is
closed because the defining equations are closed conditions and the star operation is continuous,
and bounded because a unitary has operator norm at most one; in finite dimensions the operator space
is proper, so Heine--Borel applies.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalGroup.lean

complete

theorem ContinuousLinearMap.instCompactSpaceUnitary.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] : CompactSpace ↥(unitary (E →L[ℝ] E))

theorem ContinuousLinearMap.instCompactSpaceUnitary.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] :
  CompactSpace ↥(unitary (E →L[ℝ] E))

defdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalGroup.lean

complete

def ContinuousLinearMap.orthogonalHaar.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] : MeasureTheory.Measure ↥(unitary (E →L[ℝ] E))

def ContinuousLinearMap.orthogonalHaar.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] :
  MeasureTheory.Measure
    ↥(unitary (E →L[ℝ] E))

Implementation after :=

:= Measure.haarMeasure ⊤

**The Haar probability measure on the orthogonal group.** The group is compact, so the Haar
measure normalized on the whole group is a probability measure, and that is the normalization an
invariant measure on a Stiefel manifold is built from.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalGroup.lean

complete

theorem ContinuousLinearMap.instIsProbabilityMeasureOrthogonalHaar.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] :
  MeasureTheory.IsProbabilityMeasure ContinuousLinearMap.orthogonalHaar

theorem ContinuousLinearMap.instIsProbabilityMeasureOrthogonalHaar.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] :
  MeasureTheory.IsProbabilityMeasure
    ContinuousLinearMap.orthogonalHaar

defdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalGroup.lean

complete

def ContinuousLinearMap.instTopologicalSpaceLinearIsometry.{u_1, u_2}
  {F : Type u_1} {E : Type u_2} [NormedAddCommGroup F]
  [InnerProductSpace ℝ F] [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] : TopologicalSpace (F →ₗᵢ[ℝ] E)

def ContinuousLinearMap.instTopologicalSpaceLinearIsometry.{u_1,
    u_2}
  {F : Type u_1} {E : Type u_2}
  [NormedAddCommGroup F]
  [InnerProductSpace ℝ F]
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] :
  TopologicalSpace (F →ₗᵢ[ℝ] E)

Implementation after :=

:=
  TopologicalSpace.induced LinearIsometry.toContinuousLinearMap inferInstance

The operator-norm topology on the space of linear isometries, induced from the continuous linear
maps. Mathlib gives `LinearIsometry` no topology, and the Stiefel manifold of orthonormal `k`-frames
in `E` is exactly `ℝ^k →ₗᵢ[ℝ] E`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalGroup.lean

complete

theorem ContinuousLinearMap.continuous_toContinuousLinearMap.{u_1, u_2}
  {F : Type u_1} {E : Type u_2} [NormedAddCommGroup F]
  [InnerProductSpace ℝ F] [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] :
  Continuous LinearIsometry.toContinuousLinearMap

theorem ContinuousLinearMap.continuous_toContinuousLinearMap.{u_1,
    u_2}
  {F : Type u_1} {E : Type u_2}
  [NormedAddCommGroup F]
  [InnerProductSpace ℝ F]
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] :
  Continuous
    LinearIsometry.toContinuousLinearMap

defdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalGroup.lean

complete

def ContinuousLinearMap.unitaryIsometry.{u_2} {E : Type u_2}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (Q : ↥(unitary (E →L[ℝ] E))) : E →ₗᵢ[ℝ] E

def ContinuousLinearMap.unitaryIsometry.{u_2}
  {E : Type u_2} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (Q : ↥(unitary (E →L[ℝ] E))) :
  E →ₗᵢ[ℝ] E

Implementation after :=

:= (Q : E →L[ℝ] E).toLinearMap
  norm_map' x := (Q : E →L[ℝ] E).norm_map_of_mem_unitary Q.property x

A unitary operator read as a linear isometry of `E`.

defdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalGroup.lean

complete

def ContinuousLinearMap.stiefelAct.{u_1, u_2} {F : Type u_1} {E : Type u_2}
  [NormedAddCommGroup F] [InnerProductSpace ℝ F] [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (Q : ↥(unitary (E →L[ℝ] E))) (L : F →ₗᵢ[ℝ] E) : F →ₗᵢ[ℝ] E

def ContinuousLinearMap.stiefelAct.{u_1, u_2}
  {F : Type u_1} {E : Type u_2}
  [NormedAddCommGroup F]
  [InnerProductSpace ℝ F]
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (Q : ↥(unitary (E →L[ℝ] E)))
  (L : F →ₗᵢ[ℝ] E) : F →ₗᵢ[ℝ] E

Implementation after :=

:=
  (unitaryIsometry Q).comp L

The action of the orthogonal group of `E` on the Stiefel manifold of frames `F →ₗᵢ[ℝ] E`, by
post-composition. It is transitive on frames of a fixed dimension, which is why the pushforward of
the Haar measure along it does not depend on the frame chosen — a fact this file does not need and
does not prove.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalGroup.lean

complete

theorem ContinuousLinearMap.stiefelAct_mul.{u_1, u_2} {F : Type u_1}
  {E : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (Q Q' : ↥(unitary (E →L[ℝ] E))) (L : F →ₗᵢ[ℝ] E) :
  ContinuousLinearMap.stiefelAct (Q * Q') L =
    ContinuousLinearMap.stiefelAct Q
      (ContinuousLinearMap.stiefelAct Q' L)

theorem ContinuousLinearMap.stiefelAct_mul.{u_1,
    u_2}
  {F : Type u_1} {E : Type u_2}
  [NormedAddCommGroup F]
  [InnerProductSpace ℝ F]
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (Q Q' : ↥(unitary (E →L[ℝ] E)))
  (L : F →ₗᵢ[ℝ] E) :
  ContinuousLinearMap.stiefelAct (Q * Q')
      L =
    ContinuousLinearMap.stiefelAct Q
      (ContinuousLinearMap.stiefelAct Q'
        L)

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalGroup.lean

complete

theorem ContinuousLinearMap.continuous_stiefelAct_left.{u_1, u_2} {F : Type u_1}
  {E : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (L : F →ₗᵢ[ℝ] E) :
  Continuous fun Q ↦ ContinuousLinearMap.stiefelAct Q L

theorem ContinuousLinearMap.continuous_stiefelAct_left.{u_1,
    u_2}
  {F : Type u_1} {E : Type u_2}
  [NormedAddCommGroup F]
  [InnerProductSpace ℝ F]
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (L : F →ₗᵢ[ℝ] E) :
  Continuous fun Q ↦
    ContinuousLinearMap.stiefelAct Q L

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalGroup.lean

complete

theorem ContinuousLinearMap.continuous_stiefelAct_right.{u_1, u_2}
  {F : Type u_1} {E : Type u_2} [NormedAddCommGroup F]
  [InnerProductSpace ℝ F] [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (Q : ↥(unitary (E →L[ℝ] E))) :
  Continuous (ContinuousLinearMap.stiefelAct Q)

theorem ContinuousLinearMap.continuous_stiefelAct_right.{u_1,
    u_2}
  {F : Type u_1} {E : Type u_2}
  [NormedAddCommGroup F]
  [InnerProductSpace ℝ F]
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (Q : ↥(unitary (E →L[ℝ] E))) :
  Continuous
    (ContinuousLinearMap.stiefelAct Q)

defdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalGroup.lean

complete

def ContinuousLinearMap.stiefelMeasure.{u_1, u_2} {F : Type u_1}
  {E : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (L : F →ₗᵢ[ℝ] E) : MeasureTheory.Measure (F →ₗᵢ[ℝ] E)

def ContinuousLinearMap.stiefelMeasure.{u_1,
    u_2}
  {F : Type u_1} {E : Type u_2}
  [NormedAddCommGroup F]
  [InnerProductSpace ℝ F]
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (L : F →ₗᵢ[ℝ] E) :
  MeasureTheory.Measure (F →ₗᵢ[ℝ] E)

Implementation after :=

:=
  Measure.map (fun Q => stiefelAct Q L) orthogonalHaar

**The invariant measure on the Stiefel manifold of orthonormal frames**, the pushforward of the
Haar probability measure of the orthogonal group along its action on a fixed frame.

Building it this way makes invariance true by construction — see
`ContinuousLinearMap.map_stiefelAct_stiefelMeasure` — rather than something to be recovered from a
uniqueness theorem, which is what a construction by iterated sphere measures would need.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalGroup.lean

complete

theorem ContinuousLinearMap.map_stiefelAct_stiefelMeasure.{u_1, u_2}
  {F : Type u_1} {E : Type u_2} [NormedAddCommGroup F]
  [InnerProductSpace ℝ F] [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (Q : ↥(unitary (E →L[ℝ] E)))
  (L : F →ₗᵢ[ℝ] E) :
  MeasureTheory.Measure.map (ContinuousLinearMap.stiefelAct Q)
      (ContinuousLinearMap.stiefelMeasure L) =
    ContinuousLinearMap.stiefelMeasure L

theorem ContinuousLinearMap.map_stiefelAct_stiefelMeasure.{u_1,
    u_2}
  {F : Type u_1} {E : Type u_2}
  [NormedAddCommGroup F]
  [InnerProductSpace ℝ F]
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (Q : ↥(unitary (E →L[ℝ] E)))
  (L : F →ₗᵢ[ℝ] E) :
  MeasureTheory.Measure.map
      (ContinuousLinearMap.stiefelAct Q)
      (ContinuousLinearMap.stiefelMeasure
        L) =
    ContinuousLinearMap.stiefelMeasure L

**The Stiefel measure is invariant under the orthogonal group.** This is the property the
construction was chosen for, and the proof is left invariance of the Haar measure: acting by `Q` on
the pushforward along `Q' ↦ Q' L` is the pushforward along `Q' ↦ (Q Q') L`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalGroup.lean

complete

theorem ContinuousLinearMap.instIsMulRightInvariantOrthogonalHaar.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] :
  ContinuousLinearMap.orthogonalHaar.IsMulRightInvariant

theorem ContinuousLinearMap.instIsMulRightInvariantOrthogonalHaar.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] :
  ContinuousLinearMap.orthogonalHaar.IsMulRightInvariant

**The orthogonal group is unimodular**: its Haar measure is right invariant as well as left
invariant. Mathlib derives right invariance from left invariance only for abelian groups; here it
comes from compactness. Right translation of a left invariant measure is again left invariant, so by
uniqueness it is a scalar multiple of the Haar measure, and the scalar is the total mass, which is
`1` on both sides because the group is compact.

defdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalGroup.lean

complete

def ContinuousLinearMap.isometryEquivOfIsometry.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (T : E →ₗᵢ[ℝ] E) : E ≃ₗᵢ[ℝ] E

def ContinuousLinearMap.isometryEquivOfIsometry.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (T : E →ₗᵢ[ℝ] E) : E ≃ₗᵢ[ℝ] E

Implementation after :=

:=
  LinearIsometryEquiv.ofSurjective T
    ((LinearMap.injective_iff_surjective (f := T.toLinearMap)).mp T.injective)

A linear isometry of a finite-dimensional space into itself is an isometric equivalence, since
an injective endomorphism of a finite-dimensional space is surjective.

defdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalGroup.lean

complete

def ContinuousLinearMap.unitaryOfIsometryEquiv.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (e : E ≃ₗᵢ[ℝ] E) : ↥(unitary (E →L[ℝ] E))

def ContinuousLinearMap.unitaryOfIsometryEquiv.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (e : E ≃ₗᵢ[ℝ] E) :
  ↥(unitary (E →L[ℝ] E))

Implementation after :=

:=
  Unitary.linearIsometryEquiv.symm e

An isometric equivalence of `E`, read as an element of the orthogonal group.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalGroup.lean

complete

theorem ContinuousLinearMap.exists_stiefelAct_eq.{u_1, u_2} {F : Type u_1}
  {E : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (L L' : F →ₗᵢ[ℝ] E) : ∃ Q, ContinuousLinearMap.stiefelAct Q L = L'

theorem ContinuousLinearMap.exists_stiefelAct_eq.{u_1,
    u_2}
  {F : Type u_1} {E : Type u_2}
  [NormedAddCommGroup F]
  [InnerProductSpace ℝ F]
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (L L' : F →ₗᵢ[ℝ] E) :
  ∃ Q,
    ContinuousLinearMap.stiefelAct Q L =
      L'

**The orthogonal group acts transitively on frames.** Two linear isometries of `F` into `E`
differ by an isometry of `E`: the map `L' ∘ L⁻¹`, defined on the range of `L`, extends to all of `E`
by `LinearIsometry.extend`, and in finite dimensions an isometry of `E` into itself is surjective,
hence a unitary.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalGroup.lean

complete

theorem ContinuousLinearMap.stiefelMeasure_eq.{u_1, u_2} {F : Type u_1}
  {E : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (L L' : F →ₗᵢ[ℝ] E) :
  ContinuousLinearMap.stiefelMeasure L =
    ContinuousLinearMap.stiefelMeasure L'

theorem ContinuousLinearMap.stiefelMeasure_eq.{u_1,
    u_2}
  {F : Type u_1} {E : Type u_2}
  [NormedAddCommGroup F]
  [InnerProductSpace ℝ F]
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (L L' : F →ₗᵢ[ℝ] E) :
  ContinuousLinearMap.stiefelMeasure L =
    ContinuousLinearMap.stiefelMeasure L'

**The Stiefel measure does not depend on the frame it is built from.** By transitivity the two
pushforwards differ by a right translation of the group, which the Haar measure does not see because
the group is unimodular.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalGroup.lean

complete

theorem ContinuousLinearMap.map_comp_right_stiefelMeasure.{u_1, u_2}
  {F : Type u_1} {E : Type u_2} [NormedAddCommGroup F]
  [InnerProductSpace ℝ F] [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (V : F ≃ₗᵢ[ℝ] F) (L : F →ₗᵢ[ℝ] E) :
  MeasureTheory.Measure.map (fun M ↦ M.comp V.toLinearIsometry)
      (ContinuousLinearMap.stiefelMeasure L) =
    ContinuousLinearMap.stiefelMeasure L

theorem ContinuousLinearMap.map_comp_right_stiefelMeasure.{u_1,
    u_2}
  {F : Type u_1} {E : Type u_2}
  [NormedAddCommGroup F]
  [InnerProductSpace ℝ F]
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (V : F ≃ₗᵢ[ℝ] F)
  (L : F →ₗᵢ[ℝ] E) :
  MeasureTheory.Measure.map
      (fun M ↦ M.comp V.toLinearIsometry)
      (ContinuousLinearMap.stiefelMeasure
        L) =
    ContinuousLinearMap.stiefelMeasure L

**The Stiefel measure is invariant under the right action of the isometries of the frame
space**, `L ↦ L ∘ V`. Precomposing by `V` only replaces the frame the measure is built from, and by
`stiefelMeasure_eq` every frame gives the same measure.

The Stiefel manifold of orthonormal k-frames is the space of linear isometries \mathbb R^k\to E, which Mathlib leaves without a topology, a Borel structure or a measure. All three are given here, the topology induced from the continuous linear maps, and the invariant measure is defined as the pushforward of the Haar probability measure along the action of the orthogonal group on a fixed frame. Defining it this way makes invariance hold by construction rather than by a uniqueness theorem — which is what a construction by iterated sphere measures would need, since the recursion there privileges the first vector of the frame and the dependent family of orthogonal complements admits no global measurable trivialization.

Two further properties are what the matrix polar integration formula in codimension greater than one needs, and both are here. Independence of the base frame: the action is transitive on frames, because the map L'\circ L^{-1} defined on the range of L extends to an isometry of all of E and in finite dimensions such an isometry is surjective, hence unitary; so the two pushforwards differ by a right translation of the group. That translation is invisible to the Haar measure because the group is unimodular — right translation of a left invariant measure is again left invariant, hence a scalar multiple of the Haar measure by uniqueness, and the scalar is the total mass, which compactness makes 1 on both sides. Mathlib derives right from left invariance only for abelian groups.

Invariance under the right action L\mapsto L\circ V of the isometries of \mathbb R^k then needs no separate argument: precomposing by V only replaces the frame the measure is built from, and by the previous paragraph every frame gives the same measure. This is the property that makes the direction integral of the matrix polar formula independent of the point of \mathbb S^{k-1} it is read at.

The sphere

Theorem5.7.2

Statement uses 2

Statement dependency previews

Preview

Theorem 5.3.2

Loading preview

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

Used by 3

Reverse dependency previews

Preview

Theorem 5.7.3

Loading preview

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

✓L∃∀N

The rotation-invariant measure on the unit sphere is unique. Mathlib records how Measure.toSphere is computed but none of its symmetries. Invariance under the orthogonal group is the first declaration group: Measure.toSphere_apply' computes \mu_{\mathbb S}(s) as \dim E times the Lebesgue measure of the open cone (0,1)\cdot s, a rotation carries that cone to the cone over the rotated set, and Lebesgue measure does not see a rotation. Uniqueness is the averaging argument: the orbit measure of a unit vector — the pushforward of the Haar probability measure along Q\mapsto Qv — does not depend on v, because the action is transitive and the Haar measure is unimodular; and averaging the invariance of the surface measure over the group, then exchanging the two integrals, identifies the surface measure with its total mass times that orbit measure. Transitivity on the sphere is the k=1 case of transitivity on frames, a unit vector being a linear isometry of the line.

Lean code for Theorem5.7.2●15 declarations

defdefined in LeanRidgelet/ToMathlib/LieGroup/SphereInvariantMeasure.lean

complete

def MeasureTheory.sphereAct.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (Q : ↥(unitary (E →L[ℝ] E))) (u : ↑(Metric.sphere 0 1)) :
  ↑(Metric.sphere 0 1)

def MeasureTheory.sphereAct.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (Q : ↥(unitary (E →L[ℝ] E)))
  (u : ↑(Metric.sphere 0 1)) :
  ↑(Metric.sphere 0 1)

Implementation after :=

:=
  ⟨(Q : E →L[ℝ] E) u, by
    rw [mem_sphere_zero_iff_norm, (Q : E →L[ℝ] E).norm_map_of_mem_unitary Q.property]
    exact mem_sphere_zero_iff_norm.1 u.2⟩

The action of the orthogonal group on the unit sphere.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SphereInvariantMeasure.lean

complete

theorem MeasureTheory.continuous_sphereAct.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] :
  Continuous fun p ↦ MeasureTheory.sphereAct p.1 p.2

theorem MeasureTheory.continuous_sphereAct.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] :
  Continuous fun p ↦
    MeasureTheory.sphereAct p.1 p.2

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SphereInvariantMeasure.lean

complete

theorem MeasureTheory.coe_image_preimage_sphereAct.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (Q : ↥(unitary (E →L[ℝ] E))) (s : Set ↑(Metric.sphere 0 1)) :
  Subtype.val '' MeasureTheory.sphereAct Q ⁻¹' s =
    (fun x ↦ ↑Q x) ⁻¹' Subtype.val '' s

theorem MeasureTheory.coe_image_preimage_sphereAct.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (Q : ↥(unitary (E →L[ℝ] E)))
  (s : Set ↑(Metric.sphere 0 1)) :
  Subtype.val ''
      MeasureTheory.sphereAct Q ⁻¹' s =
    (fun x ↦ ↑Q x) ⁻¹' Subtype.val '' s

Under the coercion to `E`, the preimage of a set of the sphere along a rotation is the preimage
along that rotation of the coerced set.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SphereInvariantMeasure.lean

complete

theorem MeasureTheory.smul_set_preimage_isometryEquiv.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e : E ≃ₗᵢ[ℝ] E)
  (S : Set ℝ) (A : Set E) : S • ⇑e ⁻¹' A = ⇑e ⁻¹' (S • A)

theorem MeasureTheory.smul_set_preimage_isometryEquiv.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (e : E ≃ₗᵢ[ℝ] E)
  (S : Set ℝ) (A : Set E) :
  S • ⇑e ⁻¹' A = ⇑e ⁻¹' (S • A)

A linear isometric equivalence commutes with the pointwise action of a set of scalars, on
preimages.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SphereInvariantMeasure.lean

complete

theorem MeasureTheory.map_sphereAct_toSphere.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] (Q : ↥(unitary (E →L[ℝ] E))) :
  MeasureTheory.Measure.map (MeasureTheory.sphereAct Q)
      MeasureTheory.volume.toSphere =
    MeasureTheory.volume.toSphere

theorem MeasureTheory.map_sphereAct_toSphere.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (Q : ↥(unitary (E →L[ℝ] E))) :
  MeasureTheory.Measure.map
      (MeasureTheory.sphereAct Q)
      MeasureTheory.volume.toSphere =
    MeasureTheory.volume.toSphere

**The surface measure of the unit sphere is invariant under the orthogonal group.** Mathlib
computes `μ.toSphere s` as `dim E` times the measure of the open cone `Ioo 0 1 • s`; a rotation
carries that cone to the cone over the rotated set, and Lebesgue measure does not see it.

defdefined in LeanRidgelet/ToMathlib/LieGroup/SphereInvariantMeasure.lean

complete

def MeasureTheory.unitVectorIsometry.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E}
  (hu : ‖u‖ = 1) : ℝ →ₗᵢ[ℝ] E

def MeasureTheory.unitVectorIsometry.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {u : E}
  (hu : ‖u‖ = 1) : ℝ →ₗᵢ[ℝ] E

Implementation after :=

:= t • u
  map_add' s t := by simp [add_smul]
  map_smul' c t := by simp [smul_smul]
  norm_map' t := by simp [norm_smul, hu]

A unit vector as a linear isometry of the line: the `k = 1` frame it is.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SphereInvariantMeasure.lean

complete

theorem MeasureTheory.exists_sphereAct_eq.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (u v : ↑(Metric.sphere 0 1)) : ∃ Q, MeasureTheory.sphereAct Q u = v

theorem MeasureTheory.exists_sphereAct_eq.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (u v : ↑(Metric.sphere 0 1)) :
  ∃ Q, MeasureTheory.sphereAct Q u = v

**The orthogonal group acts transitively on the unit sphere.** This is the `k = 1` case of
transitivity on frames: a unit vector is a linear isometry of the line.

defdefined in LeanRidgelet/ToMathlib/LieGroup/SphereInvariantMeasure.lean

complete

def MeasureTheory.sphereOrbitMeasure.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] (v : ↑(Metric.sphere 0 1)) :
  MeasureTheory.Measure ↑(Metric.sphere 0 1)

def MeasureTheory.sphereOrbitMeasure.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E]
  (v : ↑(Metric.sphere 0 1)) :
  MeasureTheory.Measure
    ↑(Metric.sphere 0 1)

Implementation after :=

:=
  Measure.map (fun Q => sphereAct Q v) ContinuousLinearMap.orthogonalHaar

The orbit measure of a unit vector: the pushforward of the Haar probability measure of the
orthogonal group along the orbit map `Q ↦ Q v`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SphereInvariantMeasure.lean

complete

theorem MeasureTheory.sphereOrbitMeasure_apply.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] (v : ↑(Metric.sphere 0 1))
  {s : Set ↑(Metric.sphere 0 1)} (hs : MeasurableSet s) :
  (MeasureTheory.sphereOrbitMeasure v) s =
    ∫⁻ (Q : ↥(unitary (E →L[ℝ] E))),
      s.indicator 1
        (MeasureTheory.sphereAct Q
          v) ∂ContinuousLinearMap.orthogonalHaar

theorem MeasureTheory.sphereOrbitMeasure_apply.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (v : ↑(Metric.sphere 0 1))
  {s : Set ↑(Metric.sphere 0 1)}
  (hs : MeasurableSet s) :
  (MeasureTheory.sphereOrbitMeasure v) s =
    ∫⁻ (Q : ↥(unitary (E →L[ℝ] E))),
      s.indicator 1
        (MeasureTheory.sphereAct Q
          v) ∂ContinuousLinearMap.orthogonalHaar

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SphereInvariantMeasure.lean

complete

theorem MeasureTheory.sphereOrbitMeasure_eq.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] (u v : ↑(Metric.sphere 0 1)) :
  MeasureTheory.sphereOrbitMeasure u =
    MeasureTheory.sphereOrbitMeasure v

theorem MeasureTheory.sphereOrbitMeasure_eq.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (u v : ↑(Metric.sphere 0 1)) :
  MeasureTheory.sphereOrbitMeasure u =
    MeasureTheory.sphereOrbitMeasure v

**The orbit measure does not depend on the vector it is taken at.** By transitivity the two
pushforwards differ by a right translation of the group, which the Haar measure does not see.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SphereInvariantMeasure.lean

complete

theorem MeasureTheory.toSphere_eq_smul_sphereOrbitMeasure.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] (v : ↑(Metric.sphere 0 1)) :
  MeasureTheory.volume.toSphere =
    MeasureTheory.volume.toSphere Set.univ •
      MeasureTheory.sphereOrbitMeasure v

theorem MeasureTheory.toSphere_eq_smul_sphereOrbitMeasure.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (v : ↑(Metric.sphere 0 1)) :
  MeasureTheory.volume.toSphere =
    MeasureTheory.volume.toSphere
        Set.univ •
      MeasureTheory.sphereOrbitMeasure v

**Uniqueness of the rotation-invariant measure on the unit sphere.** The surface measure is its
total mass times the orbit measure of any unit vector.

The proof is the standard averaging argument. Averaging the invariance of the surface measure over
the group and exchanging the two integrals turns the measure of a set into the integral over the
sphere of the orbit measure of that set, read at each point; that reading does not depend on the
point, so the integral is the total mass times a single value.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SphereInvariantMeasure.lean

complete

theorem MeasureTheory.sphereOrbitMeasure_eq_smul_toSphere.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] [Nontrivial E]
  (v : ↑(Metric.sphere 0 1)) :
  MeasureTheory.sphereOrbitMeasure v =
    (MeasureTheory.volume.toSphere Set.univ)⁻¹ •
      MeasureTheory.volume.toSphere

theorem MeasureTheory.sphereOrbitMeasure_eq_smul_toSphere.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [Nontrivial E]
  (v : ↑(Metric.sphere 0 1)) :
  MeasureTheory.sphereOrbitMeasure v =
    (MeasureTheory.volume.toSphere
          Set.univ)⁻¹ •
      MeasureTheory.volume.toSphere

Uniqueness, solved for the orbit measure: it is the normalized surface measure.

defdefined in LeanRidgelet/ToMathlib/LieGroup/SphereInvariantMeasure.lean

complete

def MeasureTheory.frameDirection.{u_1, u_2} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F' : Type u_2}
  [NormedAddCommGroup F'] [InnerProductSpace ℝ F'] (L : F' →ₗᵢ[ℝ] E)
  (ω : ↑(Metric.sphere 0 1)) : ↑(Metric.sphere 0 1)

def MeasureTheory.frameDirection.{u_1, u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {F' : Type u_2}
  [NormedAddCommGroup F']
  [InnerProductSpace ℝ F']
  (L : F' →ₗᵢ[ℝ] E)
  (ω : ↑(Metric.sphere 0 1)) :
  ↑(Metric.sphere 0 1)

Implementation after :=

:=
  ⟨L ω, by
    rw [mem_sphere_zero_iff_norm, L.norm_map]
    exact mem_sphere_zero_iff_norm.1 ω.2⟩

The direction a frame sends a unit vector of the frame space to, as a point of the unit sphere
of `E`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SphereInvariantMeasure.lean

complete

theorem MeasureTheory.continuous_frameDirection.{u_1, u_2} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F' : Type u_2}
  [NormedAddCommGroup F'] [InnerProductSpace ℝ F']
  (ω : ↑(Metric.sphere 0 1)) :
  Continuous fun L ↦ MeasureTheory.frameDirection L ω

theorem MeasureTheory.continuous_frameDirection.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {F' : Type u_2}
  [NormedAddCommGroup F']
  [InnerProductSpace ℝ F']
  (ω : ↑(Metric.sphere 0 1)) :
  Continuous fun L ↦
    MeasureTheory.frameDirection L ω

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SphereInvariantMeasure.lean

complete

theorem MeasureTheory.map_frameDirection_stiefelMeasure.{u_1, u_2}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  {F' : Type u_2} [NormedAddCommGroup F'] [InnerProductSpace ℝ F']
  [Nontrivial E] (L₀ : F' →ₗᵢ[ℝ] E) (ω : ↑(Metric.sphere 0 1))
  [FiniteDimensional ℝ F'] :
  MeasureTheory.Measure.map (fun L ↦ MeasureTheory.frameDirection L ω)
      (ContinuousLinearMap.stiefelMeasure L₀) =
    (MeasureTheory.volume.toSphere Set.univ)⁻¹ •
      MeasureTheory.volume.toSphere

theorem MeasureTheory.map_frameDirection_stiefelMeasure.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {F' : Type u_2} [NormedAddCommGroup F']
  [InnerProductSpace ℝ F'] [Nontrivial E]
  (L₀ : F' →ₗᵢ[ℝ] E)
  (ω : ↑(Metric.sphere 0 1))
  [FiniteDimensional ℝ F'] :
  MeasureTheory.Measure.map
      (fun L ↦
        MeasureTheory.frameDirection L ω)
      (ContinuousLinearMap.stiefelMeasure
        L₀) =
    (MeasureTheory.volume.toSphere
          Set.univ)⁻¹ •
      MeasureTheory.volume.toSphere

**The direction of a random frame is uniform on the sphere.** For a fixed unit vector of the
frame space, the pushforward of the invariant measure on the Stiefel manifold along `L ↦ L ω` is the
normalized surface measure — whichever unit vector is chosen, and whichever frame the Stiefel
measure was built from.

This is the identity the matrix polar integration formula turns on: it is what lets a direction
integral over frames be read as an integral over the sphere. Both halves of its proof are the point
of the two constructions: the pushforward along the orbit map of the *frame* composes with the
direction map to the orbit map of the *vector*, and the orbit measure of a vector is the normalized
surface measure by uniqueness.

The consequence the matrix polar integration formula needs is the last declaration: the direction of a random frame is uniform on the sphere. For a fixed unit vector \boldsymbol\omega of the frame space, the pushforward of the invariant measure on the Stiefel manifold along U\mapsto U\boldsymbol\omega is the normalized surface measure, whichever \boldsymbol\omega is chosen and whichever frame the Stiefel measure was built from. Both halves of the proof are what the two constructions were for: the orbit map of a frame composed with the direction map is the orbit map of a vector, and the orbit measure of a vector is the normalized surface measure by uniqueness.

The matrix polar integration formula

Theorem5.7.3

Statement uses 3

Statement dependency previews

Preview

Theorem 5.3.2

Loading preview

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

Used by 4

Reverse dependency previews

Preview

Lemma 3.1.19

Loading preview

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

✓L∃∀N

The matrix polar integration formula. Polar coordinates write an integral over \mathbb R^m as an integral over \mathbb S^{m-1}\times(0,\infty); the matrix polar formula does the same with a k-frame in place of a direction, c_{m,k}\int_{\mathbb R^m}F=\int_{V_{m,k}\times\mathbb R^k}F(U\boldsymbol b)\,|U\boldsymbol b|^{m-k}, and it is what the d-plane reconstruction formulas need in codimension greater than one. The proof is three reductions and no new analysis: polar coordinates on the frame space turn the weight |U\boldsymbol b|^{m-k} together with the Jacobian r^{k-1} into r^{m-1}, which is the Jacobian of polar coordinates on \mathbb R^m; the direction integral over frames becomes an integral over \mathbb S^{m-1} because the direction of a random frame is uniform there; and polar coordinates on \mathbb R^m put it back together.

Lean code for Theorem5.7.3●11 declarations

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/MatrixPolar.lean

complete

theorem MeasureTheory.toSphere_real_smul_integral_directionAverage.{u_1, u_2,
    u_3}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  [Nontrivial E] {F' : Type u_2} [NormedAddCommGroup F']
  [InnerProductSpace ℝ F'] [FiniteDimensional ℝ F'] [MeasurableSpace F']
  [BorelSpace F'] {G : Type u_3} [NormedAddCommGroup G]
  [NormedSpace ℝ G] [CompleteSpace G] (L₀ : F' →ₗᵢ[ℝ] E)
  {H : ↑(Metric.sphere 0 1) → G}
  (hH : MeasureTheory.Integrable H MeasureTheory.volume.toSphere)
  (hprod :
    MeasureTheory.Integrable
      (fun p ↦ H (MeasureTheory.frameDirection p.1 p.2))
      ((ContinuousLinearMap.stiefelMeasure L₀).prod
        MeasureTheory.volume.toSphere)) :
  MeasureTheory.volume.toSphere.real Set.univ •
      ∫ (L : F' →ₗᵢ[ℝ] E),
        ∫ (ω : ↑(Metric.sphere 0 1)),
          H
            (MeasureTheory.frameDirection L
              ω) ∂MeasureTheory.volume.toSphere ∂ContinuousLinearMap.stiefelMeasure
          L₀ =
    MeasureTheory.volume.toSphere.real Set.univ •
      ∫ (v : ↑(Metric.sphere 0 1)), H v ∂MeasureTheory.volume.toSphere

theorem MeasureTheory.toSphere_real_smul_integral_directionAverage.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [Nontrivial E] {F' : Type u_2}
  [NormedAddCommGroup F']
  [InnerProductSpace ℝ F']
  [FiniteDimensional ℝ F']
  [MeasurableSpace F'] [BorelSpace F']
  {G : Type u_3} [NormedAddCommGroup G]
  [NormedSpace ℝ G] [CompleteSpace G]
  (L₀ : F' →ₗᵢ[ℝ] E)
  {H : ↑(Metric.sphere 0 1) → G}
  (hH :
    MeasureTheory.Integrable H
      MeasureTheory.volume.toSphere)
  (hprod :
    MeasureTheory.Integrable
      (fun p ↦
        H
          (MeasureTheory.frameDirection
            p.1 p.2))
      ((ContinuousLinearMap.stiefelMeasure
            L₀).prod
        MeasureTheory.volume.toSphere)) :
  MeasureTheory.volume.toSphere.real
        Set.univ •
      ∫ (L : F' →ₗᵢ[ℝ] E),
        ∫ (ω : ↑(Metric.sphere 0 1)),
          H
            (MeasureTheory.frameDirection
              L
              ω) ∂MeasureTheory.volume.toSphere ∂ContinuousLinearMap.stiefelMeasure
          L₀ =
    MeasureTheory.volume.toSphere.real
        Set.univ •
      ∫ (v : ↑(Metric.sphere 0 1)),
        H v ∂MeasureTheory.volume.toSphere

**The average of a function of the direction, over frames and unit vectors.** For a function `H`
on the unit sphere of `E`, averaging `H` at the direction `U ω` over frames and over unit vectors
`ω` of the frame space is averaging `H` over the sphere of `E`, up to the ratio of the two sphere
areas.

This is the shared core of the reconstruction formulas over the Stiefel manifold and over the
similitude group: whatever the weight family, the derivation ends by reducing the parameter integral
to this average. It is `map_frameDirection_stiefelMeasure` — the direction of a random frame is
uniform on the sphere — with a Fubini exchange in front of it, and the statement is multiplied out
so that no division appears.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/MatrixPolar.lean

complete

theorem MeasureTheory.toSphere_real_smul_integral_stiefelMeasure.{u_1, u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  [Nontrivial E] {F' : Type u_2} [NormedAddCommGroup F']
  [InnerProductSpace ℝ F'] [FiniteDimensional ℝ F'] [MeasurableSpace F']
  [BorelSpace F'] [Nontrivial F'] {G : Type u_3} [NormedAddCommGroup G]
  [NormedSpace ℝ G] [CompleteSpace G] (L₀ : F' →ₗᵢ[ℝ] E) {F : E → G}
  (hF : MeasureTheory.Integrable F MeasureTheory.volume)
  (hsec :
    ∀ᵐ (L : F' →ₗᵢ[ℝ] E) ∂ContinuousLinearMap.stiefelMeasure L₀,
      MeasureTheory.Integrable
        (fun b ↦
          ‖L b‖ ^ (Module.finrank ℝ E - Module.finrank ℝ F') • F (L b))
        MeasureTheory.volume)
  (hprod :
    MeasureTheory.Integrable
      (fun p ↦
        ∫ (r : ℝ) in Set.Ioi 0,
          r ^ (Module.finrank ℝ E - 1) •
            F (r • ↑(MeasureTheory.frameDirection p.1 p.2)))
      ((ContinuousLinearMap.stiefelMeasure L₀).prod
        MeasureTheory.volume.toSphere)) :
  MeasureTheory.volume.toSphere.real Set.univ •
      ∫ (L : F' →ₗᵢ[ℝ] E),
        ∫ (b : F'),
          ‖L b‖ ^ (Module.finrank ℝ E - Module.finrank ℝ F') •
            F (L b) ∂ContinuousLinearMap.stiefelMeasure L₀ =
    MeasureTheory.volume.toSphere.real Set.univ • ∫ (x : E), F x

theorem MeasureTheory.toSphere_real_smul_integral_stiefelMeasure.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [Nontrivial E] {F' : Type u_2}
  [NormedAddCommGroup F']
  [InnerProductSpace ℝ F']
  [FiniteDimensional ℝ F']
  [MeasurableSpace F'] [BorelSpace F']
  [Nontrivial F'] {G : Type u_3}
  [NormedAddCommGroup G] [NormedSpace ℝ G]
  [CompleteSpace G] (L₀ : F' →ₗᵢ[ℝ] E)
  {F : E → G}
  (hF :
    MeasureTheory.Integrable F
      MeasureTheory.volume)
  (hsec :
    ∀ᵐ (L :
      F' →ₗᵢ[ℝ]
        E) ∂ContinuousLinearMap.stiefelMeasure
        L₀,
      MeasureTheory.Integrable
        (fun b ↦
          ‖L b‖ ^
              (Module.finrank ℝ E -
                Module.finrank ℝ F') •
            F (L b))
        MeasureTheory.volume)
  (hprod :
    MeasureTheory.Integrable
      (fun p ↦
        ∫ (r : ℝ) in Set.Ioi 0,
          r ^ (Module.finrank ℝ E - 1) •
            F
              (r •
                ↑(MeasureTheory.frameDirection
                    p.1 p.2)))
      ((ContinuousLinearMap.stiefelMeasure
            L₀).prod
        MeasureTheory.volume.toSphere)) :
  MeasureTheory.volume.toSphere.real
        Set.univ •
      ∫ (L : F' →ₗᵢ[ℝ] E),
        ∫ (b : F'),
          ‖L b‖ ^
              (Module.finrank ℝ E -
                Module.finrank ℝ F') •
            F
              (L
                b) ∂ContinuousLinearMap.stiefelMeasure
          L₀ =
    MeasureTheory.volume.toSphere.real
        Set.univ •
      ∫ (x : E), F x

**The matrix polar integration formula**, the article's Lemma C.2: an integral over `E` may be
read as an integral over frames and coordinate vectors, of the same function at `U b` against the
weight `|U b|^{m-k}`. The constant is the ratio of the areas of the two unit spheres, and the
statement is multiplied out so that no division appears.

The two integrability hypotheses are the absolute convergence the article assumes: the weighted
section along almost every frame, and the doubly iterated integrand on the product.

defdefined in LeanRidgelet/ToMathlib/LieGroup/MatrixPolar.lean

complete

def MeasureTheory.radialIntegral.{u_1, u_3} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {G : Type u_3}
  [NormedAddCommGroup G] [NormedSpace ℝ G] (F : E → G)
  (v : ↑(Metric.sphere 0 1)) : G

def MeasureTheory.radialIntegral.{u_1, u_3}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {G : Type u_3}
  [NormedAddCommGroup G] [NormedSpace ℝ G]
  (F : E → G) (v : ↑(Metric.sphere 0 1)) :
  G

Implementation after :=

:=
  ∫ r in Ioi (0 : ℝ), r ^ (Module.finrank ℝ E - 1) • F (r • (v : E))

The radial integral over a ray. This is the inner integral of polar coordinates on `E`, as a
function of the direction.

defdefined in LeanRidgelet/ToMathlib/LieGroup/MatrixPolar.lean

complete

def MeasureTheory.radialLIntegral.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (F : E → ENNReal)
  (v : ↑(Metric.sphere 0 1)) : ENNReal

def MeasureTheory.radialLIntegral.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (F : E → ENNReal)
  (v : ↑(Metric.sphere 0 1)) : ENNReal

Implementation after :=

:=
  ∫⁻ r in Ioi (0 : ℝ), ENNReal.ofReal (r ^ (Module.finrank ℝ E - 1)) * F (r • (v : E))

The radial integral over a ray, unsigned. This is the inner integral of polar coordinates on
`E`, as a function of the direction.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/MatrixPolar.lean

complete

theorem MeasureTheory.measurable_radialLIntegral.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E]
  [BorelSpace E] {F : E → ENNReal} (hF : Measurable F) :
  Measurable (MeasureTheory.radialLIntegral F)

theorem MeasureTheory.measurable_radialLIntegral.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {F : E → ENNReal} (hF : Measurable F) :
  Measurable
    (MeasureTheory.radialLIntegral F)

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/MatrixPolar.lean

complete

theorem MeasureTheory.toSphere_mul_lintegral_directionAverage.{u_1, u_2}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  [Nontrivial E] {F' : Type u_2} [NormedAddCommGroup F']
  [InnerProductSpace ℝ F'] [FiniteDimensional ℝ F'] [MeasurableSpace F']
  [BorelSpace F'] (L₀ : F' →ₗᵢ[ℝ] E)
  {H : ↑(Metric.sphere 0 1) → ENNReal} (hH : Measurable H) :
  MeasureTheory.volume.toSphere Set.univ *
      ∫⁻ (L : F' →ₗᵢ[ℝ] E),
        ∫⁻ (ω : ↑(Metric.sphere 0 1)),
          H
            (MeasureTheory.frameDirection L
              ω) ∂MeasureTheory.volume.toSphere ∂ContinuousLinearMap.stiefelMeasure
          L₀ =
    MeasureTheory.volume.toSphere Set.univ *
      ∫⁻ (v : ↑(Metric.sphere 0 1)), H v ∂MeasureTheory.volume.toSphere

theorem MeasureTheory.toSphere_mul_lintegral_directionAverage.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [Nontrivial E] {F' : Type u_2}
  [NormedAddCommGroup F']
  [InnerProductSpace ℝ F']
  [FiniteDimensional ℝ F']
  [MeasurableSpace F'] [BorelSpace F']
  (L₀ : F' →ₗᵢ[ℝ] E)
  {H : ↑(Metric.sphere 0 1) → ENNReal}
  (hH : Measurable H) :
  MeasureTheory.volume.toSphere Set.univ *
      ∫⁻ (L : F' →ₗᵢ[ℝ] E),
        ∫⁻ (ω : ↑(Metric.sphere 0 1)),
          H
            (MeasureTheory.frameDirection
              L
              ω) ∂MeasureTheory.volume.toSphere ∂ContinuousLinearMap.stiefelMeasure
          L₀ =
    MeasureTheory.volume.toSphere
        Set.univ *
      ∫⁻ (v : ↑(Metric.sphere 0 1)),
        H v ∂MeasureTheory.volume.toSphere

**The direction average, unsigned.** The counterpart of
`MeasureTheory.toSphere_real_smul_integral_directionAverage` for the lower Lebesgue integral: only
measurability is assumed, the exchange of the two integrals being Tonelli.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/MatrixPolar.lean

complete

theorem MeasureTheory.toSphere_mul_lintegral_stiefelMeasure.{u_1, u_2}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  [Nontrivial E] {F' : Type u_2} [NormedAddCommGroup F']
  [InnerProductSpace ℝ F'] [FiniteDimensional ℝ F'] [MeasurableSpace F']
  [BorelSpace F'] [Nontrivial F'] (L₀ : F' →ₗᵢ[ℝ] E) {F : E → ENNReal}
  (hF : Measurable F) :
  MeasureTheory.volume.toSphere Set.univ *
      ∫⁻ (L : F' →ₗᵢ[ℝ] E),
        ∫⁻ (b : F'),
          ENNReal.ofReal
              (‖L b‖ ^ (Module.finrank ℝ E - Module.finrank ℝ F')) *
            F (L b) ∂ContinuousLinearMap.stiefelMeasure L₀ =
    MeasureTheory.volume.toSphere Set.univ * ∫⁻ (x : E), F x

theorem MeasureTheory.toSphere_mul_lintegral_stiefelMeasure.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [Nontrivial E] {F' : Type u_2}
  [NormedAddCommGroup F']
  [InnerProductSpace ℝ F']
  [FiniteDimensional ℝ F']
  [MeasurableSpace F'] [BorelSpace F']
  [Nontrivial F'] (L₀ : F' →ₗᵢ[ℝ] E)
  {F : E → ENNReal} (hF : Measurable F) :
  MeasureTheory.volume.toSphere Set.univ *
      ∫⁻ (L : F' →ₗᵢ[ℝ] E),
        ∫⁻ (b : F'),
          ENNReal.ofReal
              (‖L b‖ ^
                (Module.finrank ℝ E -
                  Module.finrank ℝ F')) *
            F
              (L
                b) ∂ContinuousLinearMap.stiefelMeasure
          L₀ =
    MeasureTheory.volume.toSphere
        Set.univ *
      ∫⁻ (x : E), F x

**The matrix polar integration formula, unsigned.** The counterpart of
`MeasureTheory.toSphere_real_smul_integral_stiefelMeasure` for the lower Lebesgue integral: the only
hypothesis is measurability of the integrand, since both reductions are Tonelli.

The frame section needs no almost-everywhere qualifier here either: a frame is an isometry, so the
weight `|U b|^{m-k}` is `|b|^{m-k}` and the reduction holds at *every* frame.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/MatrixPolar.lean

complete

theorem MeasureTheory.continuous_frameApply.{u_1, u_2} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F' : Type u_2}
  [NormedAddCommGroup F'] [InnerProductSpace ℝ F'] :
  Continuous fun p ↦ p.1 p.2

theorem MeasureTheory.continuous_frameApply.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {F' : Type u_2}
  [NormedAddCommGroup F']
  [InnerProductSpace ℝ F'] :
  Continuous fun p ↦ p.1 p.2

Applying a frame to a vector is jointly continuous.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/MatrixPolar.lean

complete

theorem MeasureTheory.ae_integrable_weighted_frameSection.{u_1, u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  [Nontrivial E] {F' : Type u_2} [NormedAddCommGroup F']
  [InnerProductSpace ℝ F'] [FiniteDimensional ℝ F'] [MeasurableSpace F']
  [BorelSpace F'] [Nontrivial F'] {G : Type u_3} [NormedAddCommGroup G]
  [NormedSpace ℝ G] (L₀ : F' →ₗᵢ[ℝ] E) {F : E → G}
  (hFm : MeasureTheory.StronglyMeasurable F)
  (hF : MeasureTheory.Integrable F MeasureTheory.volume) :
  ∀ᵐ (L : F' →ₗᵢ[ℝ] E) ∂ContinuousLinearMap.stiefelMeasure L₀,
    MeasureTheory.Integrable
      (fun b ↦
        ‖L b‖ ^ (Module.finrank ℝ E - Module.finrank ℝ F') • F (L b))
      MeasureTheory.volume

theorem MeasureTheory.ae_integrable_weighted_frameSection.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [Nontrivial E] {F' : Type u_2}
  [NormedAddCommGroup F']
  [InnerProductSpace ℝ F']
  [FiniteDimensional ℝ F']
  [MeasurableSpace F'] [BorelSpace F']
  [Nontrivial F'] {G : Type u_3}
  [NormedAddCommGroup G] [NormedSpace ℝ G]
  (L₀ : F' →ₗᵢ[ℝ] E) {F : E → G}
  (hFm :
    MeasureTheory.StronglyMeasurable F)
  (hF :
    MeasureTheory.Integrable F
      MeasureTheory.volume) :
  ∀ᵐ (L :
    F' →ₗᵢ[ℝ]
      E) ∂ContinuousLinearMap.stiefelMeasure
      L₀,
    MeasureTheory.Integrable
      (fun b ↦
        ‖L b‖ ^
            (Module.finrank ℝ E -
              Module.finrank ℝ F') •
          F (L b))
      MeasureTheory.volume

**The weighted frame section of an integrable function is integrable at almost every frame.**
This is the first convergence hypothesis of the matrix polar formula, derived from its unsigned
form.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/MatrixPolar.lean

complete

theorem MeasureTheory.integrable_prod_radialIntegral.{u_1, u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  [Nontrivial E] {F' : Type u_2} [NormedAddCommGroup F']
  [InnerProductSpace ℝ F'] [FiniteDimensional ℝ F'] [MeasurableSpace F']
  [BorelSpace F'] {G : Type u_3} [NormedAddCommGroup G]
  [NormedSpace ℝ G] (L₀ : F' →ₗᵢ[ℝ] E) {F : E → G}
  (hFm : MeasureTheory.StronglyMeasurable F)
  (hF : MeasureTheory.Integrable F MeasureTheory.volume) :
  MeasureTheory.Integrable
    (fun p ↦
      MeasureTheory.radialIntegral F
        (MeasureTheory.frameDirection p.1 p.2))
    ((ContinuousLinearMap.stiefelMeasure L₀).prod
      MeasureTheory.volume.toSphere)

theorem MeasureTheory.integrable_prod_radialIntegral.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [Nontrivial E] {F' : Type u_2}
  [NormedAddCommGroup F']
  [InnerProductSpace ℝ F']
  [FiniteDimensional ℝ F']
  [MeasurableSpace F'] [BorelSpace F']
  {G : Type u_3} [NormedAddCommGroup G]
  [NormedSpace ℝ G] (L₀ : F' →ₗᵢ[ℝ] E)
  {F : E → G}
  (hFm :
    MeasureTheory.StronglyMeasurable F)
  (hF :
    MeasureTheory.Integrable F
      MeasureTheory.volume) :
  MeasureTheory.Integrable
    (fun p ↦
      MeasureTheory.radialIntegral F
        (MeasureTheory.frameDirection p.1
          p.2))
    ((ContinuousLinearMap.stiefelMeasure
          L₀).prod
      MeasureTheory.volume.toSphere)

**The doubly iterated integrand of the matrix polar formula is integrable on the product.** This
is the second convergence hypothesis, derived from the unsigned direction average.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/MatrixPolar.lean

complete

theorem MeasureTheory.toSphere_real_smul_integral_stiefelMeasure_of_stronglyMeasurable.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  [Nontrivial E] {F' : Type u_2} [NormedAddCommGroup F']
  [InnerProductSpace ℝ F'] [FiniteDimensional ℝ F'] [MeasurableSpace F']
  [BorelSpace F'] [Nontrivial F'] {G : Type u_3} [NormedAddCommGroup G]
  [NormedSpace ℝ G] [CompleteSpace G] (L₀ : F' →ₗᵢ[ℝ] E) {F : E → G}
  (hFm : MeasureTheory.StronglyMeasurable F)
  (hF : MeasureTheory.Integrable F MeasureTheory.volume) :
  MeasureTheory.volume.toSphere.real Set.univ •
      ∫ (L : F' →ₗᵢ[ℝ] E),
        ∫ (b : F'),
          ‖L b‖ ^ (Module.finrank ℝ E - Module.finrank ℝ F') •
            F (L b) ∂ContinuousLinearMap.stiefelMeasure L₀ =
    MeasureTheory.volume.toSphere.real Set.univ • ∫ (x : E), F x

theorem MeasureTheory.toSphere_real_smul_integral_stiefelMeasure_of_stronglyMeasurable.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [Nontrivial E] {F' : Type u_2}
  [NormedAddCommGroup F']
  [InnerProductSpace ℝ F']
  [FiniteDimensional ℝ F']
  [MeasurableSpace F'] [BorelSpace F']
  [Nontrivial F'] {G : Type u_3}
  [NormedAddCommGroup G] [NormedSpace ℝ G]
  [CompleteSpace G] (L₀ : F' →ₗᵢ[ℝ] E)
  {F : E → G}
  (hFm :
    MeasureTheory.StronglyMeasurable F)
  (hF :
    MeasureTheory.Integrable F
      MeasureTheory.volume) :
  MeasureTheory.volume.toSphere.real
        Set.univ •
      ∫ (L : F' →ₗᵢ[ℝ] E),
        ∫ (b : F'),
          ‖L b‖ ^
              (Module.finrank ℝ E -
                Module.finrank ℝ F') •
            F
              (L
                b) ∂ContinuousLinearMap.stiefelMeasure
          L₀ =
    MeasureTheory.volume.toSphere.real
        Set.univ •
      ∫ (x : E), F x

**The matrix polar integration formula for a strongly measurable integrand**, with no
convergence hypothesis beyond integrability. The measurability is what the left-hand side needs in
order to be determined at all: it reads the integrand only along the ranges of the frames, which are
null sets of `E` when `k < m`.

Since the invariant measure on the Stiefel manifold is normalized to a probability measure, the constant comes out as a ratio of sphere areas, |\mathbb S^{k-1}|/|\mathbb S^{m-1}|, and the statement is written multiplied out so that no division appears. That form is independent of how the Stiefel manifold is normalized. In the classical normalization, where the Stiefel manifold carries total mass \sigma_{m,k}=\prod_{j<k}|\mathbb S^{m-1-j}|, the constant becomes |\mathbb S^{k-1}|\cdot\sigma_{m-1,k-1} — the article's c_{m,k} with frames of the orthogonal complement of the direction rather than of the whole space. The two readings agree at k=1, which is why the codimension-one development did not see the difference.

The middle move is stated separately as the direction average, the first declaration: averaging a function of the direction U\boldsymbol\omega over frames and over unit vectors of the frame space is averaging it over \mathbb S^{m-1}, up to the ratio of the two sphere areas. That is the shared core of the reconstruction formulas over the Stiefel manifold and over the similitude group — whatever the weight family, the derivation ends by reducing the parameter integral to this average — so it is worth having on its own rather than inlined.

Both reductions are Tonelli rather than Fubini when read for the lower Lebesgue integral, so the unsigned form of the formula needs no hypothesis but measurability — and there the frame section needs no almost-everywhere qualifier either, a frame being an isometry, so the weight |U\boldsymbol b|^{m-k} is |\boldsymbol b|^{m-k} and the reduction holds at every frame.

That is what discharges the absolute convergence of the signed formula, which the article carries as a standing assumption: for a strongly measurable integrand, both hypotheses — the weighted section along almost every frame, and the doubly iterated integrand on the product — follow from integrability, by computing the integral of the norm with the unsigned formula and reading off that almost every fibre is finite.

The measurability cannot be weakened to almost-everywhere measurability, and the reason is not a technicality. The left-hand side reads the integrand only along the ranges of the frames, each of which is a null set of E when k<m; an integrable integrand may therefore be modified there — off a null set of E, so without disturbing the right-hand side — into one whose frame sections are not even measurable. What the unsigned formula does say is that a measurable null set is met in a null set by almost every frame, so the formula is insensitive to modifying a strongly measurable integrand on a null set even though no individual frame section is.

Codimension one

Theorem5.7.4

Statement uses 2

Statement dependency previews

Preview

Theorem 5.5.2

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Theorem 3.1.21

Loading preview

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

✓L∃∀N

The Stiefel manifold at codimension one is the unit sphere. The set-level identification is in mathlib_dplane_transform and the measure theory of the two sides is in mathlib_sphere_invariant_measure; this joins them. The identification is a homeomorphism: sending a frame to its unit vector is continuous because the topology on the Stiefel manifold is induced from the continuous linear maps, and sending a unit vector to the frame that scales it is continuous because that frame is the coordinate functional tensored with the vector, a bounded bilinear operation. Reading "the direction of a random frame is uniform on the sphere" through the identification then makes it measure preserving, onto the surface measure divided by its total mass — the only difference between the two sides being that the invariant measure on the Stiefel manifold is normalized to a probability measure and Measure.toSphere is not.

Lean code for Theorem5.7.4●5 declarations

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/StiefelCodimOne.lean

complete

theorem MeasureTheory.continuous_frameOfUnitVector.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] :
  Continuous MeasureTheory.frameOfUnitVector

theorem MeasureTheory.continuous_frameOfUnitVector.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] :
  Continuous
    MeasureTheory.frameOfUnitVector

Building a codimension-one frame out of a unit vector is continuous: as a continuous linear map
the frame is `MeasureTheory.EuclideanSpace.proj 0` tensored with the vector, and that is bilinear
and bounded.

defdefined in LeanRidgelet/ToMathlib/LieGroup/StiefelCodimOne.lean

complete

def MeasureTheory.stiefelHomeomorphSphere.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] :
  (EuclideanSpace ℝ (Fin 1) →ₗᵢ[ℝ] E) ≃ₜ ↑(Metric.sphere 0 1)

def MeasureTheory.stiefelHomeomorphSphere.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] :
  (EuclideanSpace ℝ (Fin 1) →ₗᵢ[ℝ] E) ≃ₜ
    ↑(Metric.sphere 0 1)

Implementation after :=

:= frameDirection L unitVectorFinOne
  invFun u := frameOfUnitVector u
  left_inv L := by
    ext b
    exact (apply_eq_smul_frameVectorCodimOne L b).symm
  right_inv u := by
    ext
    simp
  continuous_toFun := continuous_frameDirection _
  continuous_invFun := continuous_frameOfUnitVector

**The Stiefel manifold at codimension one is the unit sphere.** A frame is its unit vector and a
unit vector is the frame that scales it.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/StiefelCodimOne.lean

complete

theorem MeasureTheory.stiefelHomeomorphSphere_apply.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  (L : EuclideanSpace ℝ (Fin 1) →ₗᵢ[ℝ] E) :
  ↑(MeasureTheory.stiefelHomeomorphSphere L) =
    MeasureTheory.frameVectorCodimOne L

theorem MeasureTheory.stiefelHomeomorphSphere_apply.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (L :
    EuclideanSpace ℝ (Fin 1) →ₗᵢ[ℝ] E) :
  ↑(MeasureTheory.stiefelHomeomorphSphere
        L) =
    MeasureTheory.frameVectorCodimOne L

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/StiefelCodimOne.lean

complete

theorem MeasureTheory.measurePreserving_stiefelHomeomorphSphere.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  [Nontrivial E] (L₀ : EuclideanSpace ℝ (Fin 1) →ₗᵢ[ℝ] E) :
  MeasureTheory.MeasurePreserving
    (⇑MeasureTheory.stiefelHomeomorphSphere)
    (ContinuousLinearMap.stiefelMeasure L₀)
    ((MeasureTheory.volume.toSphere Set.univ)⁻¹ •
      MeasureTheory.volume.toSphere)

theorem MeasureTheory.measurePreserving_stiefelHomeomorphSphere.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [Nontrivial E]
  (L₀ :
    EuclideanSpace ℝ (Fin 1) →ₗᵢ[ℝ] E) :
  MeasureTheory.MeasurePreserving
    (⇑MeasureTheory.stiefelHomeomorphSphere)
    (ContinuousLinearMap.stiefelMeasure
      L₀)
    ((MeasureTheory.volume.toSphere
          Set.univ)⁻¹ •
      MeasureTheory.volume.toSphere)

**The invariant measure of `V_{m,1}` is the normalized surface measure of `𝕊^{m-1}`.** This is
`MeasureTheory.map_frameDirection_stiefelMeasure` read through the identification of the two spaces;
the inverse of the total mass is there because
`MeasureTheory.ContinuousLinearMap.stiefelMeasure` is a probability measure.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/StiefelCodimOne.lean

complete

theorem MeasureTheory.integral_stiefelMeasure_codimOne.{u_1, u_2} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] [Nontrivial E]
  (L₀ : EuclideanSpace ℝ (Fin 1) →ₗᵢ[ℝ] E) {G : Type u_2}
  [NormedAddCommGroup G] [NormedSpace ℝ G]
  (g : ↑(Metric.sphere 0 1) → G) :
  ∫ (L : EuclideanSpace ℝ (Fin 1) →ₗᵢ[ℝ] E),
      g
        (MeasureTheory.frameDirection L
          MeasureTheory.unitVectorFinOne) ∂ContinuousLinearMap.stiefelMeasure
        L₀ =
    (MeasureTheory.volume.toSphere.real Set.univ)⁻¹ •
      ∫ (u : ↑(Metric.sphere 0 1)), g u ∂MeasureTheory.volume.toSphere

theorem MeasureTheory.integral_stiefelMeasure_codimOne.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [Nontrivial E]
  (L₀ : EuclideanSpace ℝ (Fin 1) →ₗᵢ[ℝ] E)
  {G : Type u_2} [NormedAddCommGroup G]
  [NormedSpace ℝ G]
  (g : ↑(Metric.sphere 0 1) → G) :
  ∫ (L :
      EuclideanSpace ℝ (Fin 1) →ₗᵢ[ℝ] E),
      g
        (MeasureTheory.frameDirection L
          MeasureTheory.unitVectorFinOne) ∂ContinuousLinearMap.stiefelMeasure
        L₀ =
    (MeasureTheory.volume.toSphere.real
          Set.univ)⁻¹ •
      ∫ (u : ↑(Metric.sphere 0 1)),
        g u ∂MeasureTheory.volume.toSphere

**Integration over `V_{m,1}` is normalized integration over `𝕊^{m-1}`.** No measurability
hypothesis on the integrand is needed: the change of variables is along an equivalence.

The change of variables for integrals follows with no measurability hypothesis on the integrand, the substitution being along an equivalence. Its use is to make "the general codimension specializes to codimension one" a theorem about the two layers rather than a remark about two constructions that resemble each other.

Matrix decompositions

Theorem5.7.5

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 3.1.23

Loading preview

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

✓L∃∀N

Singular value decomposition of an injective linear map. Mathlib has singular values — LinearMap.singularValues, the square roots of the eigenvalues of A^\top A — but not the decomposition they are the values of. It is proved here in the case that integration over a matrix space needs: an injective A:\mathbb R^k\to E factors as A=UDV^\top with U an orthonormal k-frame, V a rotation of \mathbb R^k, and D the coordinatewise scaling by k positive numbers.

Lean code for Theorem5.7.5●6 declarations

defdefined in LeanRidgelet/ToMathlib/LieGroup/SingularValueDecomposition.lean

complete

def MeasureTheory.linearMapOfFamily.{u_1} {k : ℕ} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : Fin k → E) :
  EuclideanSpace ℝ (Fin k) →ₗ[ℝ] E

def MeasureTheory.linearMapOfFamily.{u_1}
  {k : ℕ} {E : Type u_1}
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (u : Fin k → E) :
  EuclideanSpace ℝ (Fin k) →ₗ[ℝ] E

Implementation after :=

:= ∑ i, ω i • u i
  map_add' ω η := by
    simp only [PiLp.add_apply, add_smul]
    exact Finset.sum_add_distrib
  map_smul' c ω := by
    simp only [PiLp.smul_apply, smul_eq_mul, mul_smul, RingHom.id_apply]
    exact Finset.smul_sum.symm

The linear map out of `ℝ^k` sending the standard basis to a given family.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SingularValueDecomposition.lean

complete

theorem MeasureTheory.linearMapOfFamily_apply.{u_1} {k : ℕ} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : Fin k → E)
  (ω : EuclideanSpace ℝ (Fin k)) :
  (MeasureTheory.linearMapOfFamily u) ω = ∑ i, ω.ofLp i • u i

theorem MeasureTheory.linearMapOfFamily_apply.{u_1}
  {k : ℕ} {E : Type u_1}
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (u : Fin k → E)
  (ω : EuclideanSpace ℝ (Fin k)) :
  (MeasureTheory.linearMapOfFamily u) ω =
    ∑ i, ω.ofLp i • u i

defdefined in LeanRidgelet/ToMathlib/LieGroup/SingularValueDecomposition.lean

complete

def MeasureTheory.isometryOfOrthonormalFamily.{u_1} {k : ℕ} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : Fin k → E}
  (hu : Orthonormal ℝ u) : EuclideanSpace ℝ (Fin k) →ₗᵢ[ℝ] E

def MeasureTheory.isometryOfOrthonormalFamily.{u_1}
  {k : ℕ} {E : Type u_1}
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {u : Fin k → E}
  (hu : Orthonormal ℝ u) :
  EuclideanSpace ℝ (Fin k) →ₗᵢ[ℝ] E

Implementation after :=

:= linearMapOfFamily u
  norm_map' ω := by
    rw [linearMapOfFamily_apply]
    have hinner : (inner ℝ (∑ i, ω i • u i) (∑ i, ω i • u i) : ℝ) = ∑ i, ω i * ω i := by
      rw [hu.inner_sum]
      exact Finset.sum_congr rfl fun i _ => by simp
    rw [norm_eq_sqrt_real_inner, hinner, EuclideanSpace.norm_eq]
    congr 1
    exact Finset.sum_congr rfl fun i _ => by rw [Real.norm_eq_abs, sq_abs, sq]

**An orthonormal family indexed by `Fin k` is a linear isometry out of `ℝ^k`**, sending the
standard basis to the family.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SingularValueDecomposition.lean

complete

theorem MeasureTheory.isometryOfOrthonormalFamily_apply.{u_1} {k : ℕ}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  {u : Fin k → E} (hu : Orthonormal ℝ u)
  (ω : EuclideanSpace ℝ (Fin k)) :
  (MeasureTheory.isometryOfOrthonormalFamily hu) ω = ∑ i, ω.ofLp i • u i

theorem MeasureTheory.isometryOfOrthonormalFamily_apply.{u_1}
  {k : ℕ} {E : Type u_1}
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {u : Fin k → E}
  (hu : Orthonormal ℝ u)
  (ω : EuclideanSpace ℝ (Fin k)) :
  (MeasureTheory.isometryOfOrthonormalFamily
        hu)
      ω =
    ∑ i, ω.ofLp i • u i

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SingularValueDecomposition.lean

complete

theorem MeasureTheory.isometryOfOrthonormalFamily_single.{u_1} {k : ℕ}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  {u : Fin k → E} (hu : Orthonormal ℝ u) (i : Fin k) :
  (MeasureTheory.isometryOfOrthonormalFamily hu)
      (EuclideanSpace.single i 1) =
    u i

theorem MeasureTheory.isometryOfOrthonormalFamily_single.{u_1}
  {k : ℕ} {E : Type u_1}
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {u : Fin k → E}
  (hu : Orthonormal ℝ u) (i : Fin k) :
  (MeasureTheory.isometryOfOrthonormalFamily
        hu)
      (EuclideanSpace.single i 1) =
    u i

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SingularValueDecomposition.lean

complete

theorem MeasureTheory.exists_svd.{u_1} {k : ℕ} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (A : EuclideanSpace ℝ (Fin k) →ₗ[ℝ] E) (hA : Function.Injective ⇑A) :
  ∃ U d V,
    (∀ (i : Fin k), 0 < d.ofLp i) ∧
      ∀ (ω : EuclideanSpace ℝ (Fin k)),
        A ω = U ((MeasureTheory.diagScale d.ofLp) (V.symm ω))

theorem MeasureTheory.exists_svd.{u_1} {k : ℕ}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (A : EuclideanSpace ℝ (Fin k) →ₗ[ℝ] E)
  (hA : Function.Injective ⇑A) :
  ∃ U d V,
    (∀ (i : Fin k), 0 < d.ofLp i) ∧
      ∀ (ω : EuclideanSpace ℝ (Fin k)),
        A ω =
          U
            ((MeasureTheory.diagScale
                d.ofLp)
              (V.symm ω))

**Singular value decomposition.** An injective linear map `A : ℝ^k → E` is an orthonormal
`k`-frame composed with a coordinatewise scaling by positive numbers composed with a rotation of
`ℝ^k`. Only the existence is proved here; the Jacobian of the decomposition is not.

The proof is the spectral theorem and nothing else. T=A^\top A is symmetric, and positive definite because A is injective; its orthonormal eigenbasis (b_i) has eigenvalues \mu_i=\|Ab_i\|^2>0; the vectors u_i=Ab_i/\sqrt{\mu_i} are orthonormal in E because \langle Ab_i,Ab_j\rangle=\langle Tb_i,b_j\rangle=\mu_i\delta_{ij}; and reading A in the two bases gives the factorization with d_i=\sqrt{\mu_i} and V the basis change. One auxiliary construction is worth naming on its own: an orthonormal family indexed by Fin k is a linear isometry out of \mathbb R^k, sending the standard basis to the family.

What is not here is the measure-theoretic half — the Jacobian \mathrm dA=\delta(D)\,\mathrm dD\,\mathrm dU\,\mathrm dV, which is what turns an integral over the matrix space into one over the singular value coordinates. Its published proofs go through exterior differential forms, or through the Jacobian of the matrix polar decomposition together with Weyl's integration formula for real symmetric matrices, and Mathlib has none of those.

Haar measure on the unit group of a finite-dimensional algebra

Theorem5.7.6

uses 0

Used by 2

Reverse dependency previews

Preview

Theorem 5.7.7

Loading preview

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

✓L∃∀N

Haar measure of a unit group as a weighted Lebesgue measure. The unit group of a finite-dimensional real normed algebra A is open in A, so its Haar measure should be an explicit weighted additive Haar measure of A. The weight is the reciprocal absolute algebra norm |N(a)|^{-1}, where N(a)=\det(x\mapsto ax) is Mathlib's Algebra.norm. Multiplicativity of the algebra norm — free, since Algebra.norm is a monoid homomorphism — makes the weighted measure invariant under left multiplication by units: substituting b=u^{-1}b' rescales additive Haar measure by |N(u)|^{-1} while the weight picks up the reciprocal factor |N(u^{-1})|^{-1}, and the two cancel because N(u^{-1})N(u)=1. No determinant power in \dim A has to be evaluated.

Lean code for Theorem5.7.6●26 declarations

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

theorem MeasureTheory.lmul_eq_mulLeft.{u_1} {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A] (a : A) :
  (Algebra.lmul ℝ A) a = LinearMap.mulLeft ℝ a

theorem MeasureTheory.lmul_eq_mulLeft.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A] (a : A) :
  (Algebra.lmul ℝ A) a =
    LinearMap.mulLeft ℝ a

Left multiplication as a linear map is the algebra multiplication map used by the algebra
norm.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

theorem MeasureTheory.continuous_algebraNorm.{u_1} {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A] : Continuous ⇑(Algebra.norm ℝ)

theorem MeasureTheory.continuous_algebraNorm.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A] :
  Continuous ⇑(Algebra.norm ℝ)

The algebra norm of a finite-dimensional real normed algebra is continuous: it is the
determinant of left multiplication, which depends continuously on the multiplier.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

theorem MeasureTheory.algebraNorm_units_ne_zero.{u_1} {A : Type u_1}
  [NormedRing A] [NormedAlgebra ℝ A] (u : Aˣ) : (Algebra.norm ℝ) ↑u ≠ 0

theorem MeasureTheory.algebraNorm_units_ne_zero.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A] (u : Aˣ) :
  (Algebra.norm ℝ) ↑u ≠ 0

The algebra norm of a unit is nonzero.

defdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

def MeasureTheory.unitsHaarDensity.{u_1} {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A] (a : A) : ENNReal

def MeasureTheory.unitsHaarDensity.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A] (a : A) : ENNReal

Implementation after :=

:= ENNReal.ofReal |Algebra.norm ℝ a|⁻¹

The density turning the additive Haar measure of a finite-dimensional real algebra into the
multiplicative Haar measure of its unit group: the reciprocal absolute algebra norm.

Multiplicativity of the algebra norm makes this density a multiplicative cocycle, which is the only
property used in the invariance proof; in particular no determinant power in the dimension of `A`
has to be evaluated.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

theorem MeasureTheory.unitsHaarDensity_apply.{u_1} {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A] (a : A) :
  MeasureTheory.unitsHaarDensity a =
    ENNReal.ofReal |(Algebra.norm ℝ) a|⁻¹

theorem MeasureTheory.unitsHaarDensity_apply.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A] (a : A) :
  MeasureTheory.unitsHaarDensity a =
    ENNReal.ofReal |(Algebra.norm ℝ) a|⁻¹

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

theorem MeasureTheory.continuous_unitsHaarDensity_comp_units_val.{u_1}
  {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] :
  Continuous fun u ↦ |(Algebra.norm ℝ) ↑u|⁻¹

theorem MeasureTheory.continuous_unitsHaarDensity_comp_units_val.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A] :
  Continuous fun u ↦
    |(Algebra.norm ℝ) ↑u|⁻¹

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

theorem MeasureTheory.measurable_unitsHaarDensity.{u_1} {A : Type u_1}
  [NormedRing A] [NormedAlgebra ℝ A] [MeasurableSpace A]
  [BorelSpace A] : Measurable MeasureTheory.unitsHaarDensity

theorem MeasureTheory.measurable_unitsHaarDensity.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A] [MeasurableSpace A]
  [BorelSpace A] :
  Measurable
    MeasureTheory.unitsHaarDensity

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

theorem MeasureTheory.unitsHaarDensity_mul.{u_1} {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A] (a b : A) :
  MeasureTheory.unitsHaarDensity (a * b) =
    MeasureTheory.unitsHaarDensity a * MeasureTheory.unitsHaarDensity b

theorem MeasureTheory.unitsHaarDensity_mul.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A] (a b : A) :
  MeasureTheory.unitsHaarDensity (a * b) =
    MeasureTheory.unitsHaarDensity a *
      MeasureTheory.unitsHaarDensity b

The density is multiplicative, because the algebra norm is.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

theorem MeasureTheory.unitsHaarDensity_one.{u_1} {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A] : MeasureTheory.unitsHaarDensity 1 = 1

theorem MeasureTheory.unitsHaarDensity_one.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A] :
  MeasureTheory.unitsHaarDensity 1 = 1

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

theorem MeasureTheory.unitsHaarDensity_units_ne_zero.{u_1} {A : Type u_1}
  [NormedRing A] [NormedAlgebra ℝ A] (u : Aˣ) :
  MeasureTheory.unitsHaarDensity ↑u ≠ 0

theorem MeasureTheory.unitsHaarDensity_units_ne_zero.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A] (u : Aˣ) :
  MeasureTheory.unitsHaarDensity ↑u ≠ 0

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

theorem MeasureTheory.unitsHaarDensity_units_ne_top.{u_1} {A : Type u_1}
  [NormedRing A] [NormedAlgebra ℝ A] (u : Aˣ) :
  MeasureTheory.unitsHaarDensity ↑u ≠ ⊤

theorem MeasureTheory.unitsHaarDensity_units_ne_top.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A] (u : Aˣ) :
  MeasureTheory.unitsHaarDensity ↑u ≠ ⊤

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

theorem MeasureTheory.unitsHaarDensity_units_inv_mul_units.{u_1} {A : Type u_1}
  [NormedRing A] [NormedAlgebra ℝ A] (u : Aˣ) :
  MeasureTheory.unitsHaarDensity ↑u⁻¹ *
      MeasureTheory.unitsHaarDensity ↑u =
    1

theorem MeasureTheory.unitsHaarDensity_units_inv_mul_units.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A] (u : Aˣ) :
  MeasureTheory.unitsHaarDensity ↑u⁻¹ *
      MeasureTheory.unitsHaarDensity ↑u =
    1

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

theorem MeasureTheory.exists_unitsHaarDensity_le_of_isCompact.{u_1}
  {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] {S : Set Aˣ}
  (hS : IsCompact S) :
  ∃ C,
    C ≠ ⊤ ∧ ∀ a ∈ Units.val '' S, MeasureTheory.unitsHaarDensity a ≤ C

theorem MeasureTheory.exists_unitsHaarDensity_le_of_isCompact.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A] {S : Set Aˣ}
  (hS : IsCompact S) :
  ∃ C,
    C ≠ ⊤ ∧
      ∀ a ∈ Units.val '' S,
        MeasureTheory.unitsHaarDensity a ≤
          C

On a compact subset of the unit group the density is bounded.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

theorem MeasureTheory.map_mul_left_withDensity_unitsHaarDensity.{u_1}
  {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A]
  [FiniteDimensional ℝ A] [MeasurableSpace A] [BorelSpace A]
  (μ : MeasureTheory.Measure A) [μ.IsAddHaarMeasure] (u : Aˣ) :
  MeasureTheory.Measure.map (fun b ↦ ↑u * b)
      (μ.withDensity MeasureTheory.unitsHaarDensity) =
    μ.withDensity MeasureTheory.unitsHaarDensity

theorem MeasureTheory.map_mul_left_withDensity_unitsHaarDensity.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A]
  [FiniteDimensional ℝ A]
  [MeasurableSpace A] [BorelSpace A]
  (μ : MeasureTheory.Measure A)
  [μ.IsAddHaarMeasure] (u : Aˣ) :
  MeasureTheory.Measure.map
      (fun b ↦ ↑u * b)
      (μ.withDensity
        MeasureTheory.unitsHaarDensity) =
    μ.withDensity
      MeasureTheory.unitsHaarDensity

The additive Haar measure of a finite-dimensional real algebra, weighted by the reciprocal
absolute algebra norm, is invariant under left multiplication by a unit: the determinant factor
produced by the change of variables cancels against the multiplicative weight.

defdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

def MeasureTheory.Measure.unitsHaar.{u_1} {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A] [MeasurableSpace A] (μ : MeasureTheory.Measure A)
  [MeasurableSpace Aˣ] : MeasureTheory.Measure Aˣ

def MeasureTheory.Measure.unitsHaar.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A] [MeasurableSpace A]
  (μ : MeasureTheory.Measure A)
  [MeasurableSpace Aˣ] :
  MeasureTheory.Measure Aˣ

Implementation after :=

:=
  Measure.comap Units.val (μ.withDensity unitsHaarDensity)

Haar measure of the unit group of a finite-dimensional real normed algebra, realized as the
reciprocal-algebra-norm-weighted additive Haar measure of the algebra, restricted to the open set of
units.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

theorem MeasureTheory.Measure.unitsHaar_apply.{u_1} {A : Type u_1}
  [NormedRing A] [NormedAlgebra ℝ A] [FiniteDimensional ℝ A]
  [MeasurableSpace A] [BorelSpace A] (μ : MeasureTheory.Measure A)
  [MeasurableSpace Aˣ] [BorelSpace Aˣ] (s : Set Aˣ) :
  μ.unitsHaar s =
    (μ.withDensity MeasureTheory.unitsHaarDensity) (Units.val '' s)

theorem MeasureTheory.Measure.unitsHaar_apply.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A]
  [FiniteDimensional ℝ A]
  [MeasurableSpace A] [BorelSpace A]
  (μ : MeasureTheory.Measure A)
  [MeasurableSpace Aˣ] [BorelSpace Aˣ]
  (s : Set Aˣ) :
  μ.unitsHaar s =
    (μ.withDensity
        MeasureTheory.unitsHaarDensity)
      (Units.val '' s)

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

theorem MeasureTheory.Measure.unitsHaar_apply_of_measurableSet.{u_1}
  {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A]
  [FiniteDimensional ℝ A] [MeasurableSpace A] [BorelSpace A]
  (μ : MeasureTheory.Measure A) [MeasurableSpace Aˣ] [BorelSpace Aˣ]
  {s : Set Aˣ} (hs : MeasurableSet s) :
  μ.unitsHaar s =
    ∫⁻ (a : A) in Units.val '' s, MeasureTheory.unitsHaarDensity a ∂μ

theorem MeasureTheory.Measure.unitsHaar_apply_of_measurableSet.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A]
  [FiniteDimensional ℝ A]
  [MeasurableSpace A] [BorelSpace A]
  (μ : MeasureTheory.Measure A)
  [MeasurableSpace Aˣ] [BorelSpace Aˣ]
  {s : Set Aˣ} (hs : MeasurableSet s) :
  μ.unitsHaar s =
    ∫⁻ (a : A) in Units.val '' s,
      MeasureTheory.unitsHaarDensity a ∂μ

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

theorem MeasureTheory.units_val_image_preimage_mul_left.{u_1} {A : Type u_1}
  [NormedRing A] (u : Aˣ) (s : Set Aˣ) :
  Units.val '' (fun x ↦ u * x) ⁻¹' s =
    (fun b ↦ ↑u * b) ⁻¹' Units.val '' s

theorem MeasureTheory.units_val_image_preimage_mul_left.{u_1}
  {A : Type u_1} [NormedRing A] (u : Aˣ)
  (s : Set Aˣ) :
  Units.val '' (fun x ↦ u * x) ⁻¹' s =
    (fun b ↦ ↑u * b) ⁻¹' Units.val '' s

Left translation by a unit matches, through `Units.val`, left multiplication in the algebra.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

theorem MeasureTheory.Measure.isMulLeftInvariant_unitsHaar.{u_1} {A : Type u_1}
  [NormedRing A] [NormedAlgebra ℝ A] [FiniteDimensional ℝ A]
  [MeasurableSpace A] [BorelSpace A] (μ : MeasureTheory.Measure A)
  [MeasurableSpace Aˣ] [BorelSpace Aˣ] [μ.IsAddHaarMeasure] :
  μ.unitsHaar.IsMulLeftInvariant

theorem MeasureTheory.Measure.isMulLeftInvariant_unitsHaar.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A]
  [FiniteDimensional ℝ A]
  [MeasurableSpace A] [BorelSpace A]
  (μ : MeasureTheory.Measure A)
  [MeasurableSpace Aˣ] [BorelSpace Aˣ]
  [μ.IsAddHaarMeasure] :
  μ.unitsHaar.IsMulLeftInvariant

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

theorem MeasureTheory.Measure.isFiniteMeasureOnCompacts_unitsHaar.{u_1}
  {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A]
  [FiniteDimensional ℝ A] [MeasurableSpace A] [BorelSpace A]
  (μ : MeasureTheory.Measure A) [MeasurableSpace Aˣ] [BorelSpace Aˣ]
  [μ.IsAddHaarMeasure] :
  MeasureTheory.IsFiniteMeasureOnCompacts μ.unitsHaar

theorem MeasureTheory.Measure.isFiniteMeasureOnCompacts_unitsHaar.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A]
  [FiniteDimensional ℝ A]
  [MeasurableSpace A] [BorelSpace A]
  (μ : MeasureTheory.Measure A)
  [MeasurableSpace Aˣ] [BorelSpace Aˣ]
  [μ.IsAddHaarMeasure] :
  MeasureTheory.IsFiniteMeasureOnCompacts
    μ.unitsHaar

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

theorem MeasureTheory.Measure.isOpenPosMeasure_unitsHaar.{u_1} {A : Type u_1}
  [NormedRing A] [NormedAlgebra ℝ A] [FiniteDimensional ℝ A]
  [MeasurableSpace A] [BorelSpace A] (μ : MeasureTheory.Measure A)
  [MeasurableSpace Aˣ] [BorelSpace Aˣ] [μ.IsAddHaarMeasure] :
  μ.unitsHaar.IsOpenPosMeasure

theorem MeasureTheory.Measure.isOpenPosMeasure_unitsHaar.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A]
  [FiniteDimensional ℝ A]
  [MeasurableSpace A] [BorelSpace A]
  (μ : MeasureTheory.Measure A)
  [MeasurableSpace Aˣ] [BorelSpace Aˣ]
  [μ.IsAddHaarMeasure] :
  μ.unitsHaar.IsOpenPosMeasure

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

theorem MeasureTheory.Measure.isHaarMeasure_unitsHaar.{u_1} {A : Type u_1}
  [NormedRing A] [NormedAlgebra ℝ A] [FiniteDimensional ℝ A]
  [MeasurableSpace A] [BorelSpace A] (μ : MeasureTheory.Measure A)
  [MeasurableSpace Aˣ] [BorelSpace Aˣ] [μ.IsAddHaarMeasure] :
  μ.unitsHaar.IsHaarMeasure

theorem MeasureTheory.Measure.isHaarMeasure_unitsHaar.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A]
  [FiniteDimensional ℝ A]
  [MeasurableSpace A] [BorelSpace A]
  (μ : MeasureTheory.Measure A)
  [MeasurableSpace Aˣ] [BorelSpace Aˣ]
  [μ.IsAddHaarMeasure] :
  μ.unitsHaar.IsHaarMeasure

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

theorem MeasureTheory.instLocallyCompactSpaceUnits.{u_1} {A : Type u_1}
  [NormedRing A] [NormedAlgebra ℝ A] [FiniteDimensional ℝ A] :
  LocallyCompactSpace Aˣ

theorem MeasureTheory.instLocallyCompactSpaceUnits.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A]
  [FiniteDimensional ℝ A] :
  LocallyCompactSpace Aˣ

The unit group of a finite-dimensional real normed algebra is locally compact, being an open
subset of the algebra.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

theorem MeasureTheory.instSecondCountableTopologyUnits.{u_1} {A : Type u_1}
  [NormedRing A] [NormedAlgebra ℝ A] [FiniteDimensional ℝ A] :
  SecondCountableTopology Aˣ

theorem MeasureTheory.instSecondCountableTopologyUnits.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A]
  [FiniteDimensional ℝ A] :
  SecondCountableTopology Aˣ

The unit group of a finite-dimensional real normed algebra is second countable, being embedded
in the algebra.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

theorem MeasureTheory.Measure.exists_haar_eq_smul_unitsHaar.{u_1} {A : Type u_1}
  [NormedRing A] [NormedAlgebra ℝ A] [FiniteDimensional ℝ A]
  [MeasurableSpace A] [BorelSpace A] (μ : MeasureTheory.Measure A)
  [MeasurableSpace Aˣ] [BorelSpace Aˣ] [μ.IsAddHaarMeasure] :
  ∃ c,
    c ≠ 0 ∧
      c ≠ ⊤ ∧
        ∀ (s : Set Aˣ), MeasureTheory.Measure.haar s = c * μ.unitsHaar s

theorem MeasureTheory.Measure.exists_haar_eq_smul_unitsHaar.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A]
  [FiniteDimensional ℝ A]
  [MeasurableSpace A] [BorelSpace A]
  (μ : MeasureTheory.Measure A)
  [MeasurableSpace Aˣ] [BorelSpace Aˣ]
  [μ.IsAddHaarMeasure] :
  ∃ c,
    c ≠ 0 ∧
      c ≠ ⊤ ∧
        ∀ (s : Set Aˣ),
          MeasureTheory.Measure.haar s =
            c * μ.unitsHaar s

Uniqueness of Haar measure identifies the canonical Haar measure of the unit group with the
explicit weighted additive Haar measure, up to a positive finite factor.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitsHaar.lean

complete

theorem MeasureTheory.Measure.exists_map_units_val_haar_restrict_le.{u_1}
  {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A]
  [FiniteDimensional ℝ A] [MeasurableSpace A] [BorelSpace A]
  (μ : MeasureTheory.Measure A) [MeasurableSpace Aˣ] [BorelSpace Aˣ]
  [μ.IsAddHaarMeasure] {S : Set Aˣ} (hS : IsCompact S) :
  ∃ C,
    C ≠ ⊤ ∧
      MeasureTheory.Measure.map Units.val
          (MeasureTheory.Measure.haar.restrict S) ≤
        C • μ.restrict (Units.val '' S)

theorem MeasureTheory.Measure.exists_map_units_val_haar_restrict_le.{u_1}
  {A : Type u_1} [NormedRing A]
  [NormedAlgebra ℝ A]
  [FiniteDimensional ℝ A]
  [MeasurableSpace A] [BorelSpace A]
  (μ : MeasureTheory.Measure A)
  [MeasurableSpace Aˣ] [BorelSpace Aˣ]
  [μ.IsAddHaarMeasure] {S : Set Aˣ}
  (hS : IsCompact S) :
  ∃ C,
    C ≠ ⊤ ∧
      MeasureTheory.Measure.map Units.val
          (MeasureTheory.Measure.haar.restrict
            S) ≤
        C • μ.restrict (Units.val '' S)

On a compact subset of the unit group, the image of Haar measure under `Units.val` is dominated
by additive Haar measure of the algebra, restricted to the compact image.  This is the comparison
used to deduce local integrability on the unit group from integrability on the algebra; keeping the
restriction is what makes the bound usable for functions that are only locally integrable.

The weighted measure is finite on compact subsets of the unit group, because the weight is continuous there — the algebra norm is continuous, being the determinant of the continuous linear map x\mapsto ax, and it does not vanish on units — and it is positive on nonempty open sets, because the weight is positive on units. Transporting it to the unit group along the open embedding gives a Haar measure, so uniqueness of Haar measure identifies the canonical Haar measure of the unit group with it up to a positive finite factor.

The consequence used downstream is a comparison: on a compact subset of the unit group, the image of Haar measure under the inclusion into A is dominated by a multiple of additive Haar measure of A. It converts local integrability statements on the algebra into local integrability statements on the group, which is what the quotient-integral estimate of an induced representation needs.

Haar measure of a semidirect product

Theorem5.7.7

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 4.3.7

Loading preview

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

✓L∃∀N

Left Haar measure of N ⋊ G as a product measure. Haar measure of a semidirect product is Haar measure of the normal factor times a relatively invariant measure on the acting factor, the correction being exactly the factor χ(g) by which the action of g rescales Haar measure of N. The proof is short because left translation by a fixed x_0 acts on the two product coordinates separately — the acting coordinate of x_0 is fixed, so its action on N does not depend on the point being translated — hence Measure.map_prod_map applies, and the two coordinate factors χ(x_0.\mathrm{right}) and χ(x_0.\mathrm{right}^{-1}) cancel by multiplicativity alone. No positivity or finiteness of the character is used.

Lean code for Theorem5.7.7●12 declarations

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SemidirectProductHaar.lean

complete

theorem MeasureTheory.map_mul_left_withDensity_monoidHom.{u_1} {G : Type u_1}
  [Group G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G]
  [ContinuousMul G] (κ : MeasureTheory.Measure G) [κ.IsMulLeftInvariant]
  (χ : G →* ENNReal) (hχ : Measurable ⇑χ) (g₀ : G) :
  MeasureTheory.Measure.map (fun g ↦ g₀ * g) (κ.withDensity ⇑χ) =
    χ g₀⁻¹ • κ.withDensity ⇑χ

theorem MeasureTheory.map_mul_left_withDensity_monoidHom.{u_1}
  {G : Type u_1} [Group G]
  [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [ContinuousMul G]
  (κ : MeasureTheory.Measure G)
  [κ.IsMulLeftInvariant]
  (χ : G →* ENNReal) (hχ : Measurable ⇑χ)
  (g₀ : G) :
  MeasureTheory.Measure.map
      (fun g ↦ g₀ * g)
      (κ.withDensity ⇑χ) =
    χ g₀⁻¹ • κ.withDensity ⇑χ

Twisting a left-invariant measure by a multiplicative character rescales left translation by the
character of the translating element.  No positivity or finiteness of the character is needed: the
scaling factor is written as the value at the inverse.

defdefined in LeanRidgelet/ToMathlib/LieGroup/SemidirectProductHaar.lean

complete

def SemidirectProduct.prodMeasure.{u_1, u_2} {N : Type u_1} {G : Type u_2}
  [Group N] [Group G] [TopologicalSpace N] [TopologicalSpace G]
  [MeasurableSpace N] [MeasurableSpace G] (φ : G →* MulAut N)
  (ν : MeasureTheory.Measure N) (lam : MeasureTheory.Measure G) :
  MeasureTheory.Measure (N ⋊[φ] G)

def SemidirectProduct.prodMeasure.{u_1, u_2}
  {N : Type u_1} {G : Type u_2} [Group N]
  [Group G] [TopologicalSpace N]
  [TopologicalSpace G] [MeasurableSpace N]
  [MeasurableSpace G] (φ : G →* MulAut N)
  (ν : MeasureTheory.Measure N)
  (lam : MeasureTheory.Measure G) :
  MeasureTheory.Measure (N ⋊[φ] G)

Implementation after :=

:=
  Measure.map (homeomorphProd φ).symm (ν.prod lam)

The product measure of a measure on `N` and a measure on `G`, transported to the semidirect
product through the canonical product homeomorphism.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SemidirectProductHaar.lean

complete

theorem SemidirectProduct.measurable_homeomorphProd_symm.{u_1, u_2}
  {N : Type u_1} {G : Type u_2} [Group N] [Group G] [TopologicalSpace N]
  [TopologicalSpace G] [MeasurableSpace N] [BorelSpace N]
  [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G]
  (φ : G →* MulAut N) :
  Measurable ⇑(SemidirectProduct.homeomorphProd φ).symm

theorem SemidirectProduct.measurable_homeomorphProd_symm.{u_1,
    u_2}
  {N : Type u_1} {G : Type u_2} [Group N]
  [Group G] [TopologicalSpace N]
  [TopologicalSpace G] [MeasurableSpace N]
  [BorelSpace N] [MeasurableSpace G]
  [BorelSpace G]
  [SecondCountableTopology G]
  (φ : G →* MulAut N) :
  Measurable
    ⇑(SemidirectProduct.homeomorphProd
          φ).symm

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SemidirectProductHaar.lean

complete

theorem SemidirectProduct.measurable_homeomorphProd.{u_1, u_2} {N : Type u_1}
  {G : Type u_2} [Group N] [Group G] [TopologicalSpace N]
  [TopologicalSpace G] [MeasurableSpace N] [BorelSpace N]
  [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G]
  (φ : G →* MulAut N) : Measurable ⇑(SemidirectProduct.homeomorphProd φ)

theorem SemidirectProduct.measurable_homeomorphProd.{u_1,
    u_2}
  {N : Type u_1} {G : Type u_2} [Group N]
  [Group G] [TopologicalSpace N]
  [TopologicalSpace G] [MeasurableSpace N]
  [BorelSpace N] [MeasurableSpace G]
  [BorelSpace G]
  [SecondCountableTopology G]
  (φ : G →* MulAut N) :
  Measurable
    ⇑(SemidirectProduct.homeomorphProd φ)

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SemidirectProductHaar.lean

complete

theorem SemidirectProduct.prodMeasure_apply.{u_1, u_2} {N : Type u_1}
  {G : Type u_2} [Group N] [Group G] [TopologicalSpace N]
  [TopologicalSpace G] [MeasurableSpace N] [BorelSpace N]
  [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G]
  (φ : G →* MulAut N) (ν : MeasureTheory.Measure N)
  (lam : MeasureTheory.Measure G) [MeasureTheory.SFinite lam]
  {s : Set (N ⋊[φ] G)} (hs : MeasurableSet s) :
  (SemidirectProduct.prodMeasure φ ν lam) s =
    (ν.prod lam) (⇑(SemidirectProduct.homeomorphProd φ).symm ⁻¹' s)

theorem SemidirectProduct.prodMeasure_apply.{u_1,
    u_2}
  {N : Type u_1} {G : Type u_2} [Group N]
  [Group G] [TopologicalSpace N]
  [TopologicalSpace G] [MeasurableSpace N]
  [BorelSpace N] [MeasurableSpace G]
  [BorelSpace G]
  [SecondCountableTopology G]
  (φ : G →* MulAut N)
  (ν : MeasureTheory.Measure N)
  (lam : MeasureTheory.Measure G)
  [MeasureTheory.SFinite lam]
  {s : Set (N ⋊[φ] G)}
  (hs : MeasurableSet s) :
  (SemidirectProduct.prodMeasure φ ν lam)
      s =
    (ν.prod lam)
      (⇑(SemidirectProduct.homeomorphProd
              φ).symm ⁻¹'
        s)

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SemidirectProductHaar.lean

complete

theorem SemidirectProduct.homeomorphProd_symm_comp_mul_left.{u_1, u_2}
  {N : Type u_1} {G : Type u_2} [Group N] [Group G] [TopologicalSpace N]
  [TopologicalSpace G] (φ : G →* MulAut N) (x₀ : N ⋊[φ] G) :
  (fun x ↦ x₀ * x) ∘ ⇑(SemidirectProduct.homeomorphProd φ).symm =
    ⇑(SemidirectProduct.homeomorphProd φ).symm ∘
      Prod.map (fun n ↦ x₀.left * (φ x₀.right) n) fun g ↦ x₀.right * g

theorem SemidirectProduct.homeomorphProd_symm_comp_mul_left.{u_1,
    u_2}
  {N : Type u_1} {G : Type u_2} [Group N]
  [Group G] [TopologicalSpace N]
  [TopologicalSpace G] (φ : G →* MulAut N)
  (x₀ : N ⋊[φ] G) :
  (fun x ↦ x₀ * x) ∘
      ⇑(SemidirectProduct.homeomorphProd
            φ).symm =
    ⇑(SemidirectProduct.homeomorphProd
            φ).symm ∘
      Prod.map
        (fun n ↦ x₀.left * (φ x₀.right) n)
        fun g ↦ x₀.right * g

Left translation on a semidirect product acts separately on the two product coordinates: the
group coordinate of the translating element is fixed, so its action on `N` does not depend on the
point being translated.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SemidirectProductHaar.lean

complete

theorem SemidirectProduct.isMulLeftInvariant_prodMeasure.{u_1, u_2}
  {N : Type u_1} {G : Type u_2} [Group N] [Group G] [TopologicalSpace N]
  [TopologicalSpace G] [IsTopologicalGroup N] [IsTopologicalGroup G]
  [MeasurableSpace N] [BorelSpace N] [MeasurableSpace G] [BorelSpace G]
  [SecondCountableTopology G] {φ : G →* MulAut N}
  {ν : MeasureTheory.Measure N} {lam : MeasureTheory.Measure G}
  [IsTopologicalGroup (N ⋊[φ] G)] [MeasureTheory.SFinite ν]
  [MeasureTheory.SFinite lam] [ν.IsMulLeftInvariant] {χ : G →* ENNReal}
  (hφν : ∀ (g : G), MeasureTheory.Measure.map (⇑(φ g)) ν = χ g • ν)
  (hlam :
    ∀ (g₀ : G),
      MeasureTheory.Measure.map (fun g ↦ g₀ * g) lam = χ g₀⁻¹ • lam)
  (hcontinuousφ : ∀ (g : G), Continuous ⇑(φ g)) :
  (SemidirectProduct.prodMeasure φ ν lam).IsMulLeftInvariant

theorem SemidirectProduct.isMulLeftInvariant_prodMeasure.{u_1,
    u_2}
  {N : Type u_1} {G : Type u_2} [Group N]
  [Group G] [TopologicalSpace N]
  [TopologicalSpace G]
  [IsTopologicalGroup N]
  [IsTopologicalGroup G]
  [MeasurableSpace N] [BorelSpace N]
  [MeasurableSpace G] [BorelSpace G]
  [SecondCountableTopology G]
  {φ : G →* MulAut N}
  {ν : MeasureTheory.Measure N}
  {lam : MeasureTheory.Measure G}
  [IsTopologicalGroup (N ⋊[φ] G)]
  [MeasureTheory.SFinite ν]
  [MeasureTheory.SFinite lam]
  [ν.IsMulLeftInvariant]
  {χ : G →* ENNReal}
  (hφν :
    ∀ (g : G),
      MeasureTheory.Measure.map (⇑(φ g))
          ν =
        χ g • ν)
  (hlam :
    ∀ (g₀ : G),
      MeasureTheory.Measure.map
          (fun g ↦ g₀ * g) lam =
        χ g₀⁻¹ • lam)
  (hcontinuousφ :
    ∀ (g : G), Continuous ⇑(φ g)) :
  (SemidirectProduct.prodMeasure φ ν
      lam).IsMulLeftInvariant

The transported product measure is left invariant when the measure on `N` is left invariant, the
measure on `G` is relatively invariant, and the two scaling factors are reciprocal.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SemidirectProductHaar.lean

complete

theorem SemidirectProduct.isFiniteMeasureOnCompacts_prodMeasure.{u_1, u_2}
  {N : Type u_1} {G : Type u_2} [Group N] [Group G] [TopologicalSpace N]
  [TopologicalSpace G] [T2Space N] [T2Space G] [MeasurableSpace N]
  [BorelSpace N] [MeasurableSpace G] [BorelSpace G]
  [SecondCountableTopology G] {φ : G →* MulAut N}
  {ν : MeasureTheory.Measure N} {lam : MeasureTheory.Measure G}
  [MeasureTheory.SFinite lam]
  [MeasureTheory.IsFiniteMeasureOnCompacts ν]
  [MeasureTheory.IsFiniteMeasureOnCompacts lam] :
  MeasureTheory.IsFiniteMeasureOnCompacts
    (SemidirectProduct.prodMeasure φ ν lam)

theorem SemidirectProduct.isFiniteMeasureOnCompacts_prodMeasure.{u_1,
    u_2}
  {N : Type u_1} {G : Type u_2} [Group N]
  [Group G] [TopologicalSpace N]
  [TopologicalSpace G] [T2Space N]
  [T2Space G] [MeasurableSpace N]
  [BorelSpace N] [MeasurableSpace G]
  [BorelSpace G]
  [SecondCountableTopology G]
  {φ : G →* MulAut N}
  {ν : MeasureTheory.Measure N}
  {lam : MeasureTheory.Measure G}
  [MeasureTheory.SFinite lam]
  [MeasureTheory.IsFiniteMeasureOnCompacts
      ν]
  [MeasureTheory.IsFiniteMeasureOnCompacts
      lam] :
  MeasureTheory.IsFiniteMeasureOnCompacts
    (SemidirectProduct.prodMeasure φ ν
      lam)

The transported product measure is finite on compact sets.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SemidirectProductHaar.lean

complete

theorem SemidirectProduct.isOpenPosMeasure_prodMeasure.{u_1, u_2} {N : Type u_1}
  {G : Type u_2} [Group N] [Group G] [TopologicalSpace N]
  [TopologicalSpace G] [MeasurableSpace N] [BorelSpace N]
  [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G]
  {φ : G →* MulAut N} {ν : MeasureTheory.Measure N}
  {lam : MeasureTheory.Measure G} [MeasureTheory.SFinite lam]
  [ν.IsOpenPosMeasure] [lam.IsOpenPosMeasure] :
  (SemidirectProduct.prodMeasure φ ν lam).IsOpenPosMeasure

theorem SemidirectProduct.isOpenPosMeasure_prodMeasure.{u_1,
    u_2}
  {N : Type u_1} {G : Type u_2} [Group N]
  [Group G] [TopologicalSpace N]
  [TopologicalSpace G] [MeasurableSpace N]
  [BorelSpace N] [MeasurableSpace G]
  [BorelSpace G]
  [SecondCountableTopology G]
  {φ : G →* MulAut N}
  {ν : MeasureTheory.Measure N}
  {lam : MeasureTheory.Measure G}
  [MeasureTheory.SFinite lam]
  [ν.IsOpenPosMeasure]
  [lam.IsOpenPosMeasure] :
  (SemidirectProduct.prodMeasure φ ν
      lam).IsOpenPosMeasure

The transported product measure is positive on nonempty open sets.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SemidirectProductHaar.lean

complete

theorem SemidirectProduct.isHaarMeasure_prodMeasure.{u_1, u_2} {N : Type u_1}
  {G : Type u_2} [Group N] [Group G] [TopologicalSpace N]
  [TopologicalSpace G] [IsTopologicalGroup N] [IsTopologicalGroup G]
  [T2Space N] [T2Space G] [MeasurableSpace N] [BorelSpace N]
  [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G]
  {φ : G →* MulAut N} {ν : MeasureTheory.Measure N}
  {lam : MeasureTheory.Measure G} [IsTopologicalGroup (N ⋊[φ] G)]
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite lam]
  [ν.IsMulLeftInvariant] [MeasureTheory.IsFiniteMeasureOnCompacts ν]
  [ν.IsOpenPosMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts lam]
  [lam.IsOpenPosMeasure] {χ : G →* ENNReal}
  (hφν : ∀ (g : G), MeasureTheory.Measure.map (⇑(φ g)) ν = χ g • ν)
  (hlam :
    ∀ (g₀ : G),
      MeasureTheory.Measure.map (fun g ↦ g₀ * g) lam = χ g₀⁻¹ • lam)
  (hcontinuousφ : ∀ (g : G), Continuous ⇑(φ g)) :
  (SemidirectProduct.prodMeasure φ ν lam).IsHaarMeasure

theorem SemidirectProduct.isHaarMeasure_prodMeasure.{u_1,
    u_2}
  {N : Type u_1} {G : Type u_2} [Group N]
  [Group G] [TopologicalSpace N]
  [TopologicalSpace G]
  [IsTopologicalGroup N]
  [IsTopologicalGroup G] [T2Space N]
  [T2Space G] [MeasurableSpace N]
  [BorelSpace N] [MeasurableSpace G]
  [BorelSpace G]
  [SecondCountableTopology G]
  {φ : G →* MulAut N}
  {ν : MeasureTheory.Measure N}
  {lam : MeasureTheory.Measure G}
  [IsTopologicalGroup (N ⋊[φ] G)]
  [MeasureTheory.SFinite ν]
  [MeasureTheory.SFinite lam]
  [ν.IsMulLeftInvariant]
  [MeasureTheory.IsFiniteMeasureOnCompacts
      ν]
  [ν.IsOpenPosMeasure]
  [MeasureTheory.IsFiniteMeasureOnCompacts
      lam]
  [lam.IsOpenPosMeasure]
  {χ : G →* ENNReal}
  (hφν :
    ∀ (g : G),
      MeasureTheory.Measure.map (⇑(φ g))
          ν =
        χ g • ν)
  (hlam :
    ∀ (g₀ : G),
      MeasureTheory.Measure.map
          (fun g ↦ g₀ * g) lam =
        χ g₀⁻¹ • lam)
  (hcontinuousφ :
    ∀ (g : G), Continuous ⇑(φ g)) :
  (SemidirectProduct.prodMeasure φ ν
      lam).IsHaarMeasure

Left Haar measure of a topological semidirect product is the product of Haar measure of the
normal factor and a relatively invariant measure on the acting factor.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SemidirectProductHaar.lean

complete

theorem SemidirectProduct.exists_haar_eq_smul_prodMeasure.{u_1, u_2}
  {N : Type u_1} {G : Type u_2} [Group N] [Group G] [TopologicalSpace N]
  [TopologicalSpace G] [IsTopologicalGroup N] [IsTopologicalGroup G]
  [T2Space N] [T2Space G] [MeasurableSpace N] [BorelSpace N]
  [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology N]
  [SecondCountableTopology G] {φ : G →* MulAut N}
  {ν : MeasureTheory.Measure N} {lam : MeasureTheory.Measure G}
  [IsTopologicalGroup (N ⋊[φ] G)] [LocallyCompactSpace N]
  [LocallyCompactSpace G] [MeasureTheory.SFinite ν]
  [MeasureTheory.SFinite lam] [ν.IsMulLeftInvariant]
  [MeasureTheory.IsFiniteMeasureOnCompacts ν] [ν.IsOpenPosMeasure]
  [MeasureTheory.IsFiniteMeasureOnCompacts lam] [lam.IsOpenPosMeasure]
  {χ : G →* ENNReal}
  (hφν : ∀ (g : G), MeasureTheory.Measure.map (⇑(φ g)) ν = χ g • ν)
  (hlam :
    ∀ (g₀ : G),
      MeasureTheory.Measure.map (fun g ↦ g₀ * g) lam = χ g₀⁻¹ • lam)
  (hcontinuousφ : ∀ (g : G), Continuous ⇑(φ g)) :
  ∃ c,
    c ≠ 0 ∧
      c ≠ ⊤ ∧
        ∀ (s : Set (N ⋊[φ] G)),
          MeasureTheory.Measure.haar s =
            c * (SemidirectProduct.prodMeasure φ ν lam) s

theorem SemidirectProduct.exists_haar_eq_smul_prodMeasure.{u_1,
    u_2}
  {N : Type u_1} {G : Type u_2} [Group N]
  [Group G] [TopologicalSpace N]
  [TopologicalSpace G]
  [IsTopologicalGroup N]
  [IsTopologicalGroup G] [T2Space N]
  [T2Space G] [MeasurableSpace N]
  [BorelSpace N] [MeasurableSpace G]
  [BorelSpace G]
  [SecondCountableTopology N]
  [SecondCountableTopology G]
  {φ : G →* MulAut N}
  {ν : MeasureTheory.Measure N}
  {lam : MeasureTheory.Measure G}
  [IsTopologicalGroup (N ⋊[φ] G)]
  [LocallyCompactSpace N]
  [LocallyCompactSpace G]
  [MeasureTheory.SFinite ν]
  [MeasureTheory.SFinite lam]
  [ν.IsMulLeftInvariant]
  [MeasureTheory.IsFiniteMeasureOnCompacts
      ν]
  [ν.IsOpenPosMeasure]
  [MeasureTheory.IsFiniteMeasureOnCompacts
      lam]
  [lam.IsOpenPosMeasure]
  {χ : G →* ENNReal}
  (hφν :
    ∀ (g : G),
      MeasureTheory.Measure.map (⇑(φ g))
          ν =
        χ g • ν)
  (hlam :
    ∀ (g₀ : G),
      MeasureTheory.Measure.map
          (fun g ↦ g₀ * g) lam =
        χ g₀⁻¹ • lam)
  (hcontinuousφ :
    ∀ (g : G), Continuous ⇑(φ g)) :
  ∃ c,
    c ≠ 0 ∧
      c ≠ ⊤ ∧
        ∀ (s : Set (N ⋊[φ] G)),
          MeasureTheory.Measure.haar s =
            c *
              (SemidirectProduct.prodMeasure
                  φ ν lam)
                s

Uniqueness of Haar measure identifies the canonical Haar measure of a semidirect product with
the explicit product measure, up to a positive finite factor.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/SemidirectProductHaar.lean

complete

theorem SemidirectProduct.exists_map_right_haar_restrict_le.{u_1, u_2}
  {N : Type u_1} {G : Type u_2} [Group N] [Group G] [TopologicalSpace N]
  [TopologicalSpace G] [IsTopologicalGroup N] [IsTopologicalGroup G]
  [T2Space N] [T2Space G] [MeasurableSpace N] [BorelSpace N]
  [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology N]
  [SecondCountableTopology G] {φ : G →* MulAut N}
  {ν : MeasureTheory.Measure N} {lam : MeasureTheory.Measure G}
  [IsTopologicalGroup (N ⋊[φ] G)] [LocallyCompactSpace N]
  [LocallyCompactSpace G] [MeasureTheory.SFinite ν]
  [MeasureTheory.SFinite lam] [ν.IsMulLeftInvariant]
  [MeasureTheory.IsFiniteMeasureOnCompacts ν] [ν.IsOpenPosMeasure]
  [MeasureTheory.IsFiniteMeasureOnCompacts lam] [lam.IsOpenPosMeasure]
  {χ : G →* ENNReal}
  (hφν : ∀ (g : G), MeasureTheory.Measure.map (⇑(φ g)) ν = χ g • ν)
  (hlam :
    ∀ (g₀ : G),
      MeasureTheory.Measure.map (fun g ↦ g₀ * g) lam = χ g₀⁻¹ • lam)
  (hcontinuousφ : ∀ (g : G), Continuous ⇑(φ g)) {S : Set (N ⋊[φ] G)}
  (hS : IsCompact S) :
  ∃ C,
    C ≠ ⊤ ∧
      MeasureTheory.Measure.map SemidirectProduct.right
          (MeasureTheory.Measure.haar.restrict S) ≤
        C • lam.restrict (SemidirectProduct.right '' S)

theorem SemidirectProduct.exists_map_right_haar_restrict_le.{u_1,
    u_2}
  {N : Type u_1} {G : Type u_2} [Group N]
  [Group G] [TopologicalSpace N]
  [TopologicalSpace G]
  [IsTopologicalGroup N]
  [IsTopologicalGroup G] [T2Space N]
  [T2Space G] [MeasurableSpace N]
  [BorelSpace N] [MeasurableSpace G]
  [BorelSpace G]
  [SecondCountableTopology N]
  [SecondCountableTopology G]
  {φ : G →* MulAut N}
  {ν : MeasureTheory.Measure N}
  {lam : MeasureTheory.Measure G}
  [IsTopologicalGroup (N ⋊[φ] G)]
  [LocallyCompactSpace N]
  [LocallyCompactSpace G]
  [MeasureTheory.SFinite ν]
  [MeasureTheory.SFinite lam]
  [ν.IsMulLeftInvariant]
  [MeasureTheory.IsFiniteMeasureOnCompacts
      ν]
  [ν.IsOpenPosMeasure]
  [MeasureTheory.IsFiniteMeasureOnCompacts
      lam]
  [lam.IsOpenPosMeasure]
  {χ : G →* ENNReal}
  (hφν :
    ∀ (g : G),
      MeasureTheory.Measure.map (⇑(φ g))
          ν =
        χ g • ν)
  (hlam :
    ∀ (g₀ : G),
      MeasureTheory.Measure.map
          (fun g ↦ g₀ * g) lam =
        χ g₀⁻¹ • lam)
  (hcontinuousφ :
    ∀ (g : G), Continuous ⇑(φ g))
  {S : Set (N ⋊[φ] G)}
  (hS : IsCompact S) :
  ∃ C,
    C ≠ ⊤ ∧
      MeasureTheory.Measure.map
          SemidirectProduct.right
          (MeasureTheory.Measure.haar.restrict
            S) ≤
        C •
          lam.restrict
            (SemidirectProduct.right '' S)

On a compact set, the image of the semidirect-product Haar measure under the projection to the
acting factor is dominated by the relatively invariant measure of that factor.  The constant is the
Haar measure of the compact projection to the normal factor.

This is the estimate needed to bound an integral over a compact subset of the group by an integral
over the acting factor alone, which is the first step of a quotient-integral estimate for an induced
representation.

The relatively invariant measure on G comes from twisting Haar measure by the character: for a monoid homomorphism χ:G\to[0,∞], left translation rescales χ\,\mathrm dκ by χ(g_0^{-1}). Finiteness on compacts and positivity on open sets are inherited from the two factors through the product homeomorphism, so uniqueness of Haar measure identifies the canonical Haar measure of the semidirect product with the product measure up to a positive finite factor.

The estimate extracted for use downstream bounds, on a compact subset of the group, the image of Haar measure under the projection to the acting factor by the relatively invariant measure, with constant the Haar measure of the compact projection to the normal factor.

Haar measure under a group automorphism

Theorem5.7.8

uses 1used by 1✓L∃∀N

Transporting Haar measure through an automorphism. A continuous group automorphism with continuous inverse pushes Haar measure to a Haar measure, hence — by uniqueness — to a positive finite multiple of the original one. Restricted to a measurable set, the image measure is exactly that multiple of Haar measure restricted to the image set.

Lean code for Theorem5.7.8●2 theorems

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/HaarAutomorphism.lean

complete

theorem MeasureTheory.exists_map_continuousMulEquiv_haar_eq_smul_haar.{u_1}
  {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G]
  [SecondCountableTopology G] (σ : G ≃ₜ* G) :
  ∃ c,
    c ≠ 0 ∧
      c ≠ ⊤ ∧
        MeasureTheory.Measure.map (⇑σ) MeasureTheory.Measure.haar =
          c • MeasureTheory.Measure.haar

theorem MeasureTheory.exists_map_continuousMulEquiv_haar_eq_smul_haar.{u_1}
  {G : Type u_1} [Group G]
  [TopologicalSpace G]
  [IsTopologicalGroup G]
  [MeasurableSpace G] [BorelSpace G]
  [LocallyCompactSpace G]
  [SecondCountableTopology G]
  (σ : G ≃ₜ* G) :
  ∃ c,
    c ≠ 0 ∧
      c ≠ ⊤ ∧
        MeasureTheory.Measure.map (⇑σ)
            MeasureTheory.Measure.haar =
          c • MeasureTheory.Measure.haar

Pushing Haar measure forward along a topological group automorphism gives a positive finite
multiple of Haar measure.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/HaarAutomorphism.lean

complete

theorem MeasureTheory.exists_map_continuousMulEquiv_haar_restrict_eq_smul_haar_restrict.{u_1}
  {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G]
  [SecondCountableTopology G] (σ : G ≃ₜ* G) {s : Set G}
  (hs : MeasurableSet s) :
  ∃ c,
    c ≠ 0 ∧
      c ≠ ⊤ ∧
        MeasureTheory.Measure.map (⇑σ)
            (MeasureTheory.Measure.haar.restrict s) =
          c • MeasureTheory.Measure.haar.restrict (⇑σ '' s)

theorem MeasureTheory.exists_map_continuousMulEquiv_haar_restrict_eq_smul_haar_restrict.{u_1}
  {G : Type u_1} [Group G]
  [TopologicalSpace G]
  [IsTopologicalGroup G]
  [MeasurableSpace G] [BorelSpace G]
  [LocallyCompactSpace G]
  [SecondCountableTopology G]
  (σ : G ≃ₜ* G) {s : Set G}
  (hs : MeasurableSet s) :
  ∃ c,
    c ≠ 0 ∧
      c ≠ ⊤ ∧
        MeasureTheory.Measure.map (⇑σ)
            (MeasureTheory.Measure.haar.restrict
              s) =
          c •
            MeasureTheory.Measure.haar.restrict
              (⇑σ '' s)

The image of a restricted Haar measure under a topological group automorphism is a positive
finite multiple of Haar measure restricted to the image set.

This is the form in which a compactly supported estimate survives a coordinate change of the group. The case needed here is the contragredient map L\mapsto (L^\dagger)^{-1} of a general linear group, which is an automorphism because it is the composition of two anti-automorphisms, inversion and the adjoint.

Contragredient orbits of the general linear group

Theorem5.7.9

Statement uses 3

Statement dependency previews

Preview

Theorem 5.1.21

Loading preview

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

used by 1✓L∃∀N

Contragredient orbit maps and Haar measure. The contragredient map L\mapsto (L^{-1})^\dagger is an automorphism of the group of invertible operators on a finite-dimensional real inner-product space: it composes the two anti-automorphisms L\mapsto L^{-1} and L\mapsto L^\dagger, and it is an involution, so it is its own inverse. Evaluation A\mapsto A\xi at a nonzero vector is a surjective linear map, a rank-one operator realizing any prescribed value.

Lean code for Theorem5.7.9●18 declarations

defdefined in LeanRidgelet/ToMathlib/LieGroup/GeneralLinearHaar.lean

complete

def ContinuousLinearMap.contragredientUnit.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (L : (E →L[ℝ] E)ˣ) : (E →L[ℝ] E)ˣ

def ContinuousLinearMap.contragredientUnit.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (L : (E →L[ℝ] E)ˣ) : (E →L[ℝ] E)ˣ

Implementation after :=

:= (↑L⁻¹ : E →L[ℝ] E).adjoint
  inv := (↑L : E →L[ℝ] E).adjoint
  val_inv := by
    change ((↑L⁻¹ : E →L[ℝ] E).adjoint) ∘L ((↑L : E →L[ℝ] E).adjoint) = 1
    rw [← ContinuousLinearMap.adjoint_comp]
    change ((↑L : E →L[ℝ] E) * (↑L⁻¹ : E →L[ℝ] E)).adjoint = 1
    rw [← Units.val_mul, mul_inv_cancel]
    simp
  inv_val := by
    change ((↑L : E →L[ℝ] E).adjoint) ∘L ((↑L⁻¹ : E →L[ℝ] E).adjoint) = 1
    rw [← ContinuousLinearMap.adjoint_comp]
    change ((↑L⁻¹ : E →L[ℝ] E) * (↑L : E →L[ℝ] E)).adjoint = 1
    rw [← Units.val_mul, inv_mul_cancel]
    simp

The adjoint of the inverse of an invertible operator, as an invertible operator.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/GeneralLinearHaar.lean

complete

theorem ContinuousLinearMap.contragredientUnit_val.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (L : (E →L[ℝ] E)ˣ) :
  ↑(ContinuousLinearMap.contragredientUnit L) =
    ContinuousLinearMap.adjoint ↑L⁻¹

theorem ContinuousLinearMap.contragredientUnit_val.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (L : (E →L[ℝ] E)ˣ) :
  ↑(ContinuousLinearMap.contragredientUnit
        L) =
    ContinuousLinearMap.adjoint ↑L⁻¹

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/GeneralLinearHaar.lean

complete

theorem ContinuousLinearMap.contragredientUnit_inv_val.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (L : (E →L[ℝ] E)ˣ) :
  ↑(ContinuousLinearMap.contragredientUnit L)⁻¹ =
    ContinuousLinearMap.adjoint ↑L

theorem ContinuousLinearMap.contragredientUnit_inv_val.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (L : (E →L[ℝ] E)ˣ) :
  ↑(ContinuousLinearMap.contragredientUnit
          L)⁻¹ =
    ContinuousLinearMap.adjoint ↑L

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/GeneralLinearHaar.lean

complete

theorem ContinuousLinearMap.contragredientUnit_mul.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (L M : (E →L[ℝ] E)ˣ) :
  ContinuousLinearMap.contragredientUnit (L * M) =
    ContinuousLinearMap.contragredientUnit L *
      ContinuousLinearMap.contragredientUnit M

theorem ContinuousLinearMap.contragredientUnit_mul.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (L M : (E →L[ℝ] E)ˣ) :
  ContinuousLinearMap.contragredientUnit
      (L * M) =
    ContinuousLinearMap.contragredientUnit
        L *
      ContinuousLinearMap.contragredientUnit
        M

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/GeneralLinearHaar.lean

complete

theorem ContinuousLinearMap.contragredientUnit_one.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] : ContinuousLinearMap.contragredientUnit 1 = 1

theorem ContinuousLinearMap.contragredientUnit_one.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] :
  ContinuousLinearMap.contragredientUnit
      1 =
    1

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/GeneralLinearHaar.lean

complete

theorem ContinuousLinearMap.contragredientUnit_involutive.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] :
  Function.Involutive ContinuousLinearMap.contragredientUnit

theorem ContinuousLinearMap.contragredientUnit_involutive.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] :
  Function.Involutive
    ContinuousLinearMap.contragredientUnit

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/GeneralLinearHaar.lean

complete

theorem ContinuousLinearMap.continuous_contragredientUnit_val.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] :
  Continuous fun L ↦ ↑(ContinuousLinearMap.contragredientUnit L)

theorem ContinuousLinearMap.continuous_contragredientUnit_val.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] :
  Continuous fun L ↦
    ↑(ContinuousLinearMap.contragredientUnit
        L)

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/GeneralLinearHaar.lean

complete

theorem ContinuousLinearMap.continuous_contragredientUnit.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] :
  Continuous ContinuousLinearMap.contragredientUnit

theorem ContinuousLinearMap.continuous_contragredientUnit.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] :
  Continuous
    ContinuousLinearMap.contragredientUnit

defdefined in LeanRidgelet/ToMathlib/LieGroup/GeneralLinearHaar.lean

complete

def ContinuousLinearMap.contragredientUnits.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] : (E →L[ℝ] E)ˣ ≃ₜ* (E →L[ℝ] E)ˣ

def ContinuousLinearMap.contragredientUnits.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] :
  (E →L[ℝ] E)ˣ ≃ₜ* (E →L[ℝ] E)ˣ

Implementation after :=

:= contragredientUnit
  invFun := contragredientUnit
  left_inv := contragredientUnit_involutive
  right_inv := contragredientUnit_involutive
  map_mul' := contragredientUnit_mul
  continuous_toFun := continuous_contragredientUnit
  continuous_invFun := continuous_contragredientUnit

The contragredient map `L ↦ (L⁻¹)†` as a topological automorphism of the group of invertible
operators.  It is an involution, so it is its own inverse.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/GeneralLinearHaar.lean

complete

theorem ContinuousLinearMap.contragredientUnits_apply.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (L : (E →L[ℝ] E)ˣ) :
  ContinuousLinearMap.contragredientUnits L =
    ContinuousLinearMap.contragredientUnit L

theorem ContinuousLinearMap.contragredientUnits_apply.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (L : (E →L[ℝ] E)ˣ) :
  ContinuousLinearMap.contragredientUnits
      L =
    ContinuousLinearMap.contragredientUnit
      L

defdefined in LeanRidgelet/ToMathlib/LieGroup/GeneralLinearHaar.lean

complete

def ContinuousLinearMap.evalLinearMap.{u_1} (E : Type u_1)
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (xi : E) :
  (E →L[ℝ] E) →ₗ[ℝ] E

def ContinuousLinearMap.evalLinearMap.{u_1}
  (E : Type u_1) [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (xi : E) :
  (E →L[ℝ] E) →ₗ[ℝ] E

Implementation after :=

:= A xi
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

Evaluation of a continuous linear operator at a fixed vector, as a linear map.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/GeneralLinearHaar.lean

complete

theorem ContinuousLinearMap.evalLinearMap_apply.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (xi : E)
  (A : E →L[ℝ] E) : (ContinuousLinearMap.evalLinearMap E xi) A = A xi

theorem ContinuousLinearMap.evalLinearMap_apply.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (xi : E)
  (A : E →L[ℝ] E) :
  (ContinuousLinearMap.evalLinearMap E xi)
      A =
    A xi

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/GeneralLinearHaar.lean

complete

theorem ContinuousLinearMap.evalLinearMap_surjective.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {xi : E}
  (hxi : xi ≠ 0) :
  Function.Surjective ⇑(ContinuousLinearMap.evalLinearMap E xi)

theorem ContinuousLinearMap.evalLinearMap_surjective.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {xi : E}
  (hxi : xi ≠ 0) :
  Function.Surjective
    ⇑(ContinuousLinearMap.evalLinearMap E
        xi)

Evaluation at a nonzero vector is onto: a rank-one operator sends it to any prescribed
vector.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/GeneralLinearHaar.lean

complete

theorem ContinuousLinearMap.exists_map_contragredientOrbit_haar_restrict_le.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  [MeasurableSpace (E →L[ℝ] E)] [BorelSpace (E →L[ℝ] E)]
  [MeasurableSpace (E →L[ℝ] E)ˣ] [BorelSpace (E →L[ℝ] E)ˣ]
  (μ : MeasureTheory.Measure (E →L[ℝ] E)) [μ.IsAddHaarMeasure]
  (ν : MeasureTheory.Measure E) [ν.IsAddHaarMeasure] {xi : E}
  (hxi : xi ≠ 0) {S : Set (E →L[ℝ] E)ˣ} (hS : IsCompact S) :
  ∃ C B,
    C ≠ ⊤ ∧
      IsCompact B ∧
        MeasureTheory.Measure.map
            (fun L ↦
              (ContinuousLinearMap.evalLinearMap E xi)
                ↑(ContinuousLinearMap.contragredientUnit L))
            (MeasureTheory.Measure.haar.restrict S) ≤
          C • ν.restrict B

theorem ContinuousLinearMap.exists_map_contragredientOrbit_haar_restrict_le.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [MeasurableSpace (E →L[ℝ] E)]
  [BorelSpace (E →L[ℝ] E)]
  [MeasurableSpace (E →L[ℝ] E)ˣ]
  [BorelSpace (E →L[ℝ] E)ˣ]
  (μ : MeasureTheory.Measure (E →L[ℝ] E))
  [μ.IsAddHaarMeasure]
  (ν : MeasureTheory.Measure E)
  [ν.IsAddHaarMeasure] {xi : E}
  (hxi : xi ≠ 0) {S : Set (E →L[ℝ] E)ˣ}
  (hS : IsCompact S) :
  ∃ C B,
    C ≠ ⊤ ∧
      IsCompact B ∧
        MeasureTheory.Measure.map
            (fun L ↦
              (ContinuousLinearMap.evalLinearMap
                  E xi)
                ↑(ContinuousLinearMap.contragredientUnit
                    L))
            (MeasureTheory.Measure.haar.restrict
              S) ≤
          C • ν.restrict B

On a compact set of invertible operators, the image of Haar measure under a contragredient orbit
map `L ↦ (L⁻¹)† ξ` is dominated by a finite multiple of additive Haar measure of the vector space,
restricted to the compact image.

The three factors of the estimate are the Haar transport along the contragredient automorphism, the
comparison between Haar measure of the unit group and additive Haar measure of the operator algebra,
and the pushforward bound along the surjective evaluation map.

defdefined in LeanRidgelet/ToMathlib/LieGroup/GeneralLinearHaar.lean

complete

def ContinuousLinearMap.adjointEvalLinearMap.{u_1} (E : Type u_1)
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (xi : E) : (E →L[ℝ] E) →ₗ[ℝ] E

def ContinuousLinearMap.adjointEvalLinearMap.{u_1}
  (E : Type u_1) [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (xi : E) :
  (E →L[ℝ] E) →ₗ[ℝ] E

Implementation after :=

:= A.adjoint xi
  map_add' A B := by
    have hadd : (A + B).adjoint = A.adjoint + B.adjoint :=
      map_add ContinuousLinearMap.adjoint A B
    simp [hadd]
  map_smul' c A := by
    have hsmul : (c • A).adjoint = c • A.adjoint := by
      simp [map_smulₛₗ ContinuousLinearMap.adjoint c A]
    simp [hsmul]

Evaluation of the adjoint of an operator at a fixed vector, as a linear map.  Unlike the
contragredient map, this one is linear on the whole operator algebra, because it does not invert.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/GeneralLinearHaar.lean

complete

theorem ContinuousLinearMap.adjointEvalLinearMap_apply.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (xi : E) (A : E →L[ℝ] E) :
  (ContinuousLinearMap.adjointEvalLinearMap E xi) A =
    (ContinuousLinearMap.adjoint A) xi

theorem ContinuousLinearMap.adjointEvalLinearMap_apply.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (xi : E)
  (A : E →L[ℝ] E) :
  (ContinuousLinearMap.adjointEvalLinearMap
        E xi)
      A =
    (ContinuousLinearMap.adjoint A) xi

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/GeneralLinearHaar.lean

complete

theorem ContinuousLinearMap.adjointEvalLinearMap_surjective.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  {xi : E} (hxi : xi ≠ 0) :
  Function.Surjective ⇑(ContinuousLinearMap.adjointEvalLinearMap E xi)

theorem ContinuousLinearMap.adjointEvalLinearMap_surjective.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] {xi : E}
  (hxi : xi ≠ 0) :
  Function.Surjective
    ⇑(ContinuousLinearMap.adjointEvalLinearMap
        E xi)

Evaluating the adjoint at a nonzero vector is onto, because taking adjoints is involutive.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/GeneralLinearHaar.lean

complete

theorem ContinuousLinearMap.exists_map_adjointOrbit_haar_restrict_le.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  [MeasurableSpace (E →L[ℝ] E)] [BorelSpace (E →L[ℝ] E)]
  [MeasurableSpace (E →L[ℝ] E)ˣ] [BorelSpace (E →L[ℝ] E)ˣ]
  (μ : MeasureTheory.Measure (E →L[ℝ] E)) [μ.IsAddHaarMeasure]
  (ν : MeasureTheory.Measure E) [ν.IsAddHaarMeasure] {xi : E}
  (hxi : xi ≠ 0) {S : Set (E →L[ℝ] E)ˣ} (hS : IsCompact S) :
  ∃ C B,
    C ≠ ⊤ ∧
      IsCompact B ∧
        MeasureTheory.Measure.map
            (fun L ↦ (ContinuousLinearMap.adjointEvalLinearMap E xi) ↑L)
            (MeasureTheory.Measure.haar.restrict S) ≤
          C • ν.restrict B

theorem ContinuousLinearMap.exists_map_adjointOrbit_haar_restrict_le.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [MeasurableSpace (E →L[ℝ] E)]
  [BorelSpace (E →L[ℝ] E)]
  [MeasurableSpace (E →L[ℝ] E)ˣ]
  [BorelSpace (E →L[ℝ] E)ˣ]
  (μ : MeasureTheory.Measure (E →L[ℝ] E))
  [μ.IsAddHaarMeasure]
  (ν : MeasureTheory.Measure E)
  [ν.IsAddHaarMeasure] {xi : E}
  (hxi : xi ≠ 0) {S : Set (E →L[ℝ] E)ˣ}
  (hS : IsCompact S) :
  ∃ C B,
    C ≠ ⊤ ∧
      IsCompact B ∧
        MeasureTheory.Measure.map
            (fun L ↦
              (ContinuousLinearMap.adjointEvalLinearMap
                  E xi)
                ↑L)
            (MeasureTheory.Measure.haar.restrict
              S) ≤
          C • ν.restrict B

On a compact set of invertible operators, the image of Haar measure under an adjoint orbit map
`L ↦ L† ξ` is dominated by a finite multiple of additive Haar measure of the vector space,
restricted to the compact image.

This is the variant needed when the orbit map is composed with inversion, and it is cheaper than the
contragredient one: taking adjoints and evaluating are both linear on the operator algebra, so only
the unit-group comparison and the linear pushforward bound are used, with no Haar transport along a
group automorphism.

Chaining the three preceding estimates along L\mapsto(L^{-1})^\dagger\mapsto\text{(inclusion into the algebra)}\mapsto A\xi bounds, on a compact set of invertible operators, the image of Haar measure under a contragredient orbit map by a finite multiple of Lebesgue measure restricted to the compact image. Each of the three steps preserves the compact restriction, which is what makes the composite usable for functions that are only locally integrable.

The variant for the adjoint orbit map L\mapsto L^\dagger\xi — the orbit map composed with inversion, which is the form a group convolution consumes — is cheaper: taking adjoints and evaluating are both linear on the operator algebra, so only the unit-group comparison and the linear pushforward bound are used, with no Haar transport along an automorphism.

The symmetric-space material that used to close this page — the abstract Helgason--Fourier layer and the two concrete models it is instantiated at — is now the ToMathlib / Symmetric spaces page.