Documentation

TauCeti.RepresentationTheory.Compact.Haar

Normalized Haar measure on compact groups #

This file normalizes Mathlib's Haar measure on a compact topological group to a probability measure, and records its left, right, and inversion invariance.

The Layer 0 design follows the compact-groups roadmap and its accompanying Suggested.lean.

Since haarProb is a Haar measure and a probability measure, Mathlib's generic API applies to it directly: MeasureTheory.Measure.isHaarMeasure_eq_of_isProbabilityMeasure identifies it with any other Haar probability measure, and MeasureTheory.integral_mul_left_eq_self, MeasureTheory.integral_mul_right_eq_self and MeasureTheory.integral_inv_eq_self give the translation and inversion identities used for averaging representations.

source
theorem TauCeti.haar_univ_ne_zero (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] :
MeasureTheory.Measure.haar Set.univ ≠ 0

Haar measure of a nonempty locally compact group has nonzero total mass.

source
theorem TauCeti.isMulRightInvariant_of_isHaarMeasure_of_isProbabilityMeasure (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [MeasureTheory.IsProbabilityMeasure μ] :
μ.IsMulRightInvariant

Every probability Haar measure on a locally compact group is right-invariant.

source
theorem TauCeti.isInvInvariant_of_isHaarMeasure_of_isProbabilityMeasure (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [MeasureTheory.IsProbabilityMeasure μ] :
μ.IsInvInvariant

Every probability Haar measure on a locally compact group is invariant under inversion.

source
theorem TauCeti.haar_univ_lt_top (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] :
MeasureTheory.Measure.haar Set.univ < ⊤

Haar measure of a compact group has finite total mass.

source
noncomputable def TauCeti.haarProb (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] :
MeasureTheory.Measure G

Haar probability measure on a compact topological group.

Equations
Instances For
    source
    theorem TauCeti.haarProb_def (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] :
    haarProb G = (MeasureTheory.Measure.haar Set.univ)⁻¹ • MeasureTheory.Measure.haar

    The definition of normalized Haar measure as a rescaling of Mathlib's Haar measure.

    source
    instance TauCeti.isProbabilityMeasure_haarProb (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] :
    MeasureTheory.IsProbabilityMeasure (haarProb G)
    source
    theorem TauCeti.haarProb_apply_univ (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] :
    (haarProb G) Set.univ = 1

    Normalized Haar measure has total mass one.

    Not a simp lemma: simp already closes this goal from the IsProbabilityMeasure instance via MeasureTheory.measure_univ.

    source
    instance TauCeti.isMulLeftInvariant_haarProb (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] :
    (haarProb G).IsMulLeftInvariant
    source
    instance TauCeti.isHaarMeasure_haarProb (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] :
    (haarProb G).IsHaarMeasure
    source
    instance TauCeti.isMulRightInvariant_haarProb (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] :
    (haarProb G).IsMulRightInvariant

    Normalized Haar measure is invariant under right multiplication.

    source
    instance TauCeti.isInvInvariant_haarProb (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] :
    (haarProb G).IsInvInvariant

    Normalized Haar measure is invariant under inversion.

    source
    theorem TauCeti.eq_haarProb_of_isHaarMeasure_of_isProbabilityMeasure (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [MeasureTheory.IsProbabilityMeasure μ] :
    μ = haarProb G

    A probability Haar measure on a compact group is the normalized Haar measure.