Theorems · Inductive type · Lie groups

MeasureTheory.Measure.IsHaarMeasure

{G : Type u_3} → [Group G] → [TopologicalSpace G] → [inst : MeasurableSpace G] → MeasureTheory.Measure G → Prop

A measure on a group is a Haar measure if it is left-invariant, and gives finite mass to compact sets and positive mass to open sets. Textbooks generally require an additional regularity assumption to ensure nice behavior on arbitrary locally compact groups. Use [IsHaarMeasure μ] [Regular μ] or [IsHaarMeasure μ] [InnerRegular μ] in these situations. Note that a Haar measure in our sense is automatically regular and inner regular on second countable locally compact groups, as checked just below this definition.

Defined in

Mathlib.MeasureTheory.Group.Measure

Cited by

63 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

GroupTopologicalSpaceMeasurableSpace