Theorems · Definition · measure theory

MeasureTheory.Measure.haar.chaar

{G : Type u_1} →
  [inst : Group G] →
    [inst_1 : TopologicalSpace G] →
      [IsTopologicalGroup G] → TopologicalSpace.PositiveCompacts G → TopologicalSpace.Compacts G → ℝ

This is the "limit" of prehaar K₀ U K as U becomes a smaller and smaller open neighborhood of (1 : G). More precisely, it is defined to be an arbitrary element in the intersection of all the sets clPrehaar K₀ V in haarProduct K₀. This is roughly equal to the Haar measure on compact sets, but it can differ slightly. We do know that haarMeasure K₀ (interior K) ≤ chaar K₀ K ≤ haarMeasure K₀ K.

Defined in

Mathlib.MeasureTheory.Measure.Haar.Basic

Cited by

12 results in Mathlib

Foundations

Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupTopologicalSpaceIsTopologicalGroup