Theorems · Inductive type · Lie groups

MeasureTheory.Measure.IsAddHaarMeasure

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

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

Cited by

255 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 5 definitions · uses no axioms

Assumes

AddGroupTopologicalSpaceMeasurableSpace