mathlib3 documentation

measure_theory.group.action

Measures invariant under group actions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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) [has_vadd M α] {_x : measurable_space α} (μ : measure_theory.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 λ x, c +ᵥ x is equal to the measure of s.

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

Instances of this typeclass
@[protected, instance]
@[protected, instance]
theorem measure_theory.smul_invariant_measure_tfae (G : Type u_1) {α : Type u_3} {m : measurable_space α} [group G] [mul_action G α] [measurable_space G] [has_measurable_smul G α] (μ : measure_theory.measure α) :
[measure_theory.smul_invariant_measure G α μ, (c : G) (s : set α), measurable_set s μ (has_smul.smul c ⁻¹' s) = μ s, (c : G) (s : set α), measurable_set s μ (c s) = μ s, (c : G) (s : set α), μ (has_smul.smul c ⁻¹' s) = μ s, (c : G) (s : set α), μ (c s) = μ s, (c : G), measure_theory.measure.map (has_smul.smul c) μ = μ, (c : G), measure_theory.measure_preserving (has_smul.smul c) μ μ].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] [add_action G α] [measurable_space G] [has_measurable_vadd G α] (μ : measure_theory.measure α) :
[measure_theory.vadd_invariant_measure G α μ, (c : G) (s : set α), measurable_set s μ (has_vadd.vadd c ⁻¹' s) = μ s, (c : G) (s : set α), measurable_set s μ (c +ᵥ s) = μ s, (c : G) (s : set α), μ (has_vadd.vadd c ⁻¹' s) = μ s, (c : G) (s : set α), μ (c +ᵥ s) = μ s, (c : G), measure_theory.measure.map (has_vadd.vadd c) μ = μ, (c : G), measure_theory.measure_preserving (has_vadd.vadd c) μ μ].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.

@[simp]
@[simp]
theorem measure_theory.measure_smul {G : Type u_1} {α : Type u_3} {m : measurable_space α} [group G] [mul_action G α] [measurable_space G] [has_measurable_smul G α] (c : G) (μ : measure_theory.measure α) [measure_theory.smul_invariant_measure G α μ] (s : set α) :
μ (c s) = μ s
@[simp]
theorem measure_theory.measure_vadd {G : Type u_1} {α : Type u_3} {m : measurable_space α} [add_group G] [add_action G α] [measurable_space G] [has_measurable_vadd G α] (c : G) (μ : measure_theory.measure α) [measure_theory.vadd_invariant_measure G α μ] (s : set α) :
μ (c +ᵥ s) = μ s
theorem measure_theory.measure_smul_null {G : Type u_1} {α : Type u_3} {m : measurable_space α} [group G] [mul_action G α] [measurable_space G] [has_measurable_smul G α] {μ : measure_theory.measure α} [measure_theory.smul_invariant_measure G α μ] {s : set α} (h : μ s = 0) (c : G) :
μ (c s) = 0

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.

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.smul_ae_eq_self_of_mem_zpowers {G : Type u_1} {α : Type u_3} {s : set α} {m : measurable_space α} [group G] [mul_action G α] [measurable_space G] [has_measurable_smul G α] {μ : measure_theory.measure α} [measure_theory.smul_invariant_measure G α μ] {x y : G} (hs : x s =ᵐ[μ] s) (hy : y subgroup.zpowers x) :
y s =ᵐ[μ] s