# Measures invariant under group actions #

A measure μ : Measure α is said to be invariant under an action of a group G if scalar multiplication by c : G is a measure preserving map for all c. In this file we define a typeclass for measures invariant under action of an (additive or multiplicative) group and prove some basic properties of such measures.

class MeasureTheory.VAddInvariantMeasure (M : Type u_1) (α : Type u_2) [VAdd M α] :
{x : } →

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 α⦄, μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) = μ s
Instances
∀ {x : } {μ : } [self : ] (c : M) ⦃s : Set α⦄, μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) = μ s
class MeasureTheory.SMulInvariantMeasure (M : Type u_1) (α : Type u_2) [SMul M α] :
{x : } →

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 α⦄, μ ((fun (x : α) => c x) ⁻¹' s) = μ s
Instances
theorem MeasureTheory.SMulInvariantMeasure.measure_preimage_smul {M : Type u_1} {α : Type u_2} [SMul M α] :
∀ {x : } {μ : } [self : ] (c : M) ⦃s : Set α⦄, μ ((fun (x : α) => c x) ⁻¹' s) = μ s
instance MeasureTheory.VAddInvariantMeasure.zero {M : Type v} {α : Type w} [] [VAdd M α] :
Equations
• =
instance MeasureTheory.SMulInvariantMeasure.zero {M : Type v} {α : Type w} [] [SMul M α] :
Equations
• =
instance MeasureTheory.VAddInvariantMeasure.add {M : Type v} {α : Type w} [VAdd M α] {m : } {μ : } {ν : } :
Equations
• =
instance MeasureTheory.SMulInvariantMeasure.add {M : Type v} {α : Type w} [SMul M α] {m : } {μ : } {ν : } :
Equations
• =
instance MeasureTheory.VAddInvariantMeasure.vadd {M : Type v} {α : Type w} [VAdd M α] {m : } {μ : } (c : ENNReal) :
Equations
• =
instance MeasureTheory.SMulInvariantMeasure.smul {M : Type v} {α : Type w} [SMul M α] {m : } {μ : } (c : ENNReal) :
Equations
• =
instance MeasureTheory.VAddInvariantMeasure.vadd_nnreal {M : Type v} {α : Type w} [VAdd M α] {m : } {μ : } (c : NNReal) :
Equations
• =
instance MeasureTheory.SMulInvariantMeasure.smul_nnreal {M : Type v} {α : Type w} [SMul M α] {m : } {μ : } (c : NNReal) :
Equations
• =
@[simp]
theorem MeasureTheory.measurePreserving_vadd {M : Type v} {α : Type w} {m : } [] [VAdd M α] [] (c : M) (μ : ) :
MeasureTheory.MeasurePreserving (fun (x : α) => c +ᵥ x) μ μ
@[simp]
theorem MeasureTheory.measurePreserving_smul {M : Type v} {α : Type w} {m : } [] [SMul M α] [] (c : M) (μ : ) :
MeasureTheory.MeasurePreserving (fun (x : α) => c x) μ μ
@[simp]
theorem MeasureTheory.map_vadd {M : Type v} {α : Type w} {m : } [] [VAdd M α] [] (c : M) (μ : ) :
MeasureTheory.Measure.map (fun (x : α) => c +ᵥ x) μ = μ
@[simp]
theorem MeasureTheory.map_smul {M : Type v} {α : Type w} {m : } [] [SMul M α] [] (c : M) (μ : ) :
MeasureTheory.Measure.map (fun (x : α) => c x) μ = μ
theorem MeasureTheory.vaddInvariantMeasure_map {M : Type uM} {α : Type uα} {β : Type uβ} [] [] [] [VAdd M α] [VAdd M β] [] (μ : ) (f : αβ) (hsmul : ∀ (m : M) (a : α), f (m +ᵥ a) = m +ᵥ f a) (hf : ) :
theorem MeasureTheory.smulInvariantMeasure_map {M : Type uM} {α : Type uα} {β : Type uβ} [] [] [] [SMul M α] [SMul M β] [] (μ : ) (f : αβ) (hsmul : ∀ (m : M) (a : α), f (m a) = m f a) (hf : ) :
instance MeasureTheory.vaddInvariantMeasure_map_vadd {M : Type uM} {N : Type uN} {α : Type uα} [] [] [] [VAdd M α] [VAdd N α] [] [] [] (μ : ) (n : N) :
Equations
• =
instance MeasureTheory.smulInvariantMeasure_map_smul {M : Type uM} {N : Type uN} {α : Type uα} [] [] [] [SMul M α] [SMul N α] [] [] [] (μ : ) (n : N) :
Equations
• =
theorem MeasureTheory.vaddInvariantMeasure_tfae (G : Type u) {α : Type w} {m : } [] [] [] [] (μ : ) :
[, ∀ (c : G) (s : Set α), μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) = μ s, ∀ (c : G) (s : Set α), μ (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.

theorem MeasureTheory.smulInvariantMeasure_tfae (G : Type u) {α : Type w} {m : } [] [] [] [] (μ : ) :
[, ∀ (c : G) (s : Set α), μ ((fun (x : α) => c x) ⁻¹' s) = μ s, ∀ (c : G) (s : Set α), μ (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 a multiplicative action of a group.

• 0: SMulInvariantMeasure G α μ;

• 1: for every c : G and a measurable set s, the measure of the preimage of s under scalar multiplication by 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 scalar multiplication by 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, scalar multiplication by c maps μ to μ;

• 6: for any c : G, scalar multiplication by c is a measure preserving map.

@[simp]
theorem MeasureTheory.measure_preimage_vadd {G : Type u} {α : Type w} {m : } [] [] [] [] (c : G) (μ : ) (s : Set α) :
μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) = μ s
@[simp]
theorem MeasureTheory.measure_preimage_smul {G : Type u} {α : Type w} {m : } [] [] [] [] (c : G) (μ : ) (s : Set α) :
μ ((fun (x : α) => c x) ⁻¹' s) = μ s
@[simp]
theorem MeasureTheory.measure_vadd {G : Type u} {α : Type w} {m : } [] [] [] [] (c : G) (μ : ) (s : Set α) :
μ (c +ᵥ s) = μ s
@[simp]
theorem MeasureTheory.measure_smul {G : Type u} {α : Type w} {m : } [] [] [] [] (c : G) (μ : ) (s : Set α) :
μ (c s) = μ s
theorem MeasureTheory.NullMeasurableSet.vadd {G : Type u} {α : Type w} {m : } [] [] [] [] {μ : } {s : Set α} (hs : ) (c : G) :
theorem MeasureTheory.NullMeasurableSet.smul {G : Type u} {α : Type w} {m : } [] [] [] [] {μ : } {s : Set α} (hs : ) (c : G) :
theorem MeasureTheory.measure_vadd_null {G : Type u} {α : Type w} {m : } [] [] [] [] {μ : } {s : Set α} (h : μ s = 0) (c : G) :
μ (c +ᵥ s) = 0
theorem MeasureTheory.measure_smul_null {G : Type u} {α : Type w} {m : } [] [] [] [] {μ : } {s : Set α} (h : μ s = 0) (c : G) :
μ (c s) = 0
theorem MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_compact_ne_zero (G : Type u) {α : Type w} {m : } [] [] [] [] {μ : } [] [] [] {K : Set α} {U : Set α} (hK : ) (hμK : μ K 0) (hU : ) (hne : U.Nonempty) :
0 < μ U

If measure μ is invariant under an additive group action and is nonzero on a compact set K, then it is positive on any nonempty open set. In case of a regular measure, one can assume μ ≠ 0 instead of μ K ≠ 0, see MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_ne_zero.

abbrev MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_compact_ne_zero.match_1 (G : Type u_1) {α : Type u_2} [] [] {K : Set α} {U : Set α} (motive : (∃ (I : ), K gI, g +ᵥ U)Prop) :
∀ (x : ∃ (I : ), K gI, g +ᵥ U), (∀ (t : ) (ht : K gt, g +ᵥ U), motive )motive x
Equations
• =
Instances For
theorem MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_compact_ne_zero (G : Type u) {α : Type w} {m : } [] [] [] [] {μ : } [] [] [] {K : Set α} {U : Set α} (hK : ) (hμK : μ K 0) (hU : ) (hne : U.Nonempty) :
0 < μ U

If measure μ is invariant under a group action and is nonzero on a compact set K, then it is positive on any nonempty open set. In case of a regular measure, one can assume μ ≠ 0 instead of μ K ≠ 0, see MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_ne_zero.

abbrev MeasureTheory.isLocallyFiniteMeasure_of_vaddInvariant.match_1 (G : Type u_1) {α : Type u_2} [] [] {U : Set α} (x : α) (motive : (∃ (c : G), c +ᵥ x U)Prop) :
∀ (x_1 : ∃ (c : G), c +ᵥ x U), (∀ (g : G) (hg : g +ᵥ x U), motive )motive x_1
Equations
• =
Instances For
theorem MeasureTheory.isLocallyFiniteMeasure_of_vaddInvariant (G : Type u) {α : Type w} {m : } [] [] [] [] {μ : } [] [] [] {U : Set α} (hU : ) (hne : U.Nonempty) (hμU : μ U ) :
theorem MeasureTheory.isLocallyFiniteMeasure_of_smulInvariant (G : Type u) {α : Type w} {m : } [] [] [] [] {μ : } [] [] [] {U : Set α} (hU : ) (hne : U.Nonempty) (hμU : μ U ) :
abbrev MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_ne_zero.match_1 {α : Type u_1} {m : } {μ : } [] (motive : (∃ (K : Set α), μ K 0)Prop) :
∀ (x : ∃ (K : Set α), μ K 0), (∀ (_K : Set α) (hK : ) (hμK : μ _K 0), motive )motive x
Equations
• =
Instances For
theorem MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_ne_zero (G : Type u) {α : Type w} {m : } [] [] [] [] {μ : } [] [] [] {U : Set α} [μ.Regular] (hμ : μ 0) (hU : ) (hne : U.Nonempty) :
0 < μ U
theorem MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_ne_zero (G : Type u) {α : Type w} {m : } [] [] [] [] {μ : } [] [] [] {U : Set α} [μ.Regular] (hμ : μ 0) (hU : ) (hne : U.Nonempty) :
0 < μ U
theorem MeasureTheory.measure_pos_iff_nonempty_of_vaddInvariant (G : Type u) {α : Type w} {m : } [] [] [] [] {μ : } [] [] [] {U : Set α} [μ.Regular] (hμ : μ 0) (hU : ) :
0 < μ U U.Nonempty
theorem MeasureTheory.measure_pos_iff_nonempty_of_smulInvariant (G : Type u) {α : Type w} {m : } [] [] [] [] {μ : } [] [] [] {U : Set α} [μ.Regular] (hμ : μ 0) (hU : ) :
0 < μ U U.Nonempty
theorem MeasureTheory.measure_eq_zero_iff_eq_empty_of_vaddInvariant (G : Type u) {α : Type w} {m : } [] [] [] [] {μ : } [] [] [] {U : Set α} [μ.Regular] (hμ : μ 0) (hU : ) :
μ U = 0 U =
theorem MeasureTheory.measure_eq_zero_iff_eq_empty_of_smulInvariant (G : Type u) {α : Type w} {m : } [] [] [] [] {μ : } [] [] [] {U : Set α} [μ.Regular] (hμ : μ 0) (hU : ) :
μ U = 0 U =
theorem MeasureTheory.smul_ae_eq_self_of_mem_zpowers {G : Type u} {α : Type w} {s : Set α} {m : } [] [] [] [] {μ : } {x : G} {y : G} (hs : μ.ae.EventuallyEq (x s) s) (hy : ) :
μ.ae.EventuallyEq (y s) s
theorem MeasureTheory.vadd_ae_eq_self_of_mem_zmultiples {G : Type u} {α : Type w} {s : Set α} {m : } [] [] [] [] {μ : } {x : G} {y : G} (hs : μ.ae.EventuallyEq (x +ᵥ s) s) (hy : ) :
μ.ae.EventuallyEq (y +ᵥ s) s
theorem MeasureTheory.neg_vadd_ae_eq_self {G : Type u} {α : Type w} {s : Set α} {m : } [] [] [] [] {μ : } {x : G} (hs : μ.ae.EventuallyEq (x +ᵥ s) s) :
μ.ae.EventuallyEq (-x +ᵥ s) s
theorem MeasureTheory.inv_smul_ae_eq_self {G : Type u} {α : Type w} {s : Set α} {m : } [] [] [] [] {μ : } {x : G} (hs : μ.ae.EventuallyEq (x s) s) :
μ.ae.EventuallyEq (x⁻¹ s) s