Structures · Analysis

MeasureTheory.Measure.IsAddHaarMeasure

A measure on an additive group is an additive 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 [IsAddHaarMeasure μ] [Regular μ] or [IsAddHaarMeasure μ] [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