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
- measure_preimage_vadd : ∀ (c : M) ⦃s : set α⦄, measurable_set s → ⇑μ ((λ (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 of this typeclass
- measure_theory.vadd_invariant_measure.zero
- measure_theory.vadd_invariant_measure.add
- measure_theory.vadd_invariant_measure.vadd
- measure_theory.vadd_invariant_measure.vadd_nnreal
- measure_theory.is_mul_left_invariant.vadd_invariant_measure
- measure_theory.is_mul_right_invariant.to_vadd_invariant_measure_op
- measure_theory.subgroup.vadd_invariant_measure
@[class]
structure
measure_theory.smul_invariant_measure
(M : Type u_4)
(α : Type u_5)
[has_smul M α]
{_x : measurable_space α}
(μ : measure_theory.measure α) :
Prop
- measure_preimage_smul : ∀ (c : M) ⦃s : set α⦄, measurable_set s → ⇑μ ((λ (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 of this typeclass
- measure_theory.smul_invariant_measure.zero
- measure_theory.smul_invariant_measure.add
- measure_theory.smul_invariant_measure.smul
- measure_theory.smul_invariant_measure.smul_nnreal
- measure_theory.is_mul_left_invariant.smul_invariant_measure
- measure_theory.is_mul_right_invariant.to_smul_invariant_measure_op
- measure_theory.subgroup.smul_invariant_measure
@[protected, instance]
def
measure_theory.vadd_invariant_measure.zero
{M : Type u_2}
{α : Type u_3}
[measurable_space α]
[has_vadd M α] :
@[protected, instance]
def
measure_theory.smul_invariant_measure.zero
{M : Type u_2}
{α : Type u_3}
[measurable_space α]
[has_smul M α] :
@[protected, instance]
def
measure_theory.smul_invariant_measure.add
{M : Type u_2}
{α : Type u_3}
[has_smul M α]
{m : measurable_space α}
{μ ν : measure_theory.measure α}
[measure_theory.smul_invariant_measure M α μ]
[measure_theory.smul_invariant_measure M α ν] :
measure_theory.smul_invariant_measure M α (μ + ν)
@[protected, instance]
def
measure_theory.vadd_invariant_measure.add
{M : Type u_2}
{α : Type u_3}
[has_vadd M α]
{m : measurable_space α}
{μ ν : measure_theory.measure α}
[measure_theory.vadd_invariant_measure M α μ]
[measure_theory.vadd_invariant_measure M α ν] :
measure_theory.vadd_invariant_measure M α (μ + ν)
@[protected, instance]
def
measure_theory.vadd_invariant_measure.vadd
{M : Type u_2}
{α : Type u_3}
[has_vadd M α]
{m : measurable_space α}
{μ : measure_theory.measure α}
[measure_theory.vadd_invariant_measure M α μ]
(c : ennreal) :
measure_theory.vadd_invariant_measure M α (c • μ)
@[protected, instance]
def
measure_theory.smul_invariant_measure.smul
{M : Type u_2}
{α : Type u_3}
[has_smul M α]
{m : measurable_space α}
{μ : measure_theory.measure α}
[measure_theory.smul_invariant_measure M α μ]
(c : ennreal) :
measure_theory.smul_invariant_measure M α (c • μ)
@[protected, instance]
def
measure_theory.vadd_invariant_measure.vadd_nnreal
{M : Type u_2}
{α : Type u_3}
[has_vadd M α]
{m : measurable_space α}
{μ : measure_theory.measure α}
[measure_theory.vadd_invariant_measure M α μ]
(c : nnreal) :
measure_theory.vadd_invariant_measure M α (c • μ)
@[protected, instance]
def
measure_theory.smul_invariant_measure.smul_nnreal
{M : Type u_2}
{α : Type u_3}
[has_smul M α]
{m : measurable_space α}
{μ : measure_theory.measure α}
[measure_theory.smul_invariant_measure M α μ]
(c : nnreal) :
measure_theory.smul_invariant_measure M α (c • μ)
@[simp]
theorem
measure_theory.measure_preserving_vadd
{M : Type u_2}
{α : Type u_3}
{m : measurable_space α}
[measurable_space M]
[has_vadd M α]
[has_measurable_vadd M α]
(c : M)
(μ : measure_theory.measure α)
[measure_theory.vadd_invariant_measure M α μ] :
@[simp]
theorem
measure_theory.measure_preserving_smul
{M : Type u_2}
{α : Type u_3}
{m : measurable_space α}
[measurable_space M]
[has_smul M α]
[has_measurable_smul M α]
(c : M)
(μ : measure_theory.measure α)
[measure_theory.smul_invariant_measure M α μ] :
@[simp]
theorem
measure_theory.map_vadd
{M : Type u_2}
{α : Type u_3}
{m : measurable_space α}
[measurable_space M]
[has_vadd M α]
[has_measurable_vadd M α]
(c : M)
(μ : measure_theory.measure α)
[measure_theory.vadd_invariant_measure M α μ] :
measure_theory.measure.map (has_vadd.vadd c) μ = μ
@[simp]
theorem
measure_theory.map_smul
{M : Type u_2}
{α : Type u_3}
{m : measurable_space α}
[measurable_space M]
[has_smul M α]
[has_measurable_smul M α]
(c : M)
(μ : measure_theory.measure α)
[measure_theory.smul_invariant_measure M α μ] :
measure_theory.measure.map (has_smul.smul c) μ = μ
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 : Gand a measurable sets, the measure of the preimage ofsunder scalar multiplication bycis equal to the measure ofs; -
2: for every
c : Gand a measurable sets, the measure of the imagec • sofsunder scalar multiplication bycis equal to the measure ofs; -
3, 4: properties 2, 3 for any set, including non-measurable ones;
-
5: for any
c : G, scalar multiplication bycmapsμtoμ; -
6: for any
c : G, scalar multiplication bycis 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 : Gand a measurable sets, the measure of the preimage ofsunder vector addition(+ᵥ) cis equal to the measure ofs; -
2: for every
c : Gand a measurable sets, the measure of the imagec +ᵥ sofsunder vector addition(+ᵥ) cis equal to the measure ofs; -
3, 4: properties 2, 3 for any set, including non-measurable ones;
-
5: for any
c : G, vector addition ofcmapsμtoμ; -
6: for any
c : G, vector addition ofcis a measure preserving map.
@[simp]
theorem
measure_theory.measure_preimage_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 α) :
⇑μ (has_vadd.vadd c ⁻¹' s) = ⇑μ s
@[simp]
theorem
measure_theory.measure_preimage_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 α) :
⇑μ (has_smul.smul c ⁻¹' s) = ⇑μ s
@[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 α) :
@[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 α) :
theorem
measure_theory.null_measurable_set.vadd
{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 α μ]
{s : set α}
(hs : measure_theory.null_measurable_set s μ)
(c : G) :
measure_theory.null_measurable_set (c +ᵥ s) μ
theorem
measure_theory.null_measurable_set.smul
{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 α}
(hs : measure_theory.null_measurable_set s μ)
(c : G) :
measure_theory.null_measurable_set (c • 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) :
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]
[add_action G α]
[measurable_space G]
[has_measurable_vadd G α]
{μ : measure_theory.measure α}
[measure_theory.vadd_invariant_measure G α μ]
[topological_space α]
[has_continuous_const_vadd G α]
[add_action.is_minimal G α]
{K U : set α}
(hK : is_compact K)
(hμK : ⇑μ K ≠ 0)
(hU : is_open U)
(hne : U.nonempty) :
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]
[mul_action G α]
[measurable_space G]
[has_measurable_smul G α]
{μ : measure_theory.measure α}
[measure_theory.smul_invariant_measure G α μ]
[topological_space α]
[has_continuous_const_smul G α]
[mul_action.is_minimal G α]
{K U : set α}
(hK : is_compact K)
(hμK : ⇑μ K ≠ 0)
(hU : is_open U)
(hne : U.nonempty) :
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]
[add_action G α]
[measurable_space G]
[has_measurable_vadd G α]
{μ : measure_theory.measure α}
[measure_theory.vadd_invariant_measure G α μ]
[topological_space α]
[has_continuous_const_vadd G α]
[add_action.is_minimal G α]
{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]
[mul_action G α]
[measurable_space G]
[has_measurable_smul G α]
{μ : measure_theory.measure α}
[measure_theory.smul_invariant_measure G α μ]
[topological_space α]
[has_continuous_const_smul G α]
[mul_action.is_minimal G α]
{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]
[mul_action G α]
[measurable_space G]
[has_measurable_smul G α]
{μ : measure_theory.measure α}
[measure_theory.smul_invariant_measure G α μ]
[topological_space α]
[has_continuous_const_smul G α]
[mul_action.is_minimal G α]
{U : set α}
[μ.regular]
(hμ : μ ≠ 0)
(hU : is_open U)
(hne : U.nonempty) :
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]
[add_action G α]
[measurable_space G]
[has_measurable_vadd G α]
{μ : measure_theory.measure α}
[measure_theory.vadd_invariant_measure G α μ]
[topological_space α]
[has_continuous_const_vadd G α]
[add_action.is_minimal G α]
{U : set α}
[μ.regular]
(hμ : μ ≠ 0)
(hU : is_open U)
(hne : U.nonempty) :
theorem
measure_theory.measure_pos_iff_nonempty_of_smul_invariant
(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 α μ]
[topological_space α]
[has_continuous_const_smul G α]
[mul_action.is_minimal G α]
{U : set α}
[μ.regular]
(hμ : μ ≠ 0)
(hU : is_open U) :
theorem
measure_theory.measure_pos_iff_nonempty_of_vadd_invariant
(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 α μ]
[topological_space α]
[has_continuous_const_vadd G α]
[add_action.is_minimal G α]
{U : set α}
[μ.regular]
(hμ : μ ≠ 0)
(hU : is_open U) :
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]
[add_action G α]
[measurable_space G]
[has_measurable_vadd G α]
{μ : measure_theory.measure α}
[measure_theory.vadd_invariant_measure G α μ]
[topological_space α]
[has_continuous_const_vadd G α]
[add_action.is_minimal G α]
{U : set α}
[μ.regular]
(hμ : μ ≠ 0)
(hU : is_open 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]
[mul_action G α]
[measurable_space G]
[has_measurable_smul G α]
{μ : measure_theory.measure α}
[measure_theory.smul_invariant_measure G α μ]
[topological_space α]
[has_continuous_const_smul G α]
[mul_action.is_minimal G α]
{U : set α}
[μ.regular]
(hμ : μ ≠ 0)
(hU : is_open U) :
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) :
theorem
measure_theory.vadd_ae_eq_self_of_mem_zmultiples
{α : Type u_3}
{s : set α}
{m : measurable_space α}
{μ : measure_theory.measure α}
{G : Type u_1}
[measurable_space G]
[add_group G]
[add_action G α]
[measure_theory.vadd_invariant_measure G α μ]
[has_measurable_vadd G α]
{x y : G}
(hs : x +ᵥ s =ᵐ[μ] s)
(hy : y ∈ add_subgroup.zmultiples x) :