5.6. Mathlib candidates: unitary representations and groups🔗

Reusable representation-theoretic and topological-group infrastructure, including conjugation, pointwise Lp actions, homogeneous-space cocycles, semidirect products, and the affine orbit.

Unitary equivalence of representations

Theorem5.6.1

uses 0

Used by 6

Reverse dependency previews

Preview

Theorem 4.3.2

Loading preview

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

✓L∃∀N

Transporting a unitary representation across a Hilbert-space equivalence. A linear isometric equivalence U:H\simeq K conjugates every unitary representation by \widehat\pi(g)=U\pi(g)U^{-1}. The maps U and U⁻¹ are bundled as continuous intertwiners in the two directions; conjugating back recovers the original representation, and topological irreducibility is therefore equivalent on the two sides. Restriction along a surjective group homomorphism likewise preserves and reflects invariant closed subspaces and irreducibility. Since Mathlib's ContRepresentation does not impose continuity in the group variable, strong continuity is recorded separately as continuity of every orbit map and is preserved by restriction along a continuous homomorphism. These are the abstract steps that turn a Plancherel transform into a representation equivalence without making any pointwise choice of L^2 representatives.

Lean code for Theorem5.6.1●14 declarations

defdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

def UnitaryRepresentation.restrict.{u_1, u_2, u_3} {G : Type u_1}
  {H : Type u_2} [Group G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] {G' : Type u_3} [Group G']
  (π : UnitaryRepresentation G H) (φ : G' →* G) :
  UnitaryRepresentation G' H

def UnitaryRepresentation.restrict.{u_1, u_2,
    u_3}
  {G : Type u_1} {H : Type u_2} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] {G' : Type u_3}
  [Group G']
  (π : UnitaryRepresentation G H)
  (φ : G' →* G) :
  UnitaryRepresentation G' H

Implementation after :=

:=
  π.comp φ

Restrict a unitary representation along a group homomorphism.

defdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

def UnitaryRepresentation.IsStronglyContinuous.{u_1, u_2} {G : Type u_1}
  {H : Type u_2} [Group G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [TopologicalSpace G]
  (π : UnitaryRepresentation G H) : Prop

def UnitaryRepresentation.IsStronglyContinuous.{u_1,
    u_2}
  {G : Type u_1} {H : Type u_2} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [TopologicalSpace G]
  (π : UnitaryRepresentation G H) : Prop

Implementation after :=

:=
  ∀ x : H, Continuous fun g : G ↦ (π g : H →L[ℂ] H) x

Strong continuity of a unitary representation: every orbit map is continuous in the group
variable.  Mathlib's `ContRepresentation` only says that each represented operator is continuous;
it deliberately imposes no topology on the acting group.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

theorem UnitaryRepresentation.IsStronglyContinuous.restrict.{u_1, u_2, u_3}
  {G : Type u_1} {H : Type u_2} [Group G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] {G' : Type u_3} [Group G']
  [TopologicalSpace G] [TopologicalSpace G']
  {π : UnitaryRepresentation G H} (hπ : π.IsStronglyContinuous)
  (φ : G' →ₜ* G) : (π.restrict φ.toMonoidHom).IsStronglyContinuous

theorem UnitaryRepresentation.IsStronglyContinuous.restrict.{u_1,
    u_2, u_3}
  {G : Type u_1} {H : Type u_2} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] {G' : Type u_3}
  [Group G'] [TopologicalSpace G]
  [TopologicalSpace G']
  {π : UnitaryRepresentation G H}
  (hπ : π.IsStronglyContinuous)
  (φ : G' →ₜ* G) :
  (π.restrict
      φ.toMonoidHom).IsStronglyContinuous

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

theorem UnitaryRepresentation.restrict_isInvariant_iff_of_surjective.{u_1, u_2,
    u_3}
  {G : Type u_1} {H : Type u_2} [Group G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] {G' : Type u_3} [Group G']
  (π : UnitaryRepresentation G H) (φ : G' →* G)
  (hφ : Function.Surjective ⇑φ) (K : ClosedSubmodule ℂ H) :
  (π.restrict φ).IsInvariant K ↔ π.IsInvariant K

theorem UnitaryRepresentation.restrict_isInvariant_iff_of_surjective.{u_1,
    u_2, u_3}
  {G : Type u_1} {H : Type u_2} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] {G' : Type u_3}
  [Group G']
  (π : UnitaryRepresentation G H)
  (φ : G' →* G)
  (hφ : Function.Surjective ⇑φ)
  (K : ClosedSubmodule ℂ H) :
  (π.restrict φ).IsInvariant K ↔
    π.IsInvariant K

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

theorem UnitaryRepresentation.restrict_isTopologicallyIrreducible_iff_of_surjective.{u_1,
    u_2, u_3}
  {G : Type u_1} {H : Type u_2} [Group G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] {G' : Type u_3} [Group G']
  (π : UnitaryRepresentation G H) (φ : G' →* G)
  (hφ : Function.Surjective ⇑φ) :
  (π.restrict φ).IsTopologicallyIrreducible ↔
    π.IsTopologicallyIrreducible

theorem UnitaryRepresentation.restrict_isTopologicallyIrreducible_iff_of_surjective.{u_1,
    u_2, u_3}
  {G : Type u_1} {H : Type u_2} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] {G' : Type u_3}
  [Group G']
  (π : UnitaryRepresentation G H)
  (φ : G' →* G)
  (hφ : Function.Surjective ⇑φ) :
  (π.restrict
        φ).IsTopologicallyIrreducible ↔
    π.IsTopologicallyIrreducible

Restriction along a surjective group homomorphism preserves and reflects topological
irreducibility.

defdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryConjugation.lean

complete

def UnitaryRepresentation.conjugateLinearIsometryEquivMonoidHom.{u_2, u_3}
  {H : Type u_2} {K : Type u_3} [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [NormedAddCommGroup K] [InnerProductSpace ℂ K]
  (e : H ≃ₗᵢ[ℂ] K) : (H ≃ₗᵢ[ℂ] H) →* K ≃ₗᵢ[ℂ] K

def UnitaryRepresentation.conjugateLinearIsometryEquivMonoidHom.{u_2,
    u_3}
  {H : Type u_2} {K : Type u_3}
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [NormedAddCommGroup K]
  [InnerProductSpace ℂ K]
  (e : H ≃ₗᵢ[ℂ] K) :
  (H ≃ₗᵢ[ℂ] H) →* K ≃ₗᵢ[ℂ] K

Implementation after :=

:= e.symm.trans (U.trans e)
  map_one' := by
    apply LinearIsometryEquiv.ext
    intro x
    simp
  map_mul' U V := by
    apply LinearIsometryEquiv.ext
    intro x
    change e ((U * V) (e.symm x)) =
      e (U (e.symm (e (V (e.symm x)))))
    simp

Conjugation of linear isometric automorphisms by a linear isometric equivalence.

defdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryConjugation.lean

complete

def UnitaryRepresentation.conjugate.{u_1, u_2, u_3} {G : Type u_1}
  {H : Type u_2} {K : Type u_3} [Group G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup K]
  [InnerProductSpace ℂ K] [CompleteSpace K]
  (π : UnitaryRepresentation G H) (e : H ≃ₗᵢ[ℂ] K) :
  UnitaryRepresentation G K

def UnitaryRepresentation.conjugate.{u_1, u_2,
    u_3}
  {G : Type u_1} {H : Type u_2}
  {K : Type u_3} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup K]
  [InnerProductSpace ℂ K]
  [CompleteSpace K]
  (π : UnitaryRepresentation G H)
  (e : H ≃ₗᵢ[ℂ] K) :
  UnitaryRepresentation G K

Implementation after :=

:=
  Unitary.linearIsometryEquiv.symm.toMonoidHom.comp
    ((conjugateLinearIsometryEquivMonoidHom e).comp
      (Unitary.linearIsometryEquiv.toMonoidHom.comp π))

Transport a unitary representation across a linear isometric equivalence.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryConjugation.lean

complete

theorem UnitaryRepresentation.linearIsometryEquiv_conjugate_apply.{u_1, u_2,
    u_3}
  {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G]
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
  [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]
  (π : UnitaryRepresentation G H) (e : H ≃ₗᵢ[ℂ] K) (g : G) (x : K) :
  (Unitary.linearIsometryEquiv ((π.conjugate e) g)) x =
    e ((Unitary.linearIsometryEquiv (π g)) (e.symm x))

theorem UnitaryRepresentation.linearIsometryEquiv_conjugate_apply.{u_1,
    u_2, u_3}
  {G : Type u_1} {H : Type u_2}
  {K : Type u_3} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup K]
  [InnerProductSpace ℂ K]
  [CompleteSpace K]
  (π : UnitaryRepresentation G H)
  (e : H ≃ₗᵢ[ℂ] K) (g : G) (x : K) :
  (Unitary.linearIsometryEquiv
        ((π.conjugate e) g))
      x =
    e
      ((Unitary.linearIsometryEquiv (π g))
        (e.symm x))

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryConjugation.lean

complete

theorem UnitaryRepresentation.IsStronglyContinuous.conjugate.{u_1, u_2, u_3}
  {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G]
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
  [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]
  [TopologicalSpace G] {π : UnitaryRepresentation G H}
  (hπ : π.IsStronglyContinuous) (e : H ≃ₗᵢ[ℂ] K) :
  (π.conjugate e).IsStronglyContinuous

theorem UnitaryRepresentation.IsStronglyContinuous.conjugate.{u_1,
    u_2, u_3}
  {G : Type u_1} {H : Type u_2}
  {K : Type u_3} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup K]
  [InnerProductSpace ℂ K]
  [CompleteSpace K] [TopologicalSpace G]
  {π : UnitaryRepresentation G H}
  (hπ : π.IsStronglyContinuous)
  (e : H ≃ₗᵢ[ℂ] K) :
  (π.conjugate e).IsStronglyContinuous

Strong continuity is preserved when a unitary representation is transported across a linear
isometric equivalence.

defdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryConjugation.lean

complete

def UnitaryRepresentation.conjugateIntertwiningMap.{u_1, u_2, u_3}
  {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G]
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
  [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]
  (π : UnitaryRepresentation G H) (e : H ≃ₗᵢ[ℂ] K) :
  ContIntertwiningMap π.toContRepresentation
    (π.conjugate e).toContRepresentation

def UnitaryRepresentation.conjugateIntertwiningMap.{u_1,
    u_2, u_3}
  {G : Type u_1} {H : Type u_2}
  {K : Type u_3} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup K]
  [InnerProductSpace ℂ K]
  [CompleteSpace K]
  (π : UnitaryRepresentation G H)
  (e : H ≃ₗᵢ[ℂ] K) :
  ContIntertwiningMap
    π.toContRepresentation
    (π.conjugate e).toContRepresentation

Implementation after :=

:= e.toContinuousLinearEquiv.toContinuousLinearMap
  isIntertwining' g := by
    ext x
    change e (Unitary.linearIsometryEquiv (π g) x) =
      Unitary.linearIsometryEquiv (π.conjugate e g) (e x)
    rw [linearIsometryEquiv_conjugate_apply, e.symm_apply_apply]

The equivalence used for conjugation is a continuous intertwining map.

defdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryConjugation.lean

complete

def UnitaryRepresentation.conjugateInverseIntertwiningMap.{u_1, u_2, u_3}
  {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G]
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
  [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]
  (π : UnitaryRepresentation G H) (e : H ≃ₗᵢ[ℂ] K) :
  ContIntertwiningMap (π.conjugate e).toContRepresentation
    π.toContRepresentation

def UnitaryRepresentation.conjugateInverseIntertwiningMap.{u_1,
    u_2, u_3}
  {G : Type u_1} {H : Type u_2}
  {K : Type u_3} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup K]
  [InnerProductSpace ℂ K]
  [CompleteSpace K]
  (π : UnitaryRepresentation G H)
  (e : H ≃ₗᵢ[ℂ] K) :
  ContIntertwiningMap
    (π.conjugate e).toContRepresentation
    π.toContRepresentation

Implementation after :=

:= e.symm.toContinuousLinearEquiv.toContinuousLinearMap
  isIntertwining' g := by
    ext x
    change e.symm (Unitary.linearIsometryEquiv (π.conjugate e g) x) =
      Unitary.linearIsometryEquiv (π g) (e.symm x)
    rw [linearIsometryEquiv_conjugate_apply, e.symm_apply_apply]

The inverse equivalence intertwines the conjugated representation back with the original
representation.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryConjugation.lean

complete

theorem UnitaryRepresentation.conjugate_symm.{u_1, u_2, u_3} {G : Type u_1}
  {H : Type u_2} {K : Type u_3} [Group G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup K]
  [InnerProductSpace ℂ K] [CompleteSpace K]
  (π : UnitaryRepresentation G H) (e : H ≃ₗᵢ[ℂ] K) :
  (π.conjugate e).conjugate e.symm = π

theorem UnitaryRepresentation.conjugate_symm.{u_1,
    u_2, u_3}
  {G : Type u_1} {H : Type u_2}
  {K : Type u_3} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup K]
  [InnerProductSpace ℂ K]
  [CompleteSpace K]
  (π : UnitaryRepresentation G H)
  (e : H ≃ₗᵢ[ℂ] K) :
  (π.conjugate e).conjugate e.symm = π

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryConjugation.lean

complete

theorem UnitaryRepresentation.conjugate_isTopologicallyIrreducible.{u_1, u_2,
    u_3}
  {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G]
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
  [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]
  (π : UnitaryRepresentation G H) (e : H ≃ₗᵢ[ℂ] K)
  (hπ : π.IsTopologicallyIrreducible) :
  (π.conjugate e).IsTopologicallyIrreducible

theorem UnitaryRepresentation.conjugate_isTopologicallyIrreducible.{u_1,
    u_2, u_3}
  {G : Type u_1} {H : Type u_2}
  {K : Type u_3} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup K]
  [InnerProductSpace ℂ K]
  [CompleteSpace K]
  (π : UnitaryRepresentation G H)
  (e : H ≃ₗᵢ[ℂ] K)
  (hπ : π.IsTopologicallyIrreducible) :
  (π.conjugate
      e).IsTopologicallyIrreducible

Topological irreducibility is preserved when a unitary representation is transported across
a linear isometric equivalence.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryConjugation.lean

complete

theorem UnitaryRepresentation.conjugate_isTopologicallyIrreducible_iff.{u_1,
    u_2, u_3}
  {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G]
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
  [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]
  (π : UnitaryRepresentation G H) (e : H ≃ₗᵢ[ℂ] K) :
  (π.conjugate e).IsTopologicallyIrreducible ↔
    π.IsTopologicallyIrreducible

theorem UnitaryRepresentation.conjugate_isTopologicallyIrreducible_iff.{u_1,
    u_2, u_3}
  {G : Type u_1} {H : Type u_2}
  {K : Type u_3} [Group G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [NormedAddCommGroup K]
  [InnerProductSpace ℂ K]
  [CompleteSpace K]
  (π : UnitaryRepresentation G H)
  (e : H ≃ₗᵢ[ℂ] K) :
  (π.conjugate
        e).IsTopologicallyIrreducible ↔
    π.IsTopologicallyIrreducible

Conjugate unitary representations are topologically irreducible simultaneously.

Theorem5.6.2

uses 1used by 1✓L∃∀N

Integrated vectors of strongly continuous unitary representations. A compactly supported continuous scalar kernel times a strongly continuous unitary orbit is Bochner integrable for every measure finite on compact sets. The integral remains in each closed invariant subspace containing the input vector, by commuting the orthogonal projection with the integral. For a family of nonnegative kernels concentrating at the identity, Mathlib's peak-function convergence theorem is specialized to prove convergence of the corresponding local orbit integrals back to the input vector. Urysohn bump functions and an antitone countable neighborhood basis then construct nonnegative compactly supported Haar probability kernels whose supports shrink to the identity. Their integrated vectors converge to the input vector, both in real-scalar integral form and via the bundled complex Haar-integrated-vector API. This proves the abstract smoothing and convergence step used in Folland Lemma 6.29 without adding an approximate-identity assumption object.

Lean code for Theorem5.6.2●13 declarations

defdefined in LeanRidgelet/ToMathlib/LieGroup/IntegratedRepresentation.lean

complete

def UnitaryRepresentation.integratedVector.{u_1, u_2} {G : Type u_1}
  {H : Type u_2} [Group G] [TopologicalSpace G] [MeasurableSpace G]
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
  (π : UnitaryRepresentation G H) (μ : MeasureTheory.Measure G)
  (ψ : CompactlySupportedContinuousMap G ℂ) (v : H) : H

def UnitaryRepresentation.integratedVector.{u_1,
    u_2}
  {G : Type u_1} {H : Type u_2} [Group G]
  [TopologicalSpace G] [MeasurableSpace G]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H]
  (π : UnitaryRepresentation G H)
  (μ : MeasureTheory.Measure G)
  (ψ :
    CompactlySupportedContinuousMap G ℂ)
  (v : H) : H

Implementation after :=

:=
  ∫ g, ψ g • (π g : H →L[ℂ] H) v ∂μ

The vector obtained by integrating a compactly supported continuous scalar kernel against a
unitary orbit.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/IntegratedRepresentation.lean

complete

theorem UnitaryRepresentation.integratedVector_integrable.{u_1, u_2}
  {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G]
  [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H]
  {π : UnitaryRepresentation G H} (hπ : π.IsStronglyContinuous)
  (μ : MeasureTheory.Measure G)
  [MeasureTheory.IsFiniteMeasureOnCompacts μ]
  (ψ : CompactlySupportedContinuousMap G ℂ) (v : H) :
  MeasureTheory.Integrable (fun g ↦ ψ g • ↑(π g) v) μ

theorem UnitaryRepresentation.integratedVector_integrable.{u_1,
    u_2}
  {G : Type u_1} {H : Type u_2} [Group G]
  [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H]
  {π : UnitaryRepresentation G H}
  (hπ : π.IsStronglyContinuous)
  (μ : MeasureTheory.Measure G)
  [MeasureTheory.IsFiniteMeasureOnCompacts
      μ]
  (ψ :
    CompactlySupportedContinuousMap G ℂ)
  (v : H) :
  MeasureTheory.Integrable
    (fun g ↦ ψ g • ↑(π g) v) μ

Strong continuity and compact support make the orbit-kernel integrand Bochner integrable.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/IntegratedRepresentation.lean

complete

theorem UnitaryRepresentation.integratedVector_mem.{u_1, u_2} {G : Type u_1}
  {H : Type u_2} [Group G] [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [NormedAddCommGroup H] [InnerProductSpace ℂ H]
  [CompleteSpace H] {π : UnitaryRepresentation G H}
  (hπ : π.IsStronglyContinuous) (μ : MeasureTheory.Measure G)
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] (K : ClosedSubmodule ℂ H)
  (hK : π.IsInvariant K) (ψ : CompactlySupportedContinuousMap G ℂ)
  {v : H} (hv : v ∈ K) : π.integratedVector μ ψ v ∈ K

theorem UnitaryRepresentation.integratedVector_mem.{u_1,
    u_2}
  {G : Type u_1} {H : Type u_2} [Group G]
  [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H]
  {π : UnitaryRepresentation G H}
  (hπ : π.IsStronglyContinuous)
  (μ : MeasureTheory.Measure G)
  [MeasureTheory.IsFiniteMeasureOnCompacts
      μ]
  (K : ClosedSubmodule ℂ H)
  (hK : π.IsInvariant K)
  (ψ :
    CompactlySupportedContinuousMap G ℂ)
  {v : H} (hv : v ∈ K) :
  π.integratedVector μ ψ v ∈ K

Integrating a unitary orbit does not leave a closed invariant subspace.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/IntegratedRepresentation.lean

complete

theorem UnitaryRepresentation.tendsto_setIntegral_peak_smul_orbit.{u_1, u_2,
    u_3}
  {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G]
  [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [T2Space G] {ι : Type u_3}
  {l : Filter ι} {μ : MeasureTheory.Measure G}
  [MeasureTheory.IsFiniteMeasureOnCompacts μ]
  {π : UnitaryRepresentation G H} (hπ : π.IsStronglyContinuous) (v : H)
  {s t : Set G} (hs : IsCompact s) (ht : MeasurableSet t) (hts : t ⊆ s)
  (h'ts : t ∈ nhdsWithin 1 s) (h't : μ t ≠ ⊤) {φ : ι → G → ℝ}
  (hnφ : ∀ᶠ (i : ι) in l, ∀ g ∈ s, 0 ≤ φ i g)
  (hlφ :
    ∀ (u : Set G), IsOpen u → 1 ∈ u → TendstoUniformlyOn φ 0 l (s \ u))
  (hiφ : Filter.Tendsto (fun i ↦ ∫ (g : G) in t, φ i g ∂μ) l (nhds 1))
  (h'iφ :
    ∀ᶠ (i : ι) in l,
      MeasureTheory.AEStronglyMeasurable (φ i) (μ.restrict s)) :
  Filter.Tendsto (fun i ↦ ∫ (g : G) in s, φ i g • ↑(π g) v ∂μ) l
    (nhds v)

theorem UnitaryRepresentation.tendsto_setIntegral_peak_smul_orbit.{u_1,
    u_2, u_3}
  {G : Type u_1} {H : Type u_2} [Group G]
  [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [T2Space G]
  {ι : Type u_3} {l : Filter ι}
  {μ : MeasureTheory.Measure G}
  [MeasureTheory.IsFiniteMeasureOnCompacts
      μ]
  {π : UnitaryRepresentation G H}
  (hπ : π.IsStronglyContinuous) (v : H)
  {s t : Set G} (hs : IsCompact s)
  (ht : MeasurableSet t) (hts : t ⊆ s)
  (h'ts : t ∈ nhdsWithin 1 s)
  (h't : μ t ≠ ⊤) {φ : ι → G → ℝ}
  (hnφ :
    ∀ᶠ (i : ι) in l, ∀ g ∈ s, 0 ≤ φ i g)
  (hlφ :
    ∀ (u : Set G),
      IsOpen u →
        1 ∈ u →
          TendstoUniformlyOn φ 0 l
            (s \ u))
  (hiφ :
    Filter.Tendsto
      (fun i ↦ ∫ (g : G) in t, φ i g ∂μ) l
      (nhds 1))
  (h'iφ :
    ∀ᶠ (i : ι) in l,
      MeasureTheory.AEStronglyMeasurable
        (φ i) (μ.restrict s)) :
  Filter.Tendsto
    (fun i ↦
      ∫ (g : G) in s, φ i g • ↑(π g) v ∂μ)
    l (nhds v)

Mathlib's peak-function convergence theorem applied to a strongly continuous unitary orbit.
This is the convergence mechanism for approximate-identity smoothing in Folland Lemma 6.29.

defdefined in LeanRidgelet/ToMathlib/LieGroup/IntegratedRepresentation.lean

complete

def UnitaryRepresentation.haarIntegratedVector.{u_1, u_2} {G : Type u_1}
  {H : Type u_2} [Group G] [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [NormedAddCommGroup H] [InnerProductSpace ℂ H]
  [CompleteSpace H] [IsTopologicalGroup G] [LocallyCompactSpace G]
  (π : UnitaryRepresentation G H)
  (ψ : CompactlySupportedContinuousMap G ℂ) (v : H) : H

def UnitaryRepresentation.haarIntegratedVector.{u_1,
    u_2}
  {G : Type u_1} {H : Type u_2} [Group G]
  [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [IsTopologicalGroup G]
  [LocallyCompactSpace G]
  (π : UnitaryRepresentation G H)
  (ψ :
    CompactlySupportedContinuousMap G ℂ)
  (v : H) : H

Implementation after :=

:=
  π.integratedVector Measure.haar ψ v

Integrated vector for Mathlib's chosen left Haar measure.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/IntegratedRepresentation.lean

complete

theorem UnitaryRepresentation.haarIntegratedVector_integrable.{u_1, u_2}
  {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G]
  [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] [IsTopologicalGroup G]
  [LocallyCompactSpace G] {π : UnitaryRepresentation G H}
  (hπ : π.IsStronglyContinuous)
  (ψ : CompactlySupportedContinuousMap G ℂ) (v : H) :
  MeasureTheory.Integrable (fun g ↦ ψ g • ↑(π g) v)
    MeasureTheory.Measure.haar

theorem UnitaryRepresentation.haarIntegratedVector_integrable.{u_1,
    u_2}
  {G : Type u_1} {H : Type u_2} [Group G]
  [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [IsTopologicalGroup G]
  [LocallyCompactSpace G]
  {π : UnitaryRepresentation G H}
  (hπ : π.IsStronglyContinuous)
  (ψ :
    CompactlySupportedContinuousMap G ℂ)
  (v : H) :
  MeasureTheory.Integrable
    (fun g ↦ ψ g • ↑(π g) v)
    MeasureTheory.Measure.haar

A compactly supported kernel times a strongly continuous unitary orbit is Haar integrable.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/IntegratedRepresentation.lean

complete

theorem UnitaryRepresentation.haarIntegratedVector_mem.{u_1, u_2} {G : Type u_1}
  {H : Type u_2} [Group G] [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [NormedAddCommGroup H] [InnerProductSpace ℂ H]
  [CompleteSpace H] [IsTopologicalGroup G] [LocallyCompactSpace G]
  {π : UnitaryRepresentation G H} (hπ : π.IsStronglyContinuous)
  (K : ClosedSubmodule ℂ H) (hK : π.IsInvariant K)
  (ψ : CompactlySupportedContinuousMap G ℂ) {v : H} (hv : v ∈ K) :
  π.haarIntegratedVector ψ v ∈ K

theorem UnitaryRepresentation.haarIntegratedVector_mem.{u_1,
    u_2}
  {G : Type u_1} {H : Type u_2} [Group G]
  [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] [IsTopologicalGroup G]
  [LocallyCompactSpace G]
  {π : UnitaryRepresentation G H}
  (hπ : π.IsStronglyContinuous)
  (K : ClosedSubmodule ℂ H)
  (hK : π.IsInvariant K)
  (ψ :
    CompactlySupportedContinuousMap G ℂ)
  {v : H} (hv : v ∈ K) :
  π.haarIntegratedVector ψ v ∈ K

Haar-integrated vectors remain in every closed invariant subspace containing the input.

defdefined in LeanRidgelet/ToMathlib/LieGroup/HaarApproximateIdentity.lean

complete

def UnitaryRepresentation.complexKernel.{u_1} {G : Type u_1}
  [TopologicalSpace G] (f : CompactlySupportedContinuousMap G ℝ) :
  CompactlySupportedContinuousMap G ℂ

def UnitaryRepresentation.complexKernel.{u_1}
  {G : Type u_1} [TopologicalSpace G]
  (f :
    CompactlySupportedContinuousMap G ℝ) :
  CompactlySupportedContinuousMap G ℂ

Implementation after :=

:= f g
  continuous_toFun := Complex.continuous_ofReal.comp f.continuous
  hasCompactSupport' := by
    change HasCompactSupport (Complex.ofReal ∘ (f : G → ℝ))
    exact f.hasCompactSupport.comp_left Complex.ofReal_zero

Regard a real compactly supported kernel as a complex one.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/HaarApproximateIdentity.lean

complete

theorem UnitaryRepresentation.complexKernel_apply.{u_1} {G : Type u_1}
  [TopologicalSpace G] (f : CompactlySupportedContinuousMap G ℝ)
  (g : G) : (UnitaryRepresentation.complexKernel f) g = ↑(f g)

theorem UnitaryRepresentation.complexKernel_apply.{u_1}
  {G : Type u_1} [TopologicalSpace G]
  (f :
    CompactlySupportedContinuousMap G ℝ)
  (g : G) :
  (UnitaryRepresentation.complexKernel f)
      g =
    ↑(f g)

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/HaarApproximateIdentity.lean

complete

theorem UnitaryRepresentation.exists_haarProbabilityBump.{u_1} {G : Type u_1}
  [Group G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G]
  [IsTopologicalGroup G] [LocallyCompactSpace G] {U : Set G}
  (hU : IsOpen U) (h1U : 1 ∈ U) :
  ∃ ψ,
    (∀ (g : G), 0 ≤ ψ g) ∧
      tsupport ⇑ψ ⊆ U ∧ ∫ (g : G), ψ g ∂MeasureTheory.Measure.haar = 1

theorem UnitaryRepresentation.exists_haarProbabilityBump.{u_1}
  {G : Type u_1} [Group G]
  [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [IsTopologicalGroup G]
  [LocallyCompactSpace G] {U : Set G}
  (hU : IsOpen U) (h1U : 1 ∈ U) :
  ∃ ψ,
    (∀ (g : G), 0 ≤ ψ g) ∧
      tsupport ⇑ψ ⊆ U ∧
        ∫ (g : G),
            ψ
              g ∂MeasureTheory.Measure.haar =
          1

Every neighborhood of the identity contains the support of a nonnegative continuous Haar
probability density.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/HaarApproximateIdentity.lean

complete

theorem UnitaryRepresentation.exists_haarApproximateIdentity.{u_1}
  {G : Type u_1} [Group G] [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G]
  [FirstCountableTopology G] :
  ∃ ψ,
    (∀ (n : ℕ) (g : G), 0 ≤ (ψ n) g) ∧
      (∀ (n : ℕ), ∫ (g : G), (ψ n) g ∂MeasureTheory.Measure.haar = 1) ∧
        (∀ U ∈ nhds 1,
            ∀ᶠ (n : ℕ) in Filter.atTop, tsupport ⇑(ψ n) ⊆ U) ∧
          ∃ s, IsCompact s ∧ ∀ (n : ℕ), tsupport ⇑(ψ n) ⊆ s

theorem UnitaryRepresentation.exists_haarApproximateIdentity.{u_1}
  {G : Type u_1} [Group G]
  [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [IsTopologicalGroup G]
  [LocallyCompactSpace G]
  [FirstCountableTopology G] :
  ∃ ψ,
    (∀ (n : ℕ) (g : G), 0 ≤ (ψ n) g) ∧
      (∀ (n : ℕ),
          ∫ (g : G),
              (ψ n)
                g ∂MeasureTheory.Measure.haar =
            1) ∧
        (∀ U ∈ nhds 1,
            ∀ᶠ (n : ℕ) in Filter.atTop,
              tsupport ⇑(ψ n) ⊆ U) ∧
          ∃ s,
            IsCompact s ∧
              ∀ (n : ℕ),
                tsupport ⇑(ψ n) ⊆ s

A first-countable locally compact group admits a sequence of compactly supported continuous
nonnegative Haar probability densities whose supports eventually lie in every neighborhood of the
identity.  The supports can moreover be chosen inside one fixed compact set.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/HaarApproximateIdentity.lean

complete

theorem UnitaryRepresentation.exists_haarApproximateIdentity_tendsto_smul_orbit.{u_1,
    u_2}
  {G : Type u_1} [Group G] [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G]
  {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
  [CompleteSpace H] [FirstCountableTopology G] [T2Space G]
  {π : UnitaryRepresentation G H} (hπ : π.IsStronglyContinuous)
  (v : H) :
  ∃ ψ,
    (∀ (n : ℕ) (g : G), 0 ≤ (ψ n) g) ∧
      (∀ (n : ℕ), ∫ (g : G), (ψ n) g ∂MeasureTheory.Measure.haar = 1) ∧
        (∀ U ∈ nhds 1,
            ∀ᶠ (n : ℕ) in Filter.atTop, tsupport ⇑(ψ n) ⊆ U) ∧
          Filter.Tendsto
            (fun n ↦
              ∫ (g : G), (ψ n) g • ↑(π g) v ∂MeasureTheory.Measure.haar)
            Filter.atTop (nhds v)

theorem UnitaryRepresentation.exists_haarApproximateIdentity_tendsto_smul_orbit.{u_1,
    u_2}
  {G : Type u_1} [Group G]
  [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [IsTopologicalGroup G]
  [LocallyCompactSpace G] {H : Type u_2}
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H]
  [FirstCountableTopology G] [T2Space G]
  {π : UnitaryRepresentation G H}
  (hπ : π.IsStronglyContinuous) (v : H) :
  ∃ ψ,
    (∀ (n : ℕ) (g : G), 0 ≤ (ψ n) g) ∧
      (∀ (n : ℕ),
          ∫ (g : G),
              (ψ n)
                g ∂MeasureTheory.Measure.haar =
            1) ∧
        (∀ U ∈ nhds 1,
            ∀ᶠ (n : ℕ) in Filter.atTop,
              tsupport ⇑(ψ n) ⊆ U) ∧
          Filter.Tendsto
            (fun n ↦
              ∫ (g : G),
                (ψ n) g •
                  ↑(π g)
                    v ∂MeasureTheory.Measure.haar)
            Filter.atTop (nhds v)

A compactly supported sequential Haar approximate identity can be chosen so that its
integrated unitary orbit converges to the original vector.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/HaarApproximateIdentity.lean

complete

theorem UnitaryRepresentation.exists_haarApproximateIdentity_tendsto_integratedVector.{u_1,
    u_2}
  {G : Type u_1} [Group G] [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G]
  {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
  [CompleteSpace H] [FirstCountableTopology G] [T2Space G]
  {π : UnitaryRepresentation G H} (hπ : π.IsStronglyContinuous)
  (v : H) :
  ∃ ψ,
    (∀ (n : ℕ) (g : G), 0 ≤ (ψ n) g) ∧
      (∀ (n : ℕ), ∫ (g : G), (ψ n) g ∂MeasureTheory.Measure.haar = 1) ∧
        (∀ U ∈ nhds 1,
            ∀ᶠ (n : ℕ) in Filter.atTop, tsupport ⇑(ψ n) ⊆ U) ∧
          Filter.Tendsto
            (fun n ↦
              π.haarIntegratedVector
                (UnitaryRepresentation.complexKernel (ψ n)) v)
            Filter.atTop (nhds v)

theorem UnitaryRepresentation.exists_haarApproximateIdentity_tendsto_integratedVector.{u_1,
    u_2}
  {G : Type u_1} [Group G]
  [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [IsTopologicalGroup G]
  [LocallyCompactSpace G] {H : Type u_2}
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H]
  [FirstCountableTopology G] [T2Space G]
  {π : UnitaryRepresentation G H}
  (hπ : π.IsStronglyContinuous) (v : H) :
  ∃ ψ,
    (∀ (n : ℕ) (g : G), 0 ≤ (ψ n) g) ∧
      (∀ (n : ℕ),
          ∫ (g : G),
              (ψ n)
                g ∂MeasureTheory.Measure.haar =
            1) ∧
        (∀ U ∈ nhds 1,
            ∀ᶠ (n : ℕ) in Filter.atTop,
              tsupport ⇑(ψ n) ⊆ U) ∧
          Filter.Tendsto
            (fun n ↦
              π.haarIntegratedVector
                (UnitaryRepresentation.complexKernel
                  (ψ n))
                v)
            Filter.atTop (nhds v)

The preceding convergence written using the bundled complex Haar-integrated vector.

Theorem5.6.3

uses 0

Used by 2

Reverse dependency previews

Preview

Theorem 4.1.6

Loading preview

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

✓L∃∀N

Continuity of compact-kernel group convolution. On a noncommutative topological group, the function x\mapsto\int L(f(y^{-1}),g(xy))\,d\mu(y) is continuous when f\circ\mathrm{inv} is locally integrable and g is continuous with compact support. The proof transports the formula to Mathlib's additive convolution on the opposite group Additive Gᵐᵒᵖ; therefore it works for an arbitrary measure and needs no Haar-invariance assumption. This supplies the continuity step in Folland Lemma 6.29 independently of the quotient-model representative problem.

Lean code for Theorem5.6.3●1 theorem

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/GroupConvolution.lean

complete

theorem MeasureTheory.continuous_integral_compact_mul_right.{u_1, u_2, u_3, u_4,
    u_5}
  {G : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4}
  {𝕜 : Type u_5} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup E]
  [NormedAddCommGroup E'] [NormedAddCommGroup F]
  [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E']
  [NormedSpace 𝕜 F] [NormedSpace ℝ F] {f : G → E} {g : G → E'}
  (L : E →L[𝕜] E' →L[𝕜] F) {μ : MeasureTheory.Measure G}
  (hf : MeasureTheory.LocallyIntegrable (fun y ↦ f y⁻¹) μ)
  (hg : Continuous g) (hcg : HasCompactSupport g) :
  Continuous fun x ↦ ∫ (y : G), (L (f y⁻¹)) (g (x * y)) ∂μ

theorem MeasureTheory.continuous_integral_compact_mul_right.{u_1,
    u_2, u_3, u_4, u_5}
  {G : Type u_1} {E : Type u_2}
  {E' : Type u_3} {F : Type u_4}
  {𝕜 : Type u_5} [Group G]
  [TopologicalSpace G]
  [IsTopologicalGroup G]
  [MeasurableSpace G] [BorelSpace G]
  [NormedAddCommGroup E]
  [NormedAddCommGroup E']
  [NormedAddCommGroup F]
  [NontriviallyNormedField 𝕜]
  [NormedSpace 𝕜 E] [NormedSpace 𝕜 E']
  [NormedSpace 𝕜 F] [NormedSpace ℝ F]
  {f : G → E} {g : G → E'}
  (L : E →L[𝕜] E' →L[𝕜] F)
  {μ : MeasureTheory.Measure G}
  (hf :
    MeasureTheory.LocallyIntegrable
      (fun y ↦ f y⁻¹) μ)
  (hg : Continuous g)
  (hcg : HasCompactSupport g) :
  Continuous fun x ↦
    ∫ (y : G), (L (f y⁻¹)) (g (x * y)) ∂μ

A noncommutative group convolution is continuous when its first factor, after inversion, is
locally integrable and its second factor is continuous with compact support.

The formula is deliberately stated for an arbitrary measure. It is Mathlib's additive convolution
after transporting the group to `Additive Gᵐᵒᵖ`, so no Haar-invariance hypothesis is needed.

Theorem5.6.4

Statement uses 2

Statement dependency previews

Preview

Theorem 5.1.10

Loading preview

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

used by 1✓L∃∀N

Pointwise unitaries on Bochner L^2 and product groups. A value-space linear isometric equivalence acts pointwise on an Lp class through Mathlib's ContinuousLinearMap.compLp. Its norm preservation, inverse, composition law, and a.e. representative are proved before it is bundled as a unitary representation on Bochner L^2. Two unitary representations on the same Hilbert space whose images commute then combine, via Mathlib's noncommutative coproduct of monoid homomorphisms, into a representation of the product group. No Hilbert tensor product is needed for these constructions. For a finite-dimensional value representation, the commuting product is also proved irreducible when the scalar action is irreducible and is natural under coordinate embeddings and projections. The proof applies infinite-dimensional Schur twice: first to the matrix coefficients of an invariant projection, then to its reconstructed value-space operator.

Lean code for Theorem5.6.4●12 declarations

defdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryLp.lean

complete

def UnitaryRepresentation.lpPointwiseLinearIsometry.{u_4, u_5}
  {X : Type u_4} {E : Type u_5} [MeasurableSpace X]
  [NormedAddCommGroup E] [InnerProductSpace ℂ E] {p : ENNReal}
  {μ : MeasureTheory.Measure X} [Fact (1 ≤ p)] (U : E ≃ₗᵢ[ℂ] E) :
  ↥(MeasureTheory.Lp E p μ) →ₗᵢ[ℂ] ↥(MeasureTheory.Lp E p μ)

def UnitaryRepresentation.lpPointwiseLinearIsometry.{u_4,
    u_5}
  {X : Type u_4} {E : Type u_5}
  [MeasurableSpace X]
  [NormedAddCommGroup E]
  [InnerProductSpace ℂ E] {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  [Fact (1 ≤ p)] (U : E ≃ₗᵢ[ℂ] E) :
  ↥(MeasureTheory.Lp E p μ) →ₗᵢ[ℂ]
    ↥(MeasureTheory.Lp E p μ)

Implementation after :=

:= U.toLinearIsometry.toContinuousLinearMap.compLp f
  map_add' f g := by
    apply Lp.ext
    filter_upwards [U.toLinearIsometry.toContinuousLinearMap.coeFn_compLp (f + g),
      U.toLinearIsometry.toContinuousLinearMap.coeFn_compLp f,
      U.toLinearIsometry.toContinuousLinearMap.coeFn_compLp g,
      Lp.coeFn_add f g,
      Lp.coeFn_add
        (U.toLinearIsometry.toContinuousLinearMap.compLp f)
        (U.toLinearIsometry.toContinuousLinearMap.compLp g)] with x hfg hf hg hadd hout
    rw [hfg, hadd, Pi.add_apply, map_add, hout, Pi.add_apply, hf, hg]
  map_smul' c f := by
    apply Lp.ext
    filter_upwards [U.toLinearIsometry.toContinuousLinearMap.coeFn_compLp (c • f),
      U.toLinearIsometry.toContinuousLinearMap.coeFn_compLp f,
      Lp.coeFn_smul c f,
      Lp.coeFn_smul c (U.toLinearIsometry.toContinuousLinearMap.compLp f)] with x hcf hf hin hout
    rw [hcf, hin, Pi.smul_apply, map_smul]
    change c • U.toLinearIsometry.toContinuousLinearMap (f x) =
      ((c • U.toLinearIsometry.toContinuousLinearMap.compLp f : Lp E p μ) : X → E) x
    rw [hout, Pi.smul_apply, hf]
  norm_map' f := by
    change ‖U.toLinearIsometry.toContinuousLinearMap.compLp f‖ = ‖f‖
    rw [Lp.norm_def, Lp.norm_def]
    apply congrArg ENNReal.toReal
    apply eLpNorm_congr_norm_ae
    filter_upwards [U.toLinearIsometry.toContinuousLinearMap.coeFn_compLp f] with x hx
    rw [hx]
    exact U.norm_map (f x)

Pointwise application of a value-space linear isometric equivalence to a Bochner `Lp`
class.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryLp.lean

complete

theorem UnitaryRepresentation.lpPointwiseLinearIsometry_apply_ae.{u_4, u_5}
  {X : Type u_4} {E : Type u_5} [MeasurableSpace X]
  [NormedAddCommGroup E] [InnerProductSpace ℂ E] {p : ENNReal}
  {μ : MeasureTheory.Measure X} [Fact (1 ≤ p)] (U : E ≃ₗᵢ[ℂ] E)
  (f : ↥(MeasureTheory.Lp E p μ)) :
  ↑↑((UnitaryRepresentation.lpPointwiseLinearIsometry U) f) =ᵐ[μ]
    fun x ↦ U (↑↑f x)

theorem UnitaryRepresentation.lpPointwiseLinearIsometry_apply_ae.{u_4,
    u_5}
  {X : Type u_4} {E : Type u_5}
  [MeasurableSpace X]
  [NormedAddCommGroup E]
  [InnerProductSpace ℂ E] {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  [Fact (1 ≤ p)] (U : E ≃ₗᵢ[ℂ] E)
  (f : ↥(MeasureTheory.Lp E p μ)) :
  ↑↑((UnitaryRepresentation.lpPointwiseLinearIsometry
            U)
          f) =ᵐ[μ]
    fun x ↦ U (↑↑f x)

The pointwise `Lp` isometry has the expected a.e. representative.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryLp.lean

complete

theorem UnitaryRepresentation.lpPointwiseLinearIsometry_surjective.{u_4, u_5}
  {X : Type u_4} {E : Type u_5} [MeasurableSpace X]
  [NormedAddCommGroup E] [InnerProductSpace ℂ E] {p : ENNReal}
  {μ : MeasureTheory.Measure X} [Fact (1 ≤ p)] (U : E ≃ₗᵢ[ℂ] E) :
  Function.Surjective
    ⇑(UnitaryRepresentation.lpPointwiseLinearIsometry U)

theorem UnitaryRepresentation.lpPointwiseLinearIsometry_surjective.{u_4,
    u_5}
  {X : Type u_4} {E : Type u_5}
  [MeasurableSpace X]
  [NormedAddCommGroup E]
  [InnerProductSpace ℂ E] {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  [Fact (1 ≤ p)] (U : E ≃ₗᵢ[ℂ] E) :
  Function.Surjective
    ⇑(UnitaryRepresentation.lpPointwiseLinearIsometry
        U)

Pointwise application is onto; applying `U.symm` supplies an explicit preimage.

defdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryLp.lean

complete

def UnitaryRepresentation.lpPointwiseLinearIsometryEquiv.{u_4, u_5}
  {X : Type u_4} {E : Type u_5} [MeasurableSpace X]
  [NormedAddCommGroup E] [InnerProductSpace ℂ E] {p : ENNReal}
  {μ : MeasureTheory.Measure X} [Fact (1 ≤ p)] (U : E ≃ₗᵢ[ℂ] E) :
  ↥(MeasureTheory.Lp E p μ) ≃ₗᵢ[ℂ] ↥(MeasureTheory.Lp E p μ)

def UnitaryRepresentation.lpPointwiseLinearIsometryEquiv.{u_4,
    u_5}
  {X : Type u_4} {E : Type u_5}
  [MeasurableSpace X]
  [NormedAddCommGroup E]
  [InnerProductSpace ℂ E] {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  [Fact (1 ≤ p)] (U : E ≃ₗᵢ[ℂ] E) :
  ↥(MeasureTheory.Lp E p μ) ≃ₗᵢ[ℂ]
    ↥(MeasureTheory.Lp E p μ)

Implementation after :=

:=
  LinearIsometryEquiv.ofSurjective (lpPointwiseLinearIsometry U)
    (lpPointwiseLinearIsometry_surjective U)

Pointwise application of a value-space unitary, as an equivalence of Bochner `Lp`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryLp.lean

complete

theorem UnitaryRepresentation.lpPointwiseLinearIsometryEquiv_apply_ae.{u_4, u_5}
  {X : Type u_4} {E : Type u_5} [MeasurableSpace X]
  [NormedAddCommGroup E] [InnerProductSpace ℂ E] {p : ENNReal}
  {μ : MeasureTheory.Measure X} [Fact (1 ≤ p)] (U : E ≃ₗᵢ[ℂ] E)
  (f : ↥(MeasureTheory.Lp E p μ)) :
  ↑↑((UnitaryRepresentation.lpPointwiseLinearIsometryEquiv U) f) =ᵐ[μ]
    fun x ↦ U (↑↑f x)

theorem UnitaryRepresentation.lpPointwiseLinearIsometryEquiv_apply_ae.{u_4,
    u_5}
  {X : Type u_4} {E : Type u_5}
  [MeasurableSpace X]
  [NormedAddCommGroup E]
  [InnerProductSpace ℂ E] {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  [Fact (1 ≤ p)] (U : E ≃ₗᵢ[ℂ] E)
  (f : ↥(MeasureTheory.Lp E p μ)) :
  ↑↑((UnitaryRepresentation.lpPointwiseLinearIsometryEquiv
            U)
          f) =ᵐ[μ]
    fun x ↦ U (↑↑f x)

The bundled pointwise equivalence has the expected a.e. representative.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryLp.lean

complete

theorem UnitaryRepresentation.lpPointwiseLinearIsometryEquiv_mul_apply.{u_4,
    u_5}
  {X : Type u_4} {E : Type u_5} [MeasurableSpace X]
  [NormedAddCommGroup E] [InnerProductSpace ℂ E] {p : ENNReal}
  {μ : MeasureTheory.Measure X} [Fact (1 ≤ p)] (U V : E ≃ₗᵢ[ℂ] E)
  (f : ↥(MeasureTheory.Lp E p μ)) :
  (UnitaryRepresentation.lpPointwiseLinearIsometryEquiv (U * V)) f =
    (UnitaryRepresentation.lpPointwiseLinearIsometryEquiv U)
      ((UnitaryRepresentation.lpPointwiseLinearIsometryEquiv V) f)

theorem UnitaryRepresentation.lpPointwiseLinearIsometryEquiv_mul_apply.{u_4,
    u_5}
  {X : Type u_4} {E : Type u_5}
  [MeasurableSpace X]
  [NormedAddCommGroup E]
  [InnerProductSpace ℂ E] {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  [Fact (1 ≤ p)] (U V : E ≃ₗᵢ[ℂ] E)
  (f : ↥(MeasureTheory.Lp E p μ)) :
  (UnitaryRepresentation.lpPointwiseLinearIsometryEquiv
        (U * V))
      f =
    (UnitaryRepresentation.lpPointwiseLinearIsometryEquiv
        U)
      ((UnitaryRepresentation.lpPointwiseLinearIsometryEquiv
          V)
        f)

Pointwise application respects composition of value-space unitaries.

defdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryLp.lean

complete

def UnitaryRepresentation.lpPointwiseLinearIsometryEquivMonoidHom.{u_4, u_5}
  {X : Type u_4} {E : Type u_5} [MeasurableSpace X]
  [NormedAddCommGroup E] [InnerProductSpace ℂ E] {p : ENNReal}
  {μ : MeasureTheory.Measure X} [Fact (1 ≤ p)] :
  (E ≃ₗᵢ[ℂ] E) →*
    ↥(MeasureTheory.Lp E p μ) ≃ₗᵢ[ℂ] ↥(MeasureTheory.Lp E p μ)

def UnitaryRepresentation.lpPointwiseLinearIsometryEquivMonoidHom.{u_4,
    u_5}
  {X : Type u_4} {E : Type u_5}
  [MeasurableSpace X]
  [NormedAddCommGroup E]
  [InnerProductSpace ℂ E] {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  [Fact (1 ≤ p)] :
  (E ≃ₗᵢ[ℂ] E) →*
    ↥(MeasureTheory.Lp E p μ) ≃ₗᵢ[ℂ]
      ↥(MeasureTheory.Lp E p μ)

Implementation after :=

:= lpPointwiseLinearIsometryEquiv
  map_one' := by
    apply LinearIsometryEquiv.ext
    intro f
    change lpPointwiseLinearIsometryEquiv (LinearIsometryEquiv.refl ℂ E) f = f
    apply Lp.ext
    filter_upwards [lpPointwiseLinearIsometryEquiv_apply_ae
      (LinearIsometryEquiv.refl ℂ E) f] with x hx
    simpa using hx
  map_mul' U V := by
    apply LinearIsometryEquiv.ext
    exact lpPointwiseLinearIsometryEquiv_mul_apply U V

Pointwise application is a homomorphism on the group of value-space unitaries.

defdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryLp.lean

complete

def UnitaryRepresentation.lpPointwise.{u_1, u_4, u_5} {G : Type u_1}
  {X : Type u_4} {E : Type u_5} [Group G] [MeasurableSpace X]
  [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]
  {μ : MeasureTheory.Measure X} (π : UnitaryRepresentation G E) :
  UnitaryRepresentation G ↥(MeasureTheory.Lp E 2 μ)

def UnitaryRepresentation.lpPointwise.{u_1,
    u_4, u_5}
  {G : Type u_1} {X : Type u_4}
  {E : Type u_5} [Group G]
  [MeasurableSpace X]
  [NormedAddCommGroup E]
  [InnerProductSpace ℂ E]
  [CompleteSpace E]
  {μ : MeasureTheory.Measure X}
  (π : UnitaryRepresentation G E) :
  UnitaryRepresentation G
    ↥(MeasureTheory.Lp E 2 μ)

Implementation after :=

:=
  Unitary.linearIsometryEquiv.symm.toMonoidHom.comp
    ((lpPointwiseLinearIsometryEquivMonoidHom (p := 2) (μ := μ)).comp
      (Unitary.linearIsometryEquiv.toMonoidHom.comp π))

Lift a unitary representation on the value space to its pointwise representation on
Bochner `L²`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryLp.lean

complete

theorem UnitaryRepresentation.lpPointwise_apply_ae.{u_1, u_4, u_5}
  {G : Type u_1} {X : Type u_4} {E : Type u_5} [Group G]
  [MeasurableSpace X] [NormedAddCommGroup E] [InnerProductSpace ℂ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure X}
  (π : UnitaryRepresentation G E) (g : G)
  (f : ↥(MeasureTheory.Lp E 2 μ)) :
  ↑↑(↑(π.lpPointwise g) f) =ᵐ[μ] fun x ↦ ↑(π g) (↑↑f x)

theorem UnitaryRepresentation.lpPointwise_apply_ae.{u_1,
    u_4, u_5}
  {G : Type u_1} {X : Type u_4}
  {E : Type u_5} [Group G]
  [MeasurableSpace X]
  [NormedAddCommGroup E]
  [InnerProductSpace ℂ E]
  [CompleteSpace E]
  {μ : MeasureTheory.Measure X}
  (π : UnitaryRepresentation G E) (g : G)
  (f : ↥(MeasureTheory.Lp E 2 μ)) :
  ↑↑(↑(π.lpPointwise g) f) =ᵐ[μ] fun x ↦
    ↑(π g) (↑↑f x)

The lifted representation applies the value-space unitary pointwise, a.e.

defdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryLp.lean

complete

def UnitaryRepresentation.prodOfCommute.{u_2, u_3, u_6} {G₁ : Type u_2}
  {G₂ : Type u_3} {H : Type u_6} [Group G₁] [Group G₂]
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
  (π₁ : UnitaryRepresentation G₁ H) (π₂ : UnitaryRepresentation G₂ H)
  (hcomm : ∀ (g₁ : G₁) (g₂ : G₂), Commute (π₁ g₁) (π₂ g₂)) :
  UnitaryRepresentation (G₁ × G₂) H

def UnitaryRepresentation.prodOfCommute.{u_2,
    u_3, u_6}
  {G₁ : Type u_2} {G₂ : Type u_3}
  {H : Type u_6} [Group G₁] [Group G₂]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H]
  (π₁ : UnitaryRepresentation G₁ H)
  (π₂ : UnitaryRepresentation G₂ H)
  (hcomm :
    ∀ (g₁ : G₁) (g₂ : G₂),
      Commute (π₁ g₁) (π₂ g₂)) :
  UnitaryRepresentation (G₁ × G₂) H

Implementation after :=

:=
  π₁.noncommCoprod π₂ hcomm

Two commuting unitary representations on one Hilbert space combine to a unitary
representation of the product group.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryLp.lean

complete

theorem UnitaryRepresentation.prodOfCommute_apply.{u_2, u_3, u_6}
  {G₁ : Type u_2} {G₂ : Type u_3} {H : Type u_6} [Group G₁] [Group G₂]
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
  (π₁ : UnitaryRepresentation G₁ H) (π₂ : UnitaryRepresentation G₂ H)
  (hcomm : ∀ (g₁ : G₁) (g₂ : G₂), Commute (π₁ g₁) (π₂ g₂))
  (g : G₁ × G₂) : (π₁.prodOfCommute π₂ hcomm) g = π₁ g.1 * π₂ g.2

theorem UnitaryRepresentation.prodOfCommute_apply.{u_2,
    u_3, u_6}
  {G₁ : Type u_2} {G₂ : Type u_3}
  {H : Type u_6} [Group G₁] [Group G₂]
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H]
  (π₁ : UnitaryRepresentation G₁ H)
  (π₂ : UnitaryRepresentation G₂ H)
  (hcomm :
    ∀ (g₁ : G₁) (g₂ : G₂),
      Commute (π₁ g₁) (π₂ g₂))
  (g : G₁ × G₂) :
  (π₁.prodOfCommute π₂ hcomm) g =
    π₁ g.1 * π₂ g.2

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryLp.lean

complete

theorem UnitaryRepresentation.prodOfCommute_isTopologicallyIrreducible_of_finiteDimensional.{u_1,
    u_4, u_5, u_7}
  {G : Type u_1} {X : Type u_4} {E : Type u_5} [Group G]
  [MeasurableSpace X] [NormedAddCommGroup E] [InnerProductSpace ℂ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure X} {A : Type u_7}
  [Group A] [FiniteDimensional ℂ E] (π : UnitaryRepresentation G E)
  (ρ : UnitaryRepresentation A ↥(MeasureTheory.Lp E 2 μ))
  (ρ₀ : UnitaryRepresentation A ↥(MeasureTheory.Lp ℂ 2 μ))
  (hEmbed :
    ∀ (a : A) (v : E),
      ↑(ρ a) ∘SL ContinuousLinearMap.lpCoordinateEmbedding v =
        ContinuousLinearMap.lpCoordinateEmbedding v ∘SL ↑(ρ₀ a))
  (hProject :
    ∀ (a : A) (v : E),
      ContinuousLinearMap.lpCoordinateProjection v ∘SL ↑(ρ a) =
        ↑(ρ₀ a) ∘SL ContinuousLinearMap.lpCoordinateProjection v)
  (hcomm : ∀ (g : G) (a : A), Commute (π.lpPointwise g) (ρ a))
  (hπ : π.IsTopologicallyIrreducible)
  (hρ₀ : ρ₀.IsTopologicallyIrreducible) :
  (π.lpPointwise.prodOfCommute ρ hcomm).IsTopologicallyIrreducible

theorem UnitaryRepresentation.prodOfCommute_isTopologicallyIrreducible_of_finiteDimensional.{u_1,
    u_4, u_5, u_7}
  {G : Type u_1} {X : Type u_4}
  {E : Type u_5} [Group G]
  [MeasurableSpace X]
  [NormedAddCommGroup E]
  [InnerProductSpace ℂ E]
  [CompleteSpace E]
  {μ : MeasureTheory.Measure X}
  {A : Type u_7} [Group A]
  [FiniteDimensional ℂ E]
  (π : UnitaryRepresentation G E)
  (ρ :
    UnitaryRepresentation A
      ↥(MeasureTheory.Lp E 2 μ))
  (ρ₀ :
    UnitaryRepresentation A
      ↥(MeasureTheory.Lp ℂ 2 μ))
  (hEmbed :
    ∀ (a : A) (v : E),
      ↑(ρ a) ∘SL
          ContinuousLinearMap.lpCoordinateEmbedding
            v =
        ContinuousLinearMap.lpCoordinateEmbedding
            v ∘SL
          ↑(ρ₀ a))
  (hProject :
    ∀ (a : A) (v : E),
      ContinuousLinearMap.lpCoordinateProjection
            v ∘SL
          ↑(ρ a) =
        ↑(ρ₀ a) ∘SL
          ContinuousLinearMap.lpCoordinateProjection
            v)
  (hcomm :
    ∀ (g : G) (a : A),
      Commute (π.lpPointwise g) (ρ a))
  (hπ : π.IsTopologicallyIrreducible)
  (hρ₀ : ρ₀.IsTopologicallyIrreducible) :
  (π.lpPointwise.prodOfCommute ρ
      hcomm).IsTopologicallyIrreducible

A finite-dimensional form of irreducibility of an outer product, proved directly on Bochner
`L²` without a completed Hilbert tensor product.

The representation `ρ` on vector-valued `L²` must be natural with respect to the coordinate
embeddings and projections for its scalar counterpart `ρ₀`.  For an invariant closed subspace,
the matrix coefficients of its orthogonal projection then commute with `ρ₀`, so Schur's lemma
makes them scalar.  Finite coordinate reconstruction makes the projection the pointwise lift of
one value-space operator, and a second application of Schur to `π` makes that operator scalar.
Idempotence leaves only the zero and identity projections.

Theorem5.6.5

uses 1used by 1✓L∃∀N

The irreducible standard complexification of the orthogonal group. Entrywise inclusion sends a real orthogonal matrix to a complex unitary matrix, and Mathlib's star-algebra equivalence between matrices and operators on EuclideanSpace gives the standard complex unitary representation. For a nonempty finite index type, any nonzero invariant complex subspace contains a standard basis vector: subtracting its image under a coordinate sign reflection isolates a nonzero coordinate. Permutation matrices then put every standard basis vector in the subspace, proving irreducibility. This finite coordinate model avoids introducing a general complexification structure.

Lean code for Theorem5.6.5●11 declarations

defdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalComplexification.lean

complete

def Matrix.realToComplexStarMonoidHom.{u_1} {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] : Matrix ι ι ℝ →⋆* Matrix ι ι ℂ

def Matrix.realToComplexStarMonoidHom.{u_1}
  {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] :
  Matrix ι ι ℝ →⋆* Matrix ι ι ℂ

Implementation after :=

:= A.map (RCLike.ofReal : ℝ → ℂ)
  map_one' := by simp
  map_mul' A B := Matrix.map_mul
  map_star' A := by
    simpa only [star_eq_conjTranspose] using
      (Matrix.conjTranspose_map (A := A) (RCLike.ofReal : ℝ → ℂ) (by intro x; simp))

defdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalComplexification.lean

complete

def Matrix.orthogonalComplexificationMatrix.{u_1} {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] :
  ↥(Matrix.orthogonalGroup ι ℝ) →* ↥(Matrix.unitaryGroup ι ℂ)

def Matrix.orthogonalComplexificationMatrix.{u_1}
  {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] :
  ↥(Matrix.orthogonalGroup ι ℝ) →*
    ↥(Matrix.unitaryGroup ι ℂ)

Implementation after :=

:=
  (Unitary.map (realToComplexStarMonoidHom (ι := ι))).toMonoidHom

defdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalComplexification.lean

complete

def Matrix.standardComplexOrthogonalRepresentation.{u_1} {ι : Type u_1}
  [Fintype ι] [DecidableEq ι] :
  UnitaryRepresentation (↥(Matrix.orthogonalGroup ι ℝ))
    (EuclideanSpace ℂ ι)

def Matrix.standardComplexOrthogonalRepresentation.{u_1}
  {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] :
  UnitaryRepresentation
    (↥(Matrix.orthogonalGroup ι ℝ))
    (EuclideanSpace ℂ ι)

Implementation after :=

:=
  (Unitary.map
    (StarMonoidHom.ofClass
      (Matrix.toEuclideanCLM (n := ι) (𝕜 := ℂ)).toStarAlgHom)).toMonoidHom.comp
      orthogonalComplexificationMatrix

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalComplexification.lean

complete

theorem Matrix.standardComplexOrthogonalRepresentation_apply.{u_1}
  {ι : Type u_1} [Fintype ι] [DecidableEq ι]
  (Q : ↥(Matrix.orthogonalGroup ι ℝ)) (z : EuclideanSpace ℂ ι) :
  ↑(Matrix.standardComplexOrthogonalRepresentation Q) z =
    WithLp.toLp 2 (((↑Q).map RCLike.ofReal).mulVec z.ofLp)

theorem Matrix.standardComplexOrthogonalRepresentation_apply.{u_1}
  {ι : Type u_1} [Fintype ι]
  [DecidableEq ι]
  (Q : ↥(Matrix.orthogonalGroup ι ℝ))
  (z : EuclideanSpace ℂ ι) :
  ↑(Matrix.standardComplexOrthogonalRepresentation
          Q)
      z =
    WithLp.toLp 2
      (((↑Q).map RCLike.ofReal).mulVec
        z.ofLp)

defdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalComplexification.lean

complete

def Matrix.coordinateReflection.{u_1} {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] (i : ι) : ↥(Matrix.orthogonalGroup ι ℝ)

def Matrix.coordinateReflection.{u_1}
  {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] (i : ι) :
  ↥(Matrix.orthogonalGroup ι ℝ)

Implementation after :=

:=
  ⟨Matrix.diagonal (fun j => if j = i then -1 else 1), by
    rw [Matrix.mem_orthogonalGroup_iff]
    rw [Matrix.diagonal_transpose, Matrix.diagonal_mul_diagonal]
    ext j k
    by_cases hjk : j = k
    · subst k
      by_cases hj : j = i <;> simp [hj]
    · simp [hjk]⟩

defdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalComplexification.lean

complete

def Matrix.coordinatePermutation.{u_1} {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] (σ : Equiv.Perm ι) : ↥(Matrix.orthogonalGroup ι ℝ)

def Matrix.coordinatePermutation.{u_1}
  {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] (σ : Equiv.Perm ι) :
  ↥(Matrix.orthogonalGroup ι ℝ)

Implementation after :=

:=
  ⟨σ.permMatrix ℝ, by
    rw [Matrix.mem_orthogonalGroup_iff, Matrix.transpose_permMatrix]
    rw [← Matrix.permMatrix_mul]
    simp⟩

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalComplexification.lean

complete

theorem Matrix.coordinateReflection_mulVec.{u_1} {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] (i : ι) (z : ι → ℂ) :
  ((↑(Matrix.coordinateReflection i)).map RCLike.ofReal).mulVec z =
    Function.update z i (-z i)

theorem Matrix.coordinateReflection_mulVec.{u_1}
  {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] (i : ι) (z : ι → ℂ) :
  ((↑(Matrix.coordinateReflection i)).map
          RCLike.ofReal).mulVec
      z =
    Function.update z i (-z i)

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalComplexification.lean

complete

theorem Matrix.coordinatePermutation_mulVec.{u_1} {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] (σ : Equiv.Perm ι) (z : ι → ℂ) :
  ((↑(Matrix.coordinatePermutation σ)).map RCLike.ofReal).mulVec z =
    z ∘ ⇑σ

theorem Matrix.coordinatePermutation_mulVec.{u_1}
  {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] (σ : Equiv.Perm ι)
  (z : ι → ℂ) :
  ((↑(Matrix.coordinatePermutation σ)).map
          RCLike.ofReal).mulVec
      z =
    z ∘ ⇑σ

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalComplexification.lean

complete

theorem Matrix.standardComplexOrthogonalRepresentation_coordinateReflection.{u_1}
  {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι)
  (z : EuclideanSpace ℂ ι) :
  ↑(Matrix.standardComplexOrthogonalRepresentation
          (Matrix.coordinateReflection i))
      z =
    WithLp.toLp 2 (Function.update z.ofLp i (-z.ofLp i))

theorem Matrix.standardComplexOrthogonalRepresentation_coordinateReflection.{u_1}
  {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] (i : ι)
  (z : EuclideanSpace ℂ ι) :
  ↑(Matrix.standardComplexOrthogonalRepresentation
          (Matrix.coordinateReflection i))
      z =
    WithLp.toLp 2
      (Function.update z.ofLp i
        (-z.ofLp i))

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalComplexification.lean

complete

theorem Matrix.standardComplexOrthogonalRepresentation_coordinatePermutation.{u_1}
  {ι : Type u_1} [Fintype ι] [DecidableEq ι] (σ : Equiv.Perm ι)
  (z : EuclideanSpace ℂ ι) :
  ↑(Matrix.standardComplexOrthogonalRepresentation
          (Matrix.coordinatePermutation σ))
      z =
    WithLp.toLp 2 (z.ofLp ∘ ⇑σ)

theorem Matrix.standardComplexOrthogonalRepresentation_coordinatePermutation.{u_1}
  {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] (σ : Equiv.Perm ι)
  (z : EuclideanSpace ℂ ι) :
  ↑(Matrix.standardComplexOrthogonalRepresentation
          (Matrix.coordinatePermutation
            σ))
      z =
    WithLp.toLp 2 (z.ofLp ∘ ⇑σ)

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/OrthogonalComplexification.lean

complete

theorem Matrix.standardComplexOrthogonalRepresentation_isTopologicallyIrreducible.{u_1}
  {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] :
  Matrix.standardComplexOrthogonalRepresentation.IsTopologicallyIrreducible

theorem Matrix.standardComplexOrthogonalRepresentation_isTopologicallyIrreducible.{u_1}
  {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] [Nonempty ι] :
  Matrix.standardComplexOrthogonalRepresentation.IsTopologicallyIrreducible

Theorem5.6.6

uses 1used by 1✓L∃∀N

Circle characters as one-dimensional unitary representations. Multiplication by an element of the complex unit circle is bundled as a complex-linear isometric equivalence. Consequently every multiplicative character \chi:G\to\mathbb T gives a unitary representation on \mathbb C by \pi_\chi(g)z=\chi(g)z. A continuous character gives a strongly continuous representation, and every such representation is topologically irreducible because every closed complex subspace of the complex line is proved to be zero or the whole space. This is the general one-dimensional input used by Mackey induction.

Lean code for Theorem5.6.6●7 declarations

defdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryCharacter.lean

complete

def circleComplexLinearIsometryEquiv : Circle →* ℂ ≃ₗᵢ[ℂ] ℂ

def circleComplexLinearIsometryEquiv :
  Circle →* ℂ ≃ₗᵢ[ℂ] ℂ

Implementation after :=

:=
    { DistribMulAction.toLinearEquiv ℂ ℂ a with
      norm_map' z := show ‖a * z‖ = ‖z‖ by
        rw [norm_mul, Circle.norm_coe, one_mul] }
  map_one' := LinearIsometryEquiv.ext <| by simp
  map_mul' a b := LinearIsometryEquiv.ext <| mul_smul a b

Complex multiplication by a unit-circle element, as a complex-linear isometric equivalence.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

theorem UnitaryRepresentation.closedSubmodule_complex_eq_bot_or_top
  (K : ClosedSubmodule ℂ ℂ) : K = ⊥ ∨ K = ⊤

theorem UnitaryRepresentation.closedSubmodule_complex_eq_bot_or_top
  (K : ClosedSubmodule ℂ ℂ) :
  K = ⊥ ∨ K = ⊤

Every closed complex-linear subspace of the one-dimensional Hilbert space `ℂ` is zero or the
whole space.  This is the final fiberwise step in scalar instances of the Mackey correspondence.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Schur.lean

complete

theorem UnitaryRepresentation.complex_isTopologicallyIrreducible.{u_1}
  {G : Type u_1} [Group G] (π : UnitaryRepresentation G ℂ) :
  π.IsTopologicallyIrreducible

theorem UnitaryRepresentation.complex_isTopologicallyIrreducible.{u_1}
  {G : Type u_1} [Group G]
  (π : UnitaryRepresentation G ℂ) :
  π.IsTopologicallyIrreducible

Every unitary representation on the one-dimensional complex Hilbert space is topologically
irreducible. This supplies the character representations used in scalar Mackey induction.

defdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryCharacter.lean

complete

def UnitaryRepresentation.ofCircleCharacter.{u_1} {G : Type u_1} [Group G]
  (χ : G →* Circle) : UnitaryRepresentation G ℂ

def UnitaryRepresentation.ofCircleCharacter.{u_1}
  {G : Type u_1} [Group G]
  (χ : G →* Circle) :
  UnitaryRepresentation G ℂ

Implementation after :=

:=
  Unitary.linearIsometryEquiv.symm.toMonoidHom.comp
    (circleComplexLinearIsometryEquiv.comp χ)

A circle-valued multiplicative character acts unitarily on the complex line.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryCharacter.lean

complete

theorem UnitaryRepresentation.ofCircleCharacter_apply.{u_1} {G : Type u_1}
  [Group G] (χ : G →* Circle) (g : G) (z : ℂ) :
  ↑((UnitaryRepresentation.ofCircleCharacter χ) g) z = ↑(χ g) * z

theorem UnitaryRepresentation.ofCircleCharacter_apply.{u_1}
  {G : Type u_1} [Group G]
  (χ : G →* Circle) (g : G) (z : ℂ) :
  ↑((UnitaryRepresentation.ofCircleCharacter
            χ)
          g)
      z =
    ↑(χ g) * z

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryCharacter.lean

complete

theorem UnitaryRepresentation.ofCircleCharacter_isStronglyContinuous.{u_1}
  {G : Type u_1} [Group G] [TopologicalSpace G] (χ : G →* Circle)
  (hχ : Continuous ⇑χ) :
  (UnitaryRepresentation.ofCircleCharacter χ).IsStronglyContinuous

theorem UnitaryRepresentation.ofCircleCharacter_isStronglyContinuous.{u_1}
  {G : Type u_1} [Group G]
  [TopologicalSpace G] (χ : G →* Circle)
  (hχ : Continuous ⇑χ) :
  (UnitaryRepresentation.ofCircleCharacter
      χ).IsStronglyContinuous

A continuous circle character gives a strongly continuous one-dimensional unitary
representation.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/UnitaryCharacter.lean

complete

theorem UnitaryRepresentation.ofCircleCharacter_isTopologicallyIrreducible.{u_1}
  {G : Type u_1} [Group G] (χ : G →* Circle) :
  (UnitaryRepresentation.ofCircleCharacter χ).IsTopologicallyIrreducible

theorem UnitaryRepresentation.ofCircleCharacter_isTopologicallyIrreducible.{u_1}
  {G : Type u_1} [Group G]
  (χ : G →* Circle) :
  (UnitaryRepresentation.ofCircleCharacter
      χ).IsTopologicallyIrreducible

A circle character acts irreducibly on the complex line.

Theorem5.6.7

uses 0used by 1✓L∃∀N

Section cocycles on homogeneous spaces. For a subgroup H\leq G, any right inverse s:G/H\to G of the left-coset quotient map gives an H-valued reentry cocycle c(g,q)=s(q)^{-1}g s(g^{-1}q). It satisfies c(gh,q)=c(g,q)c(h,g^{-1}q). Composing with a multiplicative character of H gives the multiplier cocycle used by the section realization of an induced representation. Mathlib's choice-based Quotient.out is provided as a canonical set-theoretic specialization; no measurability of that choice is asserted.

Lean code for Theorem5.6.7●14 declarations

defdefined in LeanRidgelet/ToMathlib/LieGroup/HomogeneousSection.lean

complete

def QuotientGroup.leftCosetSection.{u_1} {G : Type u_1} [Group G]
  (H : Subgroup G) : G ⧸ H → G

def QuotientGroup.leftCosetSection.{u_1}
  {G : Type u_1} [Group G]
  (H : Subgroup G) : G ⧸ H → G

Implementation after :=

:=
  Quotient.out

The choice-based section of the left-coset quotient map.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/HomogeneousSection.lean

complete

theorem QuotientGroup.mk_leftCosetSection.{u_1} {G : Type u_1} [Group G]
  (H : Subgroup G) (q : G ⧸ H) :
  ↑(QuotientGroup.leftCosetSection H q) = q

theorem QuotientGroup.mk_leftCosetSection.{u_1}
  {G : Type u_1} [Group G]
  (H : Subgroup G) (q : G ⧸ H) :
  ↑(QuotientGroup.leftCosetSection H q) =
    q

The chosen representative belongs to the coset it represents.

defdefined in LeanRidgelet/ToMathlib/LieGroup/HomogeneousSection.lean

complete

def QuotientGroup.leftCosetSectionCocycleOf.{u_1} {G : Type u_1} [Group G]
  (H : Subgroup G) (sec : G ⧸ H → G)
  (hsec : Function.RightInverse sec QuotientGroup.mk) (g : G)
  (q : G ⧸ H) : ↥H

def QuotientGroup.leftCosetSectionCocycleOf.{u_1}
  {G : Type u_1} [Group G]
  (H : Subgroup G) (sec : G ⧸ H → G)
  (hsec :
    Function.RightInverse sec
      QuotientGroup.mk)
  (g : G) (q : G ⧸ H) : ↥H

Implementation after :=

:=
  ⟨(sec q)⁻¹ * g * sec (g⁻¹ • q), by
    rw [mul_assoc, ← QuotientGroup.leftRel_apply]
    apply Quotient.exact'
    calc
      QuotientGroup.mk (sec q) = q := hsec q
      _ = g • (g⁻¹ • q) := by simp
      _ = g • QuotientGroup.mk (sec (g⁻¹ • q)) :=
        congrArg (g • ·) (hsec (g⁻¹ • q)).symm
      _ = QuotientGroup.mk (g * sec (g⁻¹ • q)) := rfl⟩

The `H`-valued reentry cocycle associated with the chosen left-coset section.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/HomogeneousSection.lean

complete

theorem QuotientGroup.leftCosetSectionCocycleOf_one.{u_1} {G : Type u_1}
  [Group G] (H : Subgroup G) (sec : G ⧸ H → G)
  (hsec : Function.RightInverse sec QuotientGroup.mk) (q : G ⧸ H) :
  QuotientGroup.leftCosetSectionCocycleOf H sec hsec 1 q = 1

theorem QuotientGroup.leftCosetSectionCocycleOf_one.{u_1}
  {G : Type u_1} [Group G]
  (H : Subgroup G) (sec : G ⧸ H → G)
  (hsec :
    Function.RightInverse sec
      QuotientGroup.mk)
  (q : G ⧸ H) :
  QuotientGroup.leftCosetSectionCocycleOf
      H sec hsec 1 q =
    1

The reentry cocycle of any right inverse to the quotient map is trivial at the identity.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/HomogeneousSection.lean

complete

theorem QuotientGroup.leftCosetSectionCocycleOf_mul.{u_1} {G : Type u_1}
  [Group G] (H : Subgroup G) (sec : G ⧸ H → G)
  (hsec : Function.RightInverse sec QuotientGroup.mk) (g h : G)
  (q : G ⧸ H) :
  QuotientGroup.leftCosetSectionCocycleOf H sec hsec (g * h) q =
    QuotientGroup.leftCosetSectionCocycleOf H sec hsec g q *
      QuotientGroup.leftCosetSectionCocycleOf H sec hsec h (g⁻¹ • q)

theorem QuotientGroup.leftCosetSectionCocycleOf_mul.{u_1}
  {G : Type u_1} [Group G]
  (H : Subgroup G) (sec : G ⧸ H → G)
  (hsec :
    Function.RightInverse sec
      QuotientGroup.mk)
  (g h : G) (q : G ⧸ H) :
  QuotientGroup.leftCosetSectionCocycleOf
      H sec hsec (g * h) q =
    QuotientGroup.leftCosetSectionCocycleOf
        H sec hsec g q *
      QuotientGroup.leftCosetSectionCocycleOf
        H sec hsec h (g⁻¹ • q)

Every choice of section gives the same formal cocycle law.

defdefined in LeanRidgelet/ToMathlib/LieGroup/HomogeneousSection.lean

complete

def QuotientGroup.leftCosetSectionCocycle.{u_1} {G : Type u_1} [Group G]
  (H : Subgroup G) (g : G) (q : G ⧸ H) : ↥H

def QuotientGroup.leftCosetSectionCocycle.{u_1}
  {G : Type u_1} [Group G]
  (H : Subgroup G) (g : G) (q : G ⧸ H) :
  ↥H

Implementation after :=

:=
  leftCosetSectionCocycleOf H (leftCosetSection H) (mk_leftCosetSection H) g q

The reentry cocycle for Mathlib's choice-based quotient section.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/HomogeneousSection.lean

complete

theorem QuotientGroup.leftCosetSectionCocycle_one.{u_1} {G : Type u_1} [Group G]
  (H : Subgroup G) (q : G ⧸ H) :
  QuotientGroup.leftCosetSectionCocycle H 1 q = 1

theorem QuotientGroup.leftCosetSectionCocycle_one.{u_1}
  {G : Type u_1} [Group G]
  (H : Subgroup G) (q : G ⧸ H) :
  QuotientGroup.leftCosetSectionCocycle H
      1 q =
    1

The section cocycle is trivial at the identity.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/HomogeneousSection.lean

complete

theorem QuotientGroup.leftCosetSectionCocycle_mul.{u_1} {G : Type u_1} [Group G]
  (H : Subgroup G) (g h : G) (q : G ⧸ H) :
  QuotientGroup.leftCosetSectionCocycle H (g * h) q =
    QuotientGroup.leftCosetSectionCocycle H g q *
      QuotientGroup.leftCosetSectionCocycle H h (g⁻¹ • q)

theorem QuotientGroup.leftCosetSectionCocycle_mul.{u_1}
  {G : Type u_1} [Group G]
  (H : Subgroup G) (g h : G) (q : G ⧸ H) :
  QuotientGroup.leftCosetSectionCocycle H
      (g * h) q =
    QuotientGroup.leftCosetSectionCocycle
        H g q *
      QuotientGroup.leftCosetSectionCocycle
        H h (g⁻¹ • q)

The reentry factors multiply according to the inverse-left-translation cocycle law.

defdefined in LeanRidgelet/ToMathlib/LieGroup/HomogeneousSection.lean

complete

def QuotientGroup.leftCosetSectionMultiplierOf.{u_1, u_2} {G : Type u_1}
  {M : Type u_2} [Group G] [Monoid M] (H : Subgroup G) (sec : G ⧸ H → G)
  (hsec : Function.RightInverse sec QuotientGroup.mk) (χ : ↥H →* M)
  (g : G) (q : G ⧸ H) : M

def QuotientGroup.leftCosetSectionMultiplierOf.{u_1,
    u_2}
  {G : Type u_1} {M : Type u_2} [Group G]
  [Monoid M] (H : Subgroup G)
  (sec : G ⧸ H → G)
  (hsec :
    Function.RightInverse sec
      QuotientGroup.mk)
  (χ : ↥H →* M) (g : G) (q : G ⧸ H) : M

Implementation after :=

:=
  χ (leftCosetSectionCocycleOf H sec hsec g q)

A subgroup character applied to the section cocycle gives the multiplier used by the
section realization of an induced representation.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/HomogeneousSection.lean

complete

theorem QuotientGroup.leftCosetSectionMultiplierOf_one.{u_1, u_2} {G : Type u_1}
  {M : Type u_2} [Group G] [Monoid M] (H : Subgroup G) (sec : G ⧸ H → G)
  (hsec : Function.RightInverse sec QuotientGroup.mk) (χ : ↥H →* M)
  (q : G ⧸ H) :
  QuotientGroup.leftCosetSectionMultiplierOf H sec hsec χ 1 q = 1

theorem QuotientGroup.leftCosetSectionMultiplierOf_one.{u_1,
    u_2}
  {G : Type u_1} {M : Type u_2} [Group G]
  [Monoid M] (H : Subgroup G)
  (sec : G ⧸ H → G)
  (hsec :
    Function.RightInverse sec
      QuotientGroup.mk)
  (χ : ↥H →* M) (q : G ⧸ H) :
  QuotientGroup.leftCosetSectionMultiplierOf
      H sec hsec χ 1 q =
    1

The multiplier of an arbitrary section is one at the identity.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/HomogeneousSection.lean

complete

theorem QuotientGroup.leftCosetSectionMultiplierOf_mul.{u_1, u_2} {G : Type u_1}
  {M : Type u_2} [Group G] [Monoid M] (H : Subgroup G) (sec : G ⧸ H → G)
  (hsec : Function.RightInverse sec QuotientGroup.mk) (χ : ↥H →* M)
  (g h : G) (q : G ⧸ H) :
  QuotientGroup.leftCosetSectionMultiplierOf H sec hsec χ (g * h) q =
    QuotientGroup.leftCosetSectionMultiplierOf H sec hsec χ g q *
      QuotientGroup.leftCosetSectionMultiplierOf H sec hsec χ h
        (g⁻¹ • q)

theorem QuotientGroup.leftCosetSectionMultiplierOf_mul.{u_1,
    u_2}
  {G : Type u_1} {M : Type u_2} [Group G]
  [Monoid M] (H : Subgroup G)
  (sec : G ⧸ H → G)
  (hsec :
    Function.RightInverse sec
      QuotientGroup.mk)
  (χ : ↥H →* M) (g h : G) (q : G ⧸ H) :
  QuotientGroup.leftCosetSectionMultiplierOf
      H sec hsec χ (g * h) q =
    QuotientGroup.leftCosetSectionMultiplierOf
        H sec hsec χ g q *
      QuotientGroup.leftCosetSectionMultiplierOf
        H sec hsec χ h (g⁻¹ • q)

A character of an arbitrary section's reentry cocycle is a multiplier cocycle.

defdefined in LeanRidgelet/ToMathlib/LieGroup/HomogeneousSection.lean

complete

def QuotientGroup.leftCosetSectionMultiplier.{u_1, u_2} {G : Type u_1}
  {M : Type u_2} [Group G] [Monoid M] (H : Subgroup G) (χ : ↥H →* M)
  (g : G) (q : G ⧸ H) : M

def QuotientGroup.leftCosetSectionMultiplier.{u_1,
    u_2}
  {G : Type u_1} {M : Type u_2} [Group G]
  [Monoid M] (H : Subgroup G)
  (χ : ↥H →* M) (g : G) (q : G ⧸ H) : M

Implementation after :=

:=
  χ (leftCosetSectionCocycle H g q)

The multiplier associated with Mathlib's choice-based quotient section.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/HomogeneousSection.lean

complete

theorem QuotientGroup.leftCosetSectionMultiplier_one.{u_1, u_2} {G : Type u_1}
  {M : Type u_2} [Group G] [Monoid M] (H : Subgroup G) (χ : ↥H →* M)
  (q : G ⧸ H) : QuotientGroup.leftCosetSectionMultiplier H χ 1 q = 1

theorem QuotientGroup.leftCosetSectionMultiplier_one.{u_1,
    u_2}
  {G : Type u_1} {M : Type u_2} [Group G]
  [Monoid M] (H : Subgroup G)
  (χ : ↥H →* M) (q : G ⧸ H) :
  QuotientGroup.leftCosetSectionMultiplier
      H χ 1 q =
    1

The section multiplier is one at the identity.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/HomogeneousSection.lean

complete

theorem QuotientGroup.leftCosetSectionMultiplier_mul.{u_1, u_2} {G : Type u_1}
  {M : Type u_2} [Group G] [Monoid M] (H : Subgroup G) (χ : ↥H →* M)
  (g h : G) (q : G ⧸ H) :
  QuotientGroup.leftCosetSectionMultiplier H χ (g * h) q =
    QuotientGroup.leftCosetSectionMultiplier H χ g q *
      QuotientGroup.leftCosetSectionMultiplier H χ h (g⁻¹ • q)

theorem QuotientGroup.leftCosetSectionMultiplier_mul.{u_1,
    u_2}
  {G : Type u_1} {M : Type u_2} [Group G]
  [Monoid M] (H : Subgroup G)
  (χ : ↥H →* M) (g h : G) (q : G ⧸ H) :
  QuotientGroup.leftCosetSectionMultiplier
      H χ (g * h) q =
    QuotientGroup.leftCosetSectionMultiplier
        H χ g q *
      QuotientGroup.leftCosetSectionMultiplier
        H χ h (g⁻¹ • q)

A character of the reentry cocycle is a multiplier cocycle.

Theorem5.6.8

Statement uses 2

Statement dependency previews

Preview

Theorem 5.1.4

Loading preview

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

used by 1✓L∃∀N

Strong continuity of constant-density pullback representations. Let r_g:X\to X vary continuously in the compact-open topology and satisfy (r_g)_*\mu=c_g\mu, where c_g>0 varies continuously. If a unitary representation acts almost everywhere by f\mapsto c_g^{-1/2}f\circ r_g, then all of its orbit maps on scalar L^2(\mu) are continuous. The proof establishes continuity on indicators from symmetric-difference convergence of their preimages, extends it by induction to Lp simple functions, and then uses density together with the uniform Lipschitz bound supplied by unitarity.

Lean code for Theorem5.6.8●1 theorem

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/StronglyContinuousConstDensity.lean

complete

theorem UnitaryRepresentation.isStronglyContinuous_of_const_density.{u_1, u_2}
  {G : Type u_1} {X : Type u_2} [Group G] [TopologicalSpace G]
  [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [R1Space X]
  {μ : MeasureTheory.Measure X} [μ.InnerRegularCompactLTTop]
  [MeasureTheory.IsLocallyFiniteMeasure μ]
  (π : UnitaryRepresentation G ↥(MeasureTheory.Lp ℂ 2 μ))
  (r : G → C(X, X)) (c : G → NNReal) (hr : Continuous r)
  (hc : Continuous c) (hc_ne : ∀ (g : G), c g ≠ 0)
  (hmap : ∀ (g : G), MeasureTheory.Measure.map (⇑(r g)) μ = ↑(c g) • μ)
  (happly :
    ∀ (g : G) (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      ↑↑(↑(π g) f) =ᵐ[μ] fun x ↦
        (↑↑(NNReal.sqrt (c g)))⁻¹ • ↑↑f ((r g) x)) :
  π.IsStronglyContinuous

theorem UnitaryRepresentation.isStronglyContinuous_of_const_density.{u_1,
    u_2}
  {G : Type u_1} {X : Type u_2} [Group G]
  [TopologicalSpace G]
  [TopologicalSpace X] [MeasurableSpace X]
  [BorelSpace X] [R1Space X]
  {μ : MeasureTheory.Measure X}
  [μ.InnerRegularCompactLTTop]
  [MeasureTheory.IsLocallyFiniteMeasure μ]
  (π :
    UnitaryRepresentation G
      ↥(MeasureTheory.Lp ℂ 2 μ))
  (r : G → C(X, X)) (c : G → NNReal)
  (hr : Continuous r) (hc : Continuous c)
  (hc_ne : ∀ (g : G), c g ≠ 0)
  (hmap :
    ∀ (g : G),
      MeasureTheory.Measure.map (⇑(r g))
          μ =
        ↑(c g) • μ)
  (happly :
    ∀ (g : G)
      (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      ↑↑(↑(π g) f) =ᵐ[μ] fun x ↦
        (↑↑(NNReal.sqrt (c g)))⁻¹ •
          ↑↑f ((r g) x)) :
  π.IsStronglyContinuous

A determinant-corrected pullback formula with continuously varying positive constant density
is strongly continuous on scalar `L²`.

Topological semidirect products and the affine group

Theorem5.6.9

uses 0used by 1✓L∃∀N

Polish topology on unit groups. The units of a normed ring with summable geometric series form an open subspace of the ring. Hence the unit group is Polish whenever the ambient ring is Polish, with its existing topology rather than a newly installed one. This supplies the standard-Borel input for homogeneous spaces whose linear factor is a general linear group.

Lean code for Theorem5.6.9●1 theorem

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PolishUnits.lean

complete

theorem Units.instPolishSpaceOfNormedRing.{u_1} {R : Type u_1} [NormedRing R]
  [HasSummableGeomSeries R] [PolishSpace R] : PolishSpace Rˣ

theorem Units.instPolishSpaceOfNormedRing.{u_1}
  {R : Type u_1} [NormedRing R]
  [HasSummableGeomSeries R]
  [PolishSpace R] : PolishSpace Rˣ

The unit group of a Polish normed ring with summable geometric series is Polish.

The affine group as a locally compact semidirect product. Mathlib's semidirect product is algebraic, so the product topology and its Borel structure are transported through its canonical equivalence with the product of the two factors. A jointly continuous action then makes this a topological group, while second countability, Polishness, and local compactness are inherited from the product. Algebraically, translations and the general linear group give E\rtimes GL(E)\simeq\operatorname{Aff}(E). For a finite-dimensional real normed space, the topological model instead uses the units of the normed algebra E\to_L E; joint continuity follows from bounded bilinear evaluation, its units are locally compact, and forgetting continuity identifies the resulting semidirect product with the same affine automorphism group. Its inverse affine transformations form a continuous map from this group into the compact-open space C(E,E), and their determinant density is read directly from the linear factor. This supplies both the locally compact group input and the continuous family of changes of variables needed for Mackey theory without putting a nonstandard topology on Mathlib's algebraic LinearEquiv.

Lean code for Theorem5.6.10●20 declarations

defdefined in LeanRidgelet/ToMathlib/LieGroup/TopologicalSemidirectProduct.lean

complete

def SemidirectProduct.homeomorphProd.{u_1, u_2} {N : Type u_1}
  {G : Type u_2} [Group N] [Group G] (φ : G →* MulAut N)
  [TopologicalSpace N] [TopologicalSpace G] : N ⋊[φ] G ≃ₜ N × G

def SemidirectProduct.homeomorphProd.{u_1,
    u_2}
  {N : Type u_1} {G : Type u_2} [Group N]
  [Group G] (φ : G →* MulAut N)
  [TopologicalSpace N]
  [TopologicalSpace G] : N ⋊[φ] G ≃ₜ N × G

Implementation after :=

:= equivProd (φ := φ)
  continuous_toFun := continuous_induced_dom
  continuous_invFun := continuous_induced_rng.mpr continuous_id

A semidirect product with its product topology is homeomorphic to the product of its
factors.

defdefined in LeanRidgelet/ToMathlib/LieGroup/TopologicalSemidirectProduct.lean

complete

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

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

Implementation after :=

:=
  borel (N ⋊[φ] G)

The canonical measurable structure on a topological semidirect product is its Borel
structure.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/TopologicalSemidirectProduct.lean

complete

theorem SemidirectProduct.instBorelSpace.{u_1, u_2} {N : Type u_1}
  {G : Type u_2} [Group N] [Group G] (φ : G →* MulAut N)
  [TopologicalSpace N] [TopologicalSpace G] : BorelSpace (N ⋊[φ] G)

theorem SemidirectProduct.instBorelSpace.{u_1,
    u_2}
  {N : Type u_1} {G : Type u_2} [Group N]
  [Group G] (φ : G →* MulAut N)
  [TopologicalSpace N]
  [TopologicalSpace G] :
  BorelSpace (N ⋊[φ] G)

The measurable structure installed above is the Borel structure.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/TopologicalSemidirectProduct.lean

complete

theorem SemidirectProduct.continuous_left.{u_1, u_2} {N : Type u_1}
  {G : Type u_2} [Group N] [Group G] (φ : G →* MulAut N)
  [TopologicalSpace N] [TopologicalSpace G] :
  Continuous SemidirectProduct.left

theorem SemidirectProduct.continuous_left.{u_1,
    u_2}
  {N : Type u_1} {G : Type u_2} [Group N]
  [Group G] (φ : G →* MulAut N)
  [TopologicalSpace N]
  [TopologicalSpace G] :
  Continuous SemidirectProduct.left

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/TopologicalSemidirectProduct.lean

complete

theorem SemidirectProduct.continuous_right.{u_1, u_2} {N : Type u_1}
  {G : Type u_2} [Group N] [Group G] (φ : G →* MulAut N)
  [TopologicalSpace N] [TopologicalSpace G] :
  Continuous SemidirectProduct.right

theorem SemidirectProduct.continuous_right.{u_1,
    u_2}
  {N : Type u_1} {G : Type u_2} [Group N]
  [Group G] (φ : G →* MulAut N)
  [TopologicalSpace N]
  [TopologicalSpace G] :
  Continuous SemidirectProduct.right

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/TopologicalSemidirectProduct.lean

complete

theorem SemidirectProduct.instSecondCountableTopology.{u_1, u_2} {N : Type u_1}
  {G : Type u_2} [Group N] [Group G] (φ : G →* MulAut N)
  [TopologicalSpace N] [TopologicalSpace G] [SecondCountableTopology N]
  [SecondCountableTopology G] : SecondCountableTopology (N ⋊[φ] G)

theorem SemidirectProduct.instSecondCountableTopology.{u_1,
    u_2}
  {N : Type u_1} {G : Type u_2} [Group N]
  [Group G] (φ : G →* MulAut N)
  [TopologicalSpace N]
  [TopologicalSpace G]
  [SecondCountableTopology N]
  [SecondCountableTopology G] :
  SecondCountableTopology (N ⋊[φ] G)

Second countability of a semidirect product only depends on its product topology.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/TopologicalSemidirectProduct.lean

complete

theorem SemidirectProduct.instPolishSpace.{u_1, u_2} {N : Type u_1}
  {G : Type u_2} [Group N] [Group G] (φ : G →* MulAut N)
  [TopologicalSpace N] [TopologicalSpace G] [PolishSpace N]
  [PolishSpace G] : PolishSpace (N ⋊[φ] G)

theorem SemidirectProduct.instPolishSpace.{u_1,
    u_2}
  {N : Type u_1} {G : Type u_2} [Group N]
  [Group G] (φ : G →* MulAut N)
  [TopologicalSpace N]
  [TopologicalSpace G] [PolishSpace N]
  [PolishSpace G] : PolishSpace (N ⋊[φ] G)

A semidirect product with its product topology is Polish when both factors are Polish.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/TopologicalSemidirectProduct.lean

complete

theorem SemidirectProduct.instLocallyCompactSpace.{u_1, u_2} {N : Type u_1}
  {G : Type u_2} [Group N] [Group G] (φ : G →* MulAut N)
  [TopologicalSpace N] [TopologicalSpace G] [LocallyCompactSpace N]
  [LocallyCompactSpace G] : LocallyCompactSpace (N ⋊[φ] G)

theorem SemidirectProduct.instLocallyCompactSpace.{u_1,
    u_2}
  {N : Type u_1} {G : Type u_2} [Group N]
  [Group G] (φ : G →* MulAut N)
  [TopologicalSpace N]
  [TopologicalSpace G]
  [LocallyCompactSpace N]
  [LocallyCompactSpace G] :
  LocallyCompactSpace (N ⋊[φ] G)

Local compactness of a semidirect product only depends on its product topology.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/TopologicalSemidirectProduct.lean

complete

theorem SemidirectProduct.isTopologicalGroupOfContinuous.{u_1, u_2}
  {N : Type u_1} {G : Type u_2} [Group N] [Group G] (φ : G →* MulAut N)
  [TopologicalSpace N] [TopologicalSpace G] [IsTopologicalGroup N]
  [IsTopologicalGroup G] (hφ : Continuous fun p ↦ (φ p.1) p.2) :
  IsTopologicalGroup (N ⋊[φ] G)

theorem SemidirectProduct.isTopologicalGroupOfContinuous.{u_1,
    u_2}
  {N : Type u_1} {G : Type u_2} [Group N]
  [Group G] (φ : G →* MulAut N)
  [TopologicalSpace N]
  [TopologicalSpace G]
  [IsTopologicalGroup N]
  [IsTopologicalGroup G]
  (hφ : Continuous fun p ↦ (φ p.1) p.2) :
  IsTopologicalGroup (N ⋊[φ] G)

A jointly continuous action makes the product-topology semidirect product a topological
group.

defdefined in LeanRidgelet/ToMathlib/LieGroup/AffineSemidirect.lean

complete

def AffineEquiv.linearMultiplicativeActionHom.{u_1, u_2} (k : Type u_1)
  (E : Type u_2) [Ring k] [AddCommGroup E] [Module k E] :
  (E ≃ₗ[k] E) →* MulAut (Multiplicative E)

def AffineEquiv.linearMultiplicativeActionHom.{u_1,
    u_2}
  (k : Type u_1) (E : Type u_2) [Ring k]
  [AddCommGroup E] [Module k E] :
  (E ≃ₗ[k] E) →* MulAut (Multiplicative E)

Implementation after :=

:= L.toAddEquiv.toMultiplicative
  map_one' := by
    ext x
    rfl
  map_mul' L M := by
    ext x
    rfl

The natural action of the general linear group on the multiplicative synonym of the additive
translation group.

defdefined in LeanRidgelet/ToMathlib/LieGroup/AffineSemidirect.lean

complete

def AffineEquiv.semidirectProductEquiv.{u_1, u_2} (k : Type u_1)
  (E : Type u_2) [Ring k] [AddCommGroup E] [Module k E] :
  AffineEquiv.SemidirectProduct k E ≃* (E ≃ᵃ[k] E)

def AffineEquiv.semidirectProductEquiv.{u_1,
    u_2}
  (k : Type u_1) (E : Type u_2) [Ring k]
  [AddCommGroup E] [Module k E] :
  AffineEquiv.SemidirectProduct k E ≃*
    (E ≃ᵃ[k] E)

Implementation after :=

:= ofSemidirectProduct k E
  invFun := toSemidirectProduct k E
  left_inv p := by
    apply SemidirectProduct.ext
    · simp
    · rfl
  right_inv g := by
    exact (translation_mul_linear k E g).symm
  map_mul' p q := by
    apply AffineEquiv.ext
    intro x
    simp only [ofSemidirectProduct_apply, SemidirectProduct.mul_left,
      linearMultiplicativeActionHom_apply, toAdd_mul, toAdd_ofAdd,
      SemidirectProduct.mul_right, AffineEquiv.coe_mul, Function.comp_apply,
      map_add, LinearEquiv.mul_apply]
    ac_rfl

The coordinate-free group equivalence `E ⋊ GL(E) ≃ Aff(E)`.

defdefined in LeanRidgelet/ToMathlib/LieGroup/AffineSemidirect.lean

complete

def AffineEquiv.continuousLinearMultiplicativeActionHom.{u_3} (E : Type u_3)
  [NormedAddCommGroup E] [NormedSpace ℝ E] :
  (E →L[ℝ] E)ˣ →* MulAut (Multiplicative E)

def AffineEquiv.continuousLinearMultiplicativeActionHom.{u_3}
  (E : Type u_3) [NormedAddCommGroup E]
  [NormedSpace ℝ E] :
  (E →L[ℝ] E)ˣ →*
    MulAut (Multiplicative E)

Implementation after :=

:= (ContinuousLinearEquiv.unitsEquiv ℝ E L).toLinearEquiv.toAddEquiv.toMultiplicative
  map_one' := by
    ext x
    rfl
  map_mul' L M := by
    ext x
    rfl

The action of invertible continuous endomorphisms on the translation group.  Using units of
the continuous-endomorphism ring gives the linear factor its standard topological-group
structure.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/AffineSemidirect.lean

complete

theorem AffineEquiv.continuous_continuousLinearMultiplicativeAction.{u_3}
  (E : Type u_3) [NormedAddCommGroup E] [NormedSpace ℝ E] :
  Continuous fun p ↦
    ((AffineEquiv.continuousLinearMultiplicativeActionHom E) p.1) p.2

theorem AffineEquiv.continuous_continuousLinearMultiplicativeAction.{u_3}
  (E : Type u_3) [NormedAddCommGroup E]
  [NormedSpace ℝ E] :
  Continuous fun p ↦
    ((AffineEquiv.continuousLinearMultiplicativeActionHom
          E)
        p.1)
      p.2

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/AffineSemidirect.lean

complete

theorem AffineEquiv.instIsTopologicalGroupTopologicalSemidirectProduct.{u_3}
  (E : Type u_3) [NormedAddCommGroup E] [NormedSpace ℝ E] :
  IsTopologicalGroup (AffineEquiv.TopologicalSemidirectProduct E)

theorem AffineEquiv.instIsTopologicalGroupTopologicalSemidirectProduct.{u_3}
  (E : Type u_3) [NormedAddCommGroup E]
  [NormedSpace ℝ E] :
  IsTopologicalGroup
    (AffineEquiv.TopologicalSemidirectProduct
      E)

defdefined in LeanRidgelet/ToMathlib/LieGroup/AffineSemidirect.lean

complete

def AffineEquiv.continuousLinearUnitsEquivLinearEquiv.{u_3} (E : Type u_3)
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] :
  (E →L[ℝ] E)ˣ ≃* E ≃ₗ[ℝ] E

def AffineEquiv.continuousLinearUnitsEquivLinearEquiv.{u_3}
  (E : Type u_3) [NormedAddCommGroup E]
  [NormedSpace ℝ E]
  [FiniteDimensional ℝ E] :
  (E →L[ℝ] E)ˣ ≃* E ≃ₗ[ℝ] E

Implementation after :=

:= (ContinuousLinearEquiv.unitsEquiv ℝ E L).toLinearEquiv
  invFun L := (ContinuousLinearEquiv.unitsEquiv ℝ E).symm L.toContinuousLinearEquiv
  left_inv L := by
    apply Units.ext
    rfl
  right_inv L := by
    ext x
    rfl
  map_mul' L M := by
    ext x
    rfl

In finite dimension, forgetting continuity identifies the units of the continuous
endomorphism ring with the full general linear group.

defdefined in LeanRidgelet/ToMathlib/LieGroup/AffineSemidirect.lean

complete

def AffineEquiv.topologicalSemidirectProductEquiv.{u_3} (E : Type u_3)
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] :
  AffineEquiv.TopologicalSemidirectProduct E ≃* (E ≃ᵃ[ℝ] E)

def AffineEquiv.topologicalSemidirectProductEquiv.{u_3}
  (E : Type u_3) [NormedAddCommGroup E]
  [NormedSpace ℝ E]
  [FiniteDimensional ℝ E] :
  AffineEquiv.TopologicalSemidirectProduct
      E ≃*
    (E ≃ᵃ[ℝ] E)

Implementation after :=

:=
  (SemidirectProduct.congr (MulEquiv.refl (Multiplicative E))
      (continuousLinearUnitsEquivLinearEquiv E) (by
        intro L
        ext x
        rfl)).trans
    (semidirectProductEquiv ℝ E)

The locally compact topological semidirect-product model has the same underlying group as the
affine automorphism group.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/AffineSemidirect.lean

complete

theorem AffineEquiv.topologicalSemidirectProductEquiv_linear.{u_3}
  (E : Type u_3) [NormedAddCommGroup E] [NormedSpace ℝ E]
  [FiniteDimensional ℝ E]
  (p : AffineEquiv.TopologicalSemidirectProduct E) :
  ((AffineEquiv.topologicalSemidirectProductEquiv E) p).linear =
    ↑((ContinuousLinearEquiv.unitsEquiv ℝ E) p.right)

theorem AffineEquiv.topologicalSemidirectProductEquiv_linear.{u_3}
  (E : Type u_3) [NormedAddCommGroup E]
  [NormedSpace ℝ E]
  [FiniteDimensional ℝ E]
  (p :
    AffineEquiv.TopologicalSemidirectProduct
      E) :
  ((AffineEquiv.topologicalSemidirectProductEquiv
          E)
        p).linear =
    ↑((ContinuousLinearEquiv.unitsEquiv ℝ
          E)
        p.right)

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/AffineSemidirect.lean

complete

theorem AffineEquiv.det_topologicalSemidirectProductEquiv_linear.{u_3}
  (E : Type u_3) [NormedAddCommGroup E] [NormedSpace ℝ E]
  [FiniteDimensional ℝ E]
  (p : AffineEquiv.TopologicalSemidirectProduct E) :
  LinearMap.det
      ↑((AffineEquiv.topologicalSemidirectProductEquiv E) p).linear =
    LinearMap.det ↑↑p.right

theorem AffineEquiv.det_topologicalSemidirectProductEquiv_linear.{u_3}
  (E : Type u_3) [NormedAddCommGroup E]
  [NormedSpace ℝ E]
  [FiniteDimensional ℝ E]
  (p :
    AffineEquiv.TopologicalSemidirectProduct
      E) :
  LinearMap.det
      ↑((AffineEquiv.topologicalSemidirectProductEquiv
              E)
            p).linear =
    LinearMap.det ↑↑p.right

defdefined in LeanRidgelet/ToMathlib/LieGroup/AffineSemidirect.lean

complete

def AffineEquiv.topologicalSemidirectProductInverseContinuousMap.{u_3}
  (E : Type u_3) [NormedAddCommGroup E] [NormedSpace ℝ E]
  (p : AffineEquiv.TopologicalSemidirectProduct E) : C(E, E)

def AffineEquiv.topologicalSemidirectProductInverseContinuousMap.{u_3}
  (E : Type u_3) [NormedAddCommGroup E]
  [NormedSpace ℝ E]
  (p :
    AffineEquiv.TopologicalSemidirectProduct
      E) :
  C(E, E)

Implementation after :=

:= (↑(p.right⁻¹) : E →L[ℝ] E) (x - p.left.toAdd)
  continuous_toFun := (↑(p.right⁻¹) : E →L[ℝ] E).continuous.comp
    (continuous_id.sub continuous_const)

The inverse affine map represented by a point of the topological semidirect product, bundled
as a continuous map on the underlying normed space.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/AffineSemidirect.lean

complete

theorem AffineEquiv.continuous_topologicalSemidirectProductInverseContinuousMap.{u_3}
  (E : Type u_3) [NormedAddCommGroup E] [NormedSpace ℝ E] :
  Continuous
    (AffineEquiv.topologicalSemidirectProductInverseContinuousMap E)

theorem AffineEquiv.continuous_topologicalSemidirectProductInverseContinuousMap.{u_3}
  (E : Type u_3) [NormedAddCommGroup E]
  [NormedSpace ℝ E] :
  Continuous
    (AffineEquiv.topologicalSemidirectProductInverseContinuousMap
      E)

The inverse affine maps depend continuously on the semidirect-product parameter in the
compact-open topology.

The general linear orbit

Theorem5.6.11

uses 0used by 1✓L∃∀N

The nonzero vectors form one conull orbit of the general linear group. A reflection maps a nonzero vector to the rescaling of a target vector having the same norm, and a final invertible scalar map corrects the norm. Hence both the ordinary action Lx and the contragredient action L^{-T}x are transitive away from zero. For any additive Haar measure on a nontrivial finite-dimensional real normed space, the omitted singleton is null. These are the elementary orbit inputs for a Mackey-machine proof of affine irreducibility; they do not depend on the ridgelet theory.

Lean code for Theorem5.6.11●5 declarations

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/GeneralLinearOrbit.lean

complete

theorem LinearEquiv.exists_apply_eq_of_ne_zero.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x y : E} (hx : x ≠ 0)
  (hy : y ≠ 0) : ∃ L, L x = y

theorem LinearEquiv.exists_apply_eq_of_ne_zero.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {x y : E}
  (hx : x ≠ 0) (hy : y ≠ 0) : ∃ L, L x = y

The general linear group of a finite-dimensional real inner-product space acts transitively
on its nonzero vectors.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/GeneralLinearOrbit.lean

complete

theorem LinearEquiv.adjoint_adjoint.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (L : E ≃ₗ[ℝ] E) :
  L.adjoint.adjoint = L

theorem LinearEquiv.adjoint_adjoint.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (L : E ≃ₗ[ℝ] E) : L.adjoint.adjoint = L

Taking the adjoint twice returns the original finite-dimensional linear equivalence.

defdefined in LeanRidgelet/ToMathlib/LieGroup/GeneralLinearOrbit.lean

complete

def LinearEquiv.contragredientHom.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] : (E ≃ₗ[ℝ] E) →* E ≃ₗ[ℝ] E

def LinearEquiv.contragredientHom.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] :
  (E ≃ₗ[ℝ] E) →* E ≃ₗ[ℝ] E

Implementation after :=

:= L.symm.adjoint
  map_one' := by
    apply LinearEquiv.ext
    intro x
    apply ext_inner_left ℝ
    intro z
    change ⟪z, ((1 : E ≃ₗ[ℝ] E).symm : E →ₗ[ℝ] E).adjoint x⟫_ℝ = ⟪z, x⟫_ℝ
    rw [LinearMap.adjoint_inner_right]
    rfl
  map_mul' L M := by
    apply LinearEquiv.ext
    intro x
    apply ext_inner_left ℝ
    intro z
    change ⟪z, ((L * M).symm : E →ₗ[ℝ] E).adjoint x⟫_ℝ =
      ⟪z, (L.symm : E →ₗ[ℝ] E).adjoint ((M.symm : E →ₗ[ℝ] E).adjoint x)⟫_ℝ
    rw [LinearMap.adjoint_inner_right, LinearMap.adjoint_inner_right,
      LinearMap.adjoint_inner_right]
    rfl

The contragredient operation `L ↦ L⁻ᵀ`, as an automorphism homomorphism of the general
linear group.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/GeneralLinearOrbit.lean

complete

theorem LinearEquiv.exists_symm_adjoint_apply_eq_of_ne_zero.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  {x y : E} (hx : x ≠ 0) (hy : y ≠ 0) : ∃ L, L.symm.adjoint x = y

theorem LinearEquiv.exists_symm_adjoint_apply_eq_of_ne_zero.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] {x y : E}
  (hx : x ≠ 0) (hy : y ≠ 0) :
  ∃ L, L.symm.adjoint x = y

The contragredient automorphisms `L⁻ᵀ` also act transitively on nonzero vectors. This is
the orbit calculation used on the Fourier side of the affine quasi-regular representation.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/GeneralLinearOrbit.lean

complete

theorem MeasureTheory.setOf_ne_zero_ae_eq_univ.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  (mu : MeasureTheory.Measure E) [mu.IsAddHaarMeasure] :
  {x | x ≠ 0} =ᵐ[mu] Set.univ

theorem MeasureTheory.setOf_ne_zero_ae_eq_univ.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [Nontrivial E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (mu : MeasureTheory.Measure E)
  [mu.IsAddHaarMeasure] :
  {x | x ≠ 0} =ᵐ[mu] Set.univ

The nonzero vectors form a conull set for every additive Haar measure on a nontrivial
finite-dimensional real normed space.