Documentation

TauCeti.RepresentationTheory.Compact.Unitarizable

Weyl's unitarian trick #

Averaging the inner product of a Hilbert space over a compact group turns it into a G-invariant inner product. This file carries out that averaging for a continuous representation π of a compact group. Rather than producing a second InnerProductSpace structure on V — which would not make the given π unitary for the fixed instance Lean already has — the averaged form is represented by its Gram operator

gramOperator π hπ = ∫ g, (π g)† ∘ (π g) ∂(haarProb G),

a positive-definite self-adjoint operator satisfying ⟪v, S w⟫ = ∫ g, ⟪π g v, π g w⟫. Invariance of the averaged form is then the operator identity (π g)† ∘ S ∘ (π g) = S.

Main definitions #

Main statements #

This is the compact-group replacement for the invertibility of |G| in Maschke's theorem. The invariant-complement and complete-reducibility results of TauCeti.RepresentationTheory.Continuous.InvariantComplement take IsUnitary as a hypothesis; this file does not discharge that hypothesis, but the invariant form built here is the input a unitarization construction needs. TauCeti.RepresentationTheory.Compact.UnitaryModel carries that construction out in finite dimensions, conjugating π into a representation that is unitary for the inner product V was given.

The mathematical development follows Daniel Bump, Lie Groups, second edition, Chapter 2.

source
theorem ContRepresentation.exists_pos_mul_norm_le_norm_map {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [NontriviallyNormedField 𝕜] [Group G] [TopologicalSpace G] [CompactSpace G] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) :
∃ (c : ℝ), 0 < c ∧ ∀ (g : G) (v : V), c * ‖v‖ ≤ ‖(π g) v‖

The action operators of a continuous representation of a compact group are uniformly bounded below: there is a c > 0 with c * ‖v‖ ≤ ‖π g v‖ for every g and v.

The bound comes from applying the inverse operator π g⁻¹, whose norm is bounded uniformly in g because G is compact and π is continuous. Only the seminormed-space structure is involved, so this is stated before the inner product enters.

source
noncomputable def ContRepresentation.gramOperator {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) :
V →L[𝕜] V

The Gram operator of the Haar-averaged inner product ⟪v, w⟫_G = ∫ g, ⟪π g v, π g w⟫ ∂(haarProb G) of a continuous representation of a compact group.

The averaged form is recorded through this operator rather than as a second InnerProductSpace structure: Lean fixes one inner product on V, and it is the operator identity (π g)† ∘ gramOperator π hπ ∘ (π g) = gramOperator π hπ that expresses G-invariance of the averaged form. The real scalar action needed for integration is the canonical restriction of the 𝕜-action, so no additional scalar structure on V is required.

Equations
Instances For
    source
    theorem ContRepresentation.inner_gramOperator {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v w : V) :
    inner 𝕜 v ((π.gramOperator hπ) w) = ∫ (g : G), inner 𝕜 ((π g) v) ((π g) w) ∂TauCeti.haarProb G

    The defining property of the Gram operator: it represents the Haar-averaged inner product.

    source
    theorem ContRepresentation.inner_gramOperator_left {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v w : V) :
    inner 𝕜 ((π.gramOperator hπ) v) w = ∫ (g : G), inner 𝕜 ((π g) v) ((π g) w) ∂TauCeti.haarProb G

    The Gram operator represents the Haar-averaged inner product, written on the left.

    source
    theorem ContRepresentation.isSymmetric_gramOperator {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) :
    (↑(π.gramOperator hπ)).IsSymmetric

    The averaged form is Hermitian: the Gram operator is symmetric.

    source
    theorem ContRepresentation.isSelfAdjoint_gramOperator {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) :
    IsSelfAdjoint (π.gramOperator hπ)

    The Gram operator of the averaged form is self-adjoint.

    Positive definiteness #

    Nondegeneracy of the averaged form is where compactness of G enters a second time: the operator norms ‖π g‖ are uniformly bounded, so ‖π g v‖ is bounded below by a positive multiple of ‖v‖, and the average of ‖π g v‖ ^ 2 cannot collapse to zero.

    source
    theorem ContRepresentation.inner_gramOperator_self {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v : V) :
    inner 𝕜 ((π.gramOperator hπ) v) v = ↑(∫ (g : G), ‖(π g) v‖ ^ 2 ∂TauCeti.haarProb G)

    The averaged form evaluated on the diagonal is the average of ‖π g v‖ ^ 2.

    source
    theorem ContRepresentation.isPositive_gramOperator {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) :
    (π.gramOperator hπ).IsPositive

    The Gram operator of the averaged form is a positive operator.

    source
    theorem ContRepresentation.exists_pos_mul_norm_sq_le_re_inner_gramOperator {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) :
    ∃ (c : ℝ), 0 < c ∧ ∀ (v : V), c * ‖v‖ ^ 2 ≤ RCLike.re (inner 𝕜 ((π.gramOperator hπ) v) v)

    The Haar-averaged form bounds the original norm square below by a fixed positive multiple. In particular, its positivity is uniform over all vectors, even in infinite dimensions.

    source
    theorem ContRepresentation.re_inner_gramOperator_self_pos {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) {v : V} (hv : v ≠ 0) :
    0 < RCLike.re (inner 𝕜 ((π.gramOperator hπ) v) v)

    Positive definiteness of the averaged form. For a nonzero vector the averaged norm square is strictly positive; this is what makes ⟪v, w⟫_G = ⟪gramOperator π hπ v, w⟫ an inner product rather than merely a positive semidefinite form.

    source
    theorem ContRepresentation.gramOperator_injective {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) :
    Function.Injective ⇑(π.gramOperator hπ)

    The averaged form is nondegenerate, so the Gram operator is injective.

    Invariance #

    source
    @[simp]
    theorem ContRepresentation.inner_gramOperator_map_map {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (g : G) (v w : V) :
    inner 𝕜 ((π g) v) ((π.gramOperator hπ) ((π g) w)) = inner 𝕜 v ((π.gramOperator hπ) w)

    The averaged form is G-invariant. The original action preserves the averaged inner product ⟪v, w⟫_G = ⟪v, gramOperator π hπ w⟫, even when it does not preserve the given one.

    source
    @[simp]
    theorem ContRepresentation.adjoint_comp_gramOperator_comp {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (g : G) :
    ContinuousLinearMap.adjoint (π g) ∘SL π.gramOperator hπ ∘SL π g = π.gramOperator hπ

    The operator form of G-invariance of the averaged form: (π g)† ∘ S ∘ (π g) = S.

    source
    theorem ContRepresentation.isUnitarizable {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) :
    ∃ (S : V →L[𝕜] V), IsSelfAdjoint S ∧ (∀ (v : V), v ≠ 0 → 0 < RCLike.re (inner 𝕜 (S v) v)) ∧ ∀ (g : G), ContinuousLinearMap.adjoint (π g) ∘SL S ∘SL π g = S

    Weyl's unitarian trick. Every continuous representation of a compact group on a Hilbert space carries a G-invariant positive-definite Hermitian form, represented by a positive-definite self-adjoint operator S with (π g)† ∘ S ∘ (π g) = S.

    This operator is the input to unitarization: retopologizing V by ⟪S ·, ·⟫, or conjugating π by S ^ (1 / 2), makes every π g unitary. Neither construction is carried out here, so this file does not itself produce an IsUnitary representation; ContRepresentation.exists_isUnitary_congr does, for a finite-dimensional carrier.

    source
    @[simp]
    theorem ContRepresentation.gramOperator_eq_one {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (hunitary : π.IsUnitary) :
    π.gramOperator hπ = 1

    Averaging a form that is already invariant changes nothing: the Gram operator of a unitary representation is the identity.