Structures · Analysis

MeasureTheory.Measure.IsHaarMeasure

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

Shape

One type argument