Definitions about invariant measures #

In this file we define typeclasses for measures invariant under (scalar) multiplication.

MeasureTheory.SMulInvariantMeasure M α μ says that the measure μ is invariant under scalar multiplication by c : M;
MeasureTheory.VAddInvariantMeasure M α μ is the additive version of this typeclass;
MeasureTheory.Measure.IsMulLeftInvariant μ, MeasureTheory.Measure.IsMulRightInvariant μ say that the measure μ is invariant under multiplication on the left and on the right, respectively.
MeasureTheory.Measure.IsAddLeftInvariant μ, MeasureTheory.Measure.IsAddRightInvariant μ are the additive versions of these typeclasses.

For basic facts about the first two typeclasses, see Mathlib/MeasureTheory/Group/Action. For facts about left/right-invariant measures, see Mathlib/MeasureTheory/Group/Measure.

Implementation Notes #

The smul/vadd typeclasses and the left/right multiplication typeclasses were defined by different people with different tastes, so the former explicitly use measures of the preimages, while the latter use MeasureTheory.Measure.map.

If the left/right multiplication is measurable (which is the case in most if not all interesting examples), these definitions are equivalent.

The definitions that use MeasureTheory.Measure.map imply that the left (resp., right) multiplication is AEMeasurable.

source

class MeasureTheory.VAddInvariantMeasure (M : Type u_1) (α : Type u_2) [VAdd M α] {x✝ : MeasurableSpace α} (μ : Measure α) :

Prop

A measure μ : Measure α is invariant under an additive action of M on α if for any measurable set s : Set α and c : M, the measure of its preimage under fun x => c +ᵥ x is equal to the measure of s.

measure_preimage_vadd (c : M) ⦃s : Set α⦄ : MeasurableSet s → μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) = μ s

Instances

source

class MeasureTheory.SMulInvariantMeasure (M : Type u_1) (α : Type u_2) [SMul M α] {x✝ : MeasurableSpace α} (μ : Measure α) :

Prop

A measure μ : Measure α is invariant under a multiplicative action of M on α if for any measurable set s : Set α and c : M, the measure of its preimage under fun x => c • x is equal to the measure of s.

measure_preimage_smul (c : M) ⦃s : Set α⦄ : MeasurableSet s → μ ((fun (x : α) => c • x) ⁻¹' s) = μ s

Instances

source

theorem MeasureTheory.smulInvariantMeasure_iff (M : Type u_1) (α : Type u_2) [SMul M α] {x✝ : MeasurableSpace α} (μ : Measure α) :

SMulInvariantMeasure M α μ ↔ ∀ (c : M) ⦃s : Set α⦄, MeasurableSet s → μ ((fun (x : α) => c • x) ⁻¹' s) = μ s

source

theorem MeasureTheory.vaddInvariantMeasure_iff (M : Type u_1) (α : Type u_2) [VAdd M α] {x✝ : MeasurableSpace α} (μ : Measure α) :

VAddInvariantMeasure M α μ ↔ ∀ (c : M) ⦃s : Set α⦄, MeasurableSet s → μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) = μ s

source

class MeasureTheory.Measure.IsAddLeftInvariant {G : Type u_1} [MeasurableSpace G] [Add G] (μ : Measure G) :

Prop

A measure μ on a measurable additive group is left invariant if the measure of left translations of a set are equal to the measure of the set itself.

map_add_left_eq_self (g : G) : map (fun (x : G) => g + x) μ = μ

Instances

source

class MeasureTheory.Measure.IsMulLeftInvariant {G : Type u_1} [MeasurableSpace G] [Mul G] (μ : Measure G) :

Prop

A measure μ on a measurable group is left invariant if the measure of left translations of a set are equal to the measure of the set itself.

map_mul_left_eq_self (g : G) : map (fun (x : G) => g * x) μ = μ

Instances

source

class MeasureTheory.Measure.IsAddRightInvariant {G : Type u_1} [MeasurableSpace G] [Add G] (μ : Measure G) :

Prop

A measure μ on a measurable additive group is right invariant if the measure of right translations of a set are equal to the measure of the set itself.