Theorems · Theorem · measure theory

Module.Basis.addHaar_eq_iff

∀ {ι : Type u_1} {E : Type u_3} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [SecondCountableTopology E] (b : Module.Basis ι ℝ E)
  (μ : MeasureTheory.Measure E) [MeasureTheory.SigmaFinite μ] [μ.IsAddLeftInvariant],
  b.addHaar = μ ↔ μ ↑b.parallelepiped = 1

Let μ be a σ-finite left invariant measure on E. Then μ is equal to the Haar measure defined by b iff the parallelepiped defined by b has measure 1 for μ.

Defined in

Mathlib.MeasureTheory.Measure.Haar.OfBasis

Cited by

5 results in Mathlib

Foundations

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

Assumes

FintypeNormedAddCommGroupNormedSpaceMeasurableSpaceBorelSpaceSecondCountableTopologyMeasureTheory.SigmaFiniteMeasureTheory.Measure.IsAddLeftInvariant