Documentation

Carleson.ToMathlib.MeasureTheory.Measure.Haar.Unique

source
@[instance 100]
instance MeasureTheory.Measure.IsHaarMeasure.isInvInvariant_of_isMulRightInvariant {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsHaarMeasure] [LocallyCompactSpace G] [μ.IsMulRightInvariant] [μ.Regular] :
μ.IsInvInvariant

Any regular bi-invariant Haar measure is invariant under inversion.

source
@[instance 100]
instance MeasureTheory.Measure.IsAddHaarMeasure.isNegInvariant_of_isAddRightInvariant {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsAddHaarMeasure] [LocallyCompactSpace G] [μ.IsAddRightInvariant] [μ.Regular] :
μ.IsNegInvariant

Any regular bi-invariant additive Haar measure is invariant under negation.

source
@[instance 100]
instance MeasureTheory.Measure.IsHaarMeasure.isInvInvariant_of_regular' {G : Type u_2} [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsHaarMeasure] [LocallyCompactSpace G] [μ.Regular] :
μ.IsInvInvariant

Any regular Haar measure is invariant under inversion in an abelian group.

source
@[instance 100]
instance MeasureTheory.Measure.IsAddHaarMeasure.isNegInvariant_of_regular' {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsAddHaarMeasure] [LocallyCompactSpace G] [μ.Regular] :
μ.IsNegInvariant

Any regular additive Haar measure is invariant under negation in an abelian group.