# Documentation

Mathlib.MeasureTheory.Group.Action

# 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 : } →
• measure_preimage_vadd : ∀ (c : M) ⦃s : Set α⦄, μ ((fun x => c +ᵥ x) ⁻¹' s) = μ s

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.

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

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.

Instances
theorem MeasureTheory.VAddInvariantMeasure.zero.proof_1 {M : Type u_1} {α : Type u_2} [] [VAdd M α] :
instance MeasureTheory.VAddInvariantMeasure.zero {M : Type v} {α : Type w} [] [VAdd M α] :
instance MeasureTheory.SMulInvariantMeasure.zero {M : Type v} {α : Type w} [] [SMul M α] :
theorem MeasureTheory.VAddInvariantMeasure.add.proof_1 {M : Type u_1} {α : Type u_2} [VAdd M α] {m : } {μ : } {ν : } :
instance MeasureTheory.VAddInvariantMeasure.add {M : Type v} {α : Type w} [VAdd M α] {m : } {μ : } {ν : } :
instance MeasureTheory.SMulInvariantMeasure.add {M : Type v} {α : Type w} [SMul M α] {m : } {μ : } {ν : } :
instance MeasureTheory.VAddInvariantMeasure.vadd {M : Type v} {α : Type w} [VAdd M α] {m : } {μ : } (c : ENNReal) :
theorem MeasureTheory.VAddInvariantMeasure.vadd.proof_1 {M : Type u_1} {α : Type u_2} [VAdd M α] {m : } {μ : } (c : ENNReal) :
instance MeasureTheory.SMulInvariantMeasure.smul {M : Type v} {α : Type w} [SMul M α] {m : } {μ : } (c : ENNReal) :
instance MeasureTheory.VAddInvariantMeasure.vadd_nnreal {M : Type v} {α : Type w} [VAdd M α] {m : } {μ : } (c : NNReal) :
theorem MeasureTheory.VAddInvariantMeasure.vadd_nnreal.proof_1 {M : Type u_1} {α : Type u_2} [VAdd M α] {m : } {μ : } (c : NNReal) :
instance MeasureTheory.SMulInvariantMeasure.smul_nnreal {M : Type v} {α : Type w} [SMul M α] {m : } {μ : } (c : NNReal) :
@[simp]
theorem MeasureTheory.measurePreserving_vadd {M : Type v} {α : Type w} {m : } [] [VAdd M α] [] (c : M) (μ : ) :
@[simp]
theorem MeasureTheory.measurePreserving_smul {M : Type v} {α : Type w} {m : } [] [SMul M α] [] (c : M) (μ : ) :
@[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 : ) :
theorem MeasureTheory.vaddInvariantMeasure_map_vadd.proof_1 {M : Type u_1} {N : Type u_2} {α : Type u_3} [] [] [] [VAdd M α] [VAdd N α] [] [] [] (μ : ) (n : N) :
instance MeasureTheory.vaddInvariantMeasure_map_vadd {M : Type uM} {N : Type uN} {α : Type uα} [] [] [] [VAdd M α] [VAdd N α] [] [] [] (μ : ) (n : N) :
instance MeasureTheory.smulInvariantMeasure_map_smul {M : Type uM} {N : Type uN} {α : Type uα} [] [] [] [SMul M α] [SMul N α] [] [] [] (μ : ) (n : N) :
theorem MeasureTheory.vaddInvariantMeasure_tfae (G : Type u) {α : Type w} {m : } [] [] [] [] (μ : ) :
List.TFAE [, ∀ (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]

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 : } [] [] [] [] (μ : ) :
List.TFAE [, ∀ (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]

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 : ) :
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 ⋃ (g : G) (_ : g I), g +ᵥ U) → Prop) :
(x : I, K ⋃ (g : G) (_ : g I), g +ᵥ U) → ((t : ) → (ht : K ⋃ (g : G) (_ : g t), g +ᵥ U) → motive (_ : I, K ⋃ (g : G) (_ : g I), g +ᵥ U)) → motive x
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 : ) :
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, c +ᵥ x U) → Prop) :
(x : c, c +ᵥ x U) → ((g : G) → (hg : g +ᵥ x U) → motive (_ : c, c +ᵥ x U)) → motive x
Instances For
theorem MeasureTheory.isLocallyFiniteMeasure_of_vaddInvariant (G : Type u) {α : Type w} {m : } [] [] [] [] {μ : } [] [] [] {U : Set α} (hU : ) (hne : ) (hμU : μ U ) :
theorem MeasureTheory.isLocallyFiniteMeasure_of_smulInvariant (G : Type u) {α : Type w} {m : } [] [] [] [] {μ : } [] [] [] {U : Set α} (hU : ) (hne : ) (hμU : μ U ) :
theorem MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_ne_zero (G : Type u) {α : Type w} {m : } [] [] [] [] {μ : } [] [] [] {U : Set α} (hμ : μ 0) (hU : ) (hne : ) :
0 < μ U
abbrev MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_ne_zero.match_1 {α : Type u_1} {m : } {μ : } [] (motive : (K, μ K 0) → Prop) :
(x : K, μ K 0) → ((_K : Set α) → (hK : ) → (hμK : μ _K 0) → motive (_ : K, μ K 0)) → motive x
Instances For
theorem MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_ne_zero (G : Type u) {α : Type w} {m : } [] [] [] [] {μ : } [] [] [] {U : Set α} (hμ : μ 0) (hU : ) (hne : ) :
0 < μ U
theorem MeasureTheory.measure_pos_iff_nonempty_of_vaddInvariant (G : Type u) {α : Type w} {m : } [] [] [] [] {μ : } [] [] [] {U : Set α} (hμ : μ 0) (hU : ) :
0 < μ U
theorem MeasureTheory.measure_pos_iff_nonempty_of_smulInvariant (G : Type u) {α : Type w} {m : } [] [] [] [] {μ : } [] [] [] {U : Set α} (hμ : μ 0) (hU : ) :
0 < μ U
theorem MeasureTheory.measure_eq_zero_iff_eq_empty_of_vaddInvariant (G : Type u) {α : Type w} {m : } [] [] [] [] {μ : } [] [] [] {U : Set α} (hμ : μ 0) (hU : ) :
μ U = 0 U =
theorem MeasureTheory.measure_eq_zero_iff_eq_empty_of_smulInvariant (G : Type u) {α : Type w} {m : } [] [] [] [] {μ : } [] [] [] {U : Set α} (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 : ) (hy : ) :
theorem MeasureTheory.vadd_ae_eq_self_of_mem_zmultiples {G : Type u} {α : Type w} {s : Set α} {m : } [] [] [] [] {μ : } {x : G} {y : G} (hs : ) (hy : ) :
theorem MeasureTheory.neg_vadd_ae_eq_self {G : Type u} {α : Type w} {s : Set α} {m : } [] [] [] [] {μ : } {x : G} (hs : ) :
theorem MeasureTheory.inv_smul_ae_eq_self {G : Type u} {α : Type w} {s : Set α} {m : } [] [] [] [] {μ : } {x : G} (hs : ) :