# mathlibdocumentation

measure_theory.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]
structure measure_theory.vadd_invariant_measure (M : Type u_4) (α : Type u_5) [ α] {_x : measurable_space α} (μ : measure_theory.measure α) :
Prop
• measure_preimage_vadd : ∀ (c : M) ⦃s : set α⦄, μ ((λ (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 λ x, c +ᵥ x is equal to the measure of s.

Instances
@[class]
structure measure_theory.smul_invariant_measure (M : Type u_4) (α : Type u_5) [ α] {_x : measurable_space α} (μ : measure_theory.measure α) :
Prop
• measure_preimage_smul : ∀ (c : M) ⦃s : set α⦄, μ ((λ (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 λ x, c • x is equal to the measure of s.

Instances
@[protected, instance]
def measure_theory.vadd_invariant_measure.zero {M : Type u_2} {α : Type u_3} [ α] :
@[protected, instance]
def measure_theory.smul_invariant_measure.zero {M : Type u_2} {α : Type u_3} [ α] :
@[protected, instance]
def measure_theory.smul_invariant_measure.add {M : Type u_2} {α : Type u_3} [ α] {m : measurable_space α} {μ ν : measure_theory.measure α}  :
+ ν)
@[protected, instance]
def measure_theory.vadd_invariant_measure.add {M : Type u_2} {α : Type u_3} [ α] {m : measurable_space α} {μ ν : measure_theory.measure α}  :
+ ν)
@[protected, instance]
def measure_theory.vadd_invariant_measure.vadd {M : Type u_2} {α : Type u_3} [ α] {m : measurable_space α} {μ : measure_theory.measure α} (c : ℝ≥0∞) :
(c μ)
@[protected, instance]
def measure_theory.smul_invariant_measure.smul {M : Type u_2} {α : Type u_3} [ α] {m : measurable_space α} {μ : measure_theory.measure α} (c : ℝ≥0∞) :
(c μ)
@[protected, instance]
def measure_theory.vadd_invariant_measure.vadd_nnreal {M : Type u_2} {α : Type u_3} [ α] {m : measurable_space α} {μ : measure_theory.measure α} (c : ℝ≥0) :
(c μ)
@[protected, instance]
def measure_theory.smul_invariant_measure.smul_nnreal {M : Type u_2} {α : Type u_3} [ α] {m : measurable_space α} {μ : measure_theory.measure α} (c : ℝ≥0) :
(c μ)
theorem measure_theory.smul_invariant_measure_tfae (G : Type u_1) {α : Type u_3} {m : measurable_space α} [group G] [ α] [ α] (μ : measure_theory.measure α) :
, ∀ (c : G) (s : set α), μ ⁻¹' s) = μ s, ∀ (c : G) (s : set α), μ (c s) = μ s, ∀ (c : G) (s : set α), μ ⁻¹' s) = μ s, ∀ (c : G) (s : set α), μ (c s) = μ s, ∀ (c : G), , ∀ (c : G), .tfae

Equivalent definitions of a measure invariant under a multiplicative action of a group.

• 0: smul_invariant_measure 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.

theorem measure_theory.vadd_invariant_measure_tfae (G : Type u_1) {α : Type u_3} {m : measurable_space α} [add_group G] [ α] [ α] (μ : measure_theory.measure α) :
, ∀ (c : G) (s : set α), μ ⁻¹' s) = μ s, ∀ (c : G) (s : set α), μ (c +ᵥ s) = μ s, ∀ (c : G) (s : set α), μ ⁻¹' s) = μ s, ∀ (c : G) (s : set α), μ (c +ᵥ s) = μ s, ∀ (c : G), , ∀ (c : G), .tfae

Equivalent definitions of a measure invariant under an additive action of a group.

• 0: vadd_invariant_measure 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 measure_theory.measure_preserving_vadd {G : Type u_1} {α : Type u_3} {m : measurable_space α} [add_group G] [ α] [ α] (c : G) (μ : measure_theory.measure α)  :
theorem measure_theory.measure_preserving_smul {G : Type u_1} {α : Type u_3} {m : measurable_space α} [group G] [ α] [ α] (c : G) (μ : measure_theory.measure α)  :
@[simp]
theorem measure_theory.map_vadd {G : Type u_1} {α : Type u_3} {m : measurable_space α} [add_group G] [ α] [ α] (c : G) (μ : measure_theory.measure α)  :
@[simp]
theorem measure_theory.map_smul {G : Type u_1} {α : Type u_3} {m : measurable_space α} [group G] [ α] [ α] (c : G) (μ : measure_theory.measure α)  :
@[simp]
theorem measure_theory.measure_preimage_vadd {G : Type u_1} {α : Type u_3} {m : measurable_space α} [add_group G] [ α] [ α] (c : G) (μ : measure_theory.measure α) (s : set α) :
μ ⁻¹' s) = μ s
@[simp]
theorem measure_theory.measure_preimage_smul {G : Type u_1} {α : Type u_3} {m : measurable_space α} [group G] [ α] [ α] (c : G) (μ : measure_theory.measure α) (s : set α) :
μ ⁻¹' s) = μ s
@[simp]
theorem measure_theory.measure_vadd_set {G : Type u_1} {α : Type u_3} {m : measurable_space α} [add_group G] [ α] [ α] (c : G) (μ : measure_theory.measure α) (s : set α) :
μ (c +ᵥ s) = μ s
@[simp]
theorem measure_theory.measure_smul_set {G : Type u_1} {α : Type u_3} {m : measurable_space α} [group G] [ α] [ α] (c : G) (μ : measure_theory.measure α) (s : set α) :
μ (c s) = μ s
theorem measure_theory.measure_is_open_pos_of_vadd_invariant_of_compact_ne_zero (G : Type u_1) {α : Type u_3} {m : measurable_space α} [add_group G] [ α] [ α] {μ : measure_theory.measure α} [ α] {K U : set α} (hK : is_compact K) (hμK : μ K 0) (hU : is_open U) (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 measure_theory.measure_is_open_pos_of_vadd_invariant_of_ne_zero.

theorem measure_theory.measure_is_open_pos_of_smul_invariant_of_compact_ne_zero (G : Type u_1) {α : Type u_3} {m : measurable_space α} [group G] [ α] [ α] {μ : measure_theory.measure α} [ α] {K U : set α} (hK : is_compact K) (hμK : μ K 0) (hU : is_open U) (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 measure_theory.measure_is_open_pos_of_smul_invariant_of_ne_zero.

theorem measure_theory.is_locally_finite_measure_of_vadd_invariant (G : Type u_1) {α : Type u_3} {m : measurable_space α} [add_group G] [ α] [ α] {μ : measure_theory.measure α} [ α] {U : set α} (hU : is_open U) (hne : U.nonempty) (hμU : μ U ) :
theorem measure_theory.is_locally_finite_measure_of_smul_invariant (G : Type u_1) {α : Type u_3} {m : measurable_space α} [group G] [ α] [ α] {μ : measure_theory.measure α} [ α] {U : set α} (hU : is_open U) (hne : U.nonempty) (hμU : μ U ) :
theorem measure_theory.measure_is_open_pos_of_smul_invariant_of_ne_zero (G : Type u_1) {α : Type u_3} {m : measurable_space α} [group G] [ α] [ α] {μ : measure_theory.measure α} [ α] {U : set α} [μ.regular] (hμ : μ 0) (hU : is_open U) (hne : U.nonempty) :
0 < μ U
theorem measure_theory.measure_is_open_pos_of_vadd_invariant_of_ne_zero (G : Type u_1) {α : Type u_3} {m : measurable_space α} [add_group G] [ α] [ α] {μ : measure_theory.measure α} [ α] {U : set α} [μ.regular] (hμ : μ 0) (hU : is_open U) (hne : U.nonempty) :
0 < μ U
theorem measure_theory.measure_pos_iff_nonempty_of_smul_invariant (G : Type u_1) {α : Type u_3} {m : measurable_space α} [group G] [ α] [ α] {μ : measure_theory.measure α} [ α] {U : set α} [μ.regular] (hμ : μ 0) (hU : is_open U) :
0 < μ U U.nonempty
theorem measure_theory.measure_pos_iff_nonempty_of_vadd_invariant (G : Type u_1) {α : Type u_3} {m : measurable_space α} [add_group G] [ α] [ α] {μ : measure_theory.measure α} [ α] {U : set α} [μ.regular] (hμ : μ 0) (hU : is_open U) :
0 < μ U U.nonempty
theorem measure_theory.measure_eq_zero_iff_eq_empty_of_vadd_invariant (G : Type u_1) {α : Type u_3} {m : measurable_space α} [add_group G] [ α] [ α] {μ : measure_theory.measure α} [ α] {U : set α} [μ.regular] (hμ : μ 0) (hU : is_open U) :
μ U = 0 U =
theorem measure_theory.measure_eq_zero_iff_eq_empty_of_smul_invariant (G : Type u_1) {α : Type u_3} {m : measurable_space α} [group G] [ α] [ α] {μ : measure_theory.measure α} [ α] {U : set α} [μ.regular] (hμ : μ 0) (hU : is_open U) :
μ U = 0 U =