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.

class MeasureTheory.VAddInvariantMeasure (M : Type u_1) (α : Type u_2) [VAdd M α] : {x : MeasurableSpace α} → MeasureTheory.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

theorem MeasureTheory.VAddInvariantMeasure.measure_preimage_vadd {M : Type u_1} {α : Type u_2} : ∀ {inst : VAdd M α} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : MeasureTheory.VAddInvariantMeasure M α μ] (c : M) ⦃s : Set α⦄, MeasurableSet s → μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) = μ s

theorem MeasureTheory.smulInvariantMeasure_iff (M : Type u_1) (α : Type u_2) [SMul M α] : ∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α), MeasureTheory.SMulInvariantMeasure M α μ ↔ ∀ (c : M) ⦃s : Set α⦄, MeasurableSet s → μ ((fun (x : α) => c • x) ⁻¹' s) = μ s

class MeasureTheory.SMulInvariantMeasure (M : Type u_1) (α : Type u_2) [SMul M α] : {x : MeasurableSpace α} → MeasureTheory.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

theorem MeasureTheory.SMulInvariantMeasure.measure_preimage_smul {M : Type u_1} {α : Type u_2} : ∀ {inst : SMul M α} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : MeasureTheory.SMulInvariantMeasure M α μ] (c : M) ⦃s : Set α⦄, MeasurableSet s → μ ((fun (x : α) => c • x) ⁻¹' s) = μ s

theorem MeasureTheory.vaddInvariantMeasure_iff (M : Type u_1) (α : Type u_2) [VAdd M α] : ∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α), MeasureTheory.VAddInvariantMeasure M α μ ↔ ∀ (c : M) ⦃s : Set α⦄, MeasurableSet s → μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) = μ s

class MeasureTheory.Measure.IsAddLeftInvariant {G : Type u_1} [MeasurableSpace G] [Add G] (μ : MeasureTheory.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), MeasureTheory.Measure.map (fun (x : G) => g + x) μ = μ

theorem MeasureTheory.Measure.IsAddLeftInvariant.map_add_left_eq_self {G : Type u_1} : ∀ {inst : MeasurableSpace G} {inst_1 : Add G} {μ : MeasureTheory.Measure G} [self : μ.IsAddLeftInvariant] (g : G), MeasureTheory.Measure.map (fun (x : G) => g + x) μ = μ

class MeasureTheory.Measure.IsMulLeftInvariant {G : Type u_1} [MeasurableSpace G] [Mul G] (μ : MeasureTheory.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), MeasureTheory.Measure.map (fun (x : G) => g * x) μ = μ

theorem MeasureTheory.Measure.IsMulLeftInvariant.map_mul_left_eq_self {G : Type u_1} : ∀ {inst : MeasurableSpace G} {inst_1 : Mul G} {μ : MeasureTheory.Measure G} [self : μ.IsMulLeftInvariant] (g : G), MeasureTheory.Measure.map (fun (x : G) => g * x) μ = μ

class MeasureTheory.Measure.IsAddRightInvariant {G : Type u_1} [MeasurableSpace G] [Add G] (μ : MeasureTheory.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.

• map_add_right_eq_self : ∀ (g : G), MeasureTheory.Measure.map (fun (x : G) => x + g) μ = μ

theorem MeasureTheory.Measure.IsAddRightInvariant.map_add_right_eq_self {G : Type u_1} : ∀ {inst : MeasurableSpace G} {inst_1 : Add G} {μ : MeasureTheory.Measure G} [self : μ.IsAddRightInvariant] (g : G), MeasureTheory.Measure.map (fun (x : G) => x + g) μ = μ

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

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

• map_mul_right_eq_self : ∀ (g : G), MeasureTheory.Measure.map (fun (x : G) => x * g) μ = μ

theorem MeasureTheory.Measure.IsMulRightInvariant.map_mul_right_eq_self {G : Type u_1} : ∀ {inst : MeasurableSpace G} {inst_1 : Mul G} {μ : MeasureTheory.Measure G} [self : μ.IsMulRightInvariant] (g : G), MeasureTheory.Measure.map (fun (x : G) => x * g) μ = μ

instance MeasureTheory.Measure.IsAddLeftInvariant.vaddInvariantMeasure {G : Type u_1} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [Add G] [μ.IsAddLeftInvariant] : MeasureTheory.VAddInvariantMeasure G G μ

Equations

• ⋯ = ⋯

instance MeasureTheory.Measure.IsMulLeftInvariant.smulInvariantMeasure {G : Type u_1} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [Mul G] [μ.IsMulLeftInvariant] : MeasureTheory.SMulInvariantMeasure G G μ

Equations

• ⋯ = ⋯

instance MeasureTheory.Measure.instVAddInvariantMeasureSubtypeMemAddSubmonoidOfIsAddLeftInvariant {G : Type u_1} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddMonoid G] (s : AddSubmonoid G) [μ.IsAddLeftInvariant] : MeasureTheory.VAddInvariantMeasure (↥s) G μ

Equations

• ⋯ = ⋯

instance MeasureTheory.Measure.instSMulInvariantMeasureSubtypeMemSubmonoidOfIsMulLeftInvariant {G : Type u_1} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [Monoid G] (s : Submonoid G) [μ.IsMulLeftInvariant] : MeasureTheory.SMulInvariantMeasure (↥s) G μ

Equations

• ⋯ = ⋯

instance MeasureTheory.Measure.IsAddRightInvariant.toVAddInvariantMeasure_op {G : Type u_1} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [Add G] [μ.IsAddRightInvariant] : MeasureTheory.VAddInvariantMeasure Gᵃᵒᵖ G μ

Equations

• ⋯ = ⋯

instance MeasureTheory.Measure.IsMulRightInvariant.toSMulInvariantMeasure_op {G : Type u_1} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [Mul G] [μ.IsMulRightInvariant] : MeasureTheory.SMulInvariantMeasure Gᵐᵒᵖ G μ

Equations

• ⋯ = ⋯