Theorems · Theorem · measure theory

MeasureTheory.vaddInvariantMeasure_tfae

∀ (G : Type u) {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  (μ : MeasureTheory.Measure α) [MeasurableConstVAdd G α],
  [MeasureTheory.VAddInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun x => c +ᵥ x) ⁻¹' s) = μ s,
      ∀ (c : G) (s : Set α), MeasurableSet s → μ (c +ᵥ s) = μ s,
      ∀ (c : G) (s : Set α), μ ((fun x => c +ᵥ x) ⁻¹' s) = μ s, ∀ (c : G) (s : Set α), μ (c +ᵥ s) = μ s,
      ∀ (c : G), MeasureTheory.Measure.map (fun x => c +ᵥ x) μ = μ,
      ∀ (c : G), MeasureTheory.MeasurePreserving (fun x => c +ᵥ x) μ μ].TFAE

Equivalent definitions of a measure invariant under an additive action of a group. - 0: VAddInvariantMeasure G α μ; - 1: for every c : G and a measurable set s, the measure of the preimage of s under vector addition (c +ᵥ ·) is equal to the measure of s; - 2: for every c : G and a measurable set s, the measure of the image c +ᵥ s of s under vector addition (c +ᵥ ·) is equal to the measure of s; - 3, 4: properties 2, 3 for any set, including non-measurable ones; - 5: for any c : G, vector addition of c maps μ to μ; - 6: for any c : G, vector addition of c is a measure-preserving map.

Defined in

Mathlib.MeasureTheory.Group.Action

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddGroupAddActionMeasurableConstVAdd