Measures on Groups
We develop some properties of measures on (topological) groups
- We define properties on measures: left and right invariant measures
- We define the conjugate
A ↦ μ (A⁻¹)of a measureμ, and show that it is right invariant iffμis left invariant
def
measure_theory.is_left_invariant
{G : Type u_1}
[measurable_space G]
[has_mul G]
(μ : set G → ennreal) :
Prop
A measure μ on a topological group is left invariant if
for all measurable sets s and all g, we have μ (gs) = μ s,
where gs denotes the translate of s by left multiplication with g.
Equations
- measure_theory.is_left_invariant μ = ∀ (g : G) {A : set G}, is_measurable A → μ ((λ (h : G), g * h) ⁻¹' A) = μ A
def
measure_theory.is_right_invariant
{G : Type u_1}
[measurable_space G]
[has_mul G]
(μ : set G → ennreal) :
Prop
A measure μ on a topological group is right invariant if
for all measurable sets s and all g, we have μ (sg) = μ s,
where sg denotes the translate of s by right multiplication with g.
Equations
- measure_theory.is_right_invariant μ = ∀ (g : G) {A : set G}, is_measurable A → μ ((λ (h : G), h * g) ⁻¹' A) = μ A
theorem
measure_theory.measure.map_mul_left_eq_self
{G : Type u_1}
[measurable_space G]
[topological_space G]
[has_mul G]
[has_continuous_mul G]
[borel_space G]
{μ : measure_theory.measure G} :
(∀ (g : G), ⇑(measure_theory.measure.map (has_mul.mul g)) μ = μ) ↔ measure_theory.is_left_invariant ⇑μ
theorem
measure_theory.measure.map_mul_right_eq_self
{G : Type u_1}
[measurable_space G]
[topological_space G]
[has_mul G]
[has_continuous_mul G]
[borel_space G]
{μ : measure_theory.measure G} :
(∀ (g : G), ⇑(measure_theory.measure.map (λ (h : G), h * g)) μ = μ) ↔ measure_theory.is_right_invariant ⇑μ
def
measure_theory.measure.conj
{G : Type u_1}
[measurable_space G]
[group G]
(μ : measure_theory.measure G) :
The conjugate of a measure on a topological group.
Defined to be A ↦ μ (A⁻¹), where A⁻¹ is the pointwise inverse of A.
Equations
theorem
measure_theory.measure.conj_apply
{G : Type u_1}
[measurable_space G]
[group G]
[topological_space G]
[topological_group G]
[borel_space G]
(μ : measure_theory.measure G)
{s : set G}
(hs : is_measurable s) :
@[simp]
theorem
measure_theory.measure.conj_conj
{G : Type u_1}
[measurable_space G]
[group G]
[topological_space G]
[topological_group G]
[borel_space G]
(μ : measure_theory.measure G) :
theorem
measure_theory.measure.regular.conj
{G : Type u_1}
[measurable_space G]
[group G]
[topological_space G]
[topological_group G]
[borel_space G]
{μ : measure_theory.measure G}
[t2_space G]
(hμ : μ.regular) :
@[simp]
theorem
measure_theory.regular_conj_iff
{G : Type u_1}
[measurable_space G]
[group G]
[topological_space G]
[topological_group G]
[borel_space G]
{μ : measure_theory.measure G}
[t2_space G] :
theorem
measure_theory.is_right_invariant_conj'
{G : Type u_1}
[measurable_space G]
[group G]
[topological_space G]
[topological_group G]
[borel_space G]
{μ : measure_theory.measure G}
(h : measure_theory.is_left_invariant ⇑μ) :
theorem
measure_theory.is_left_invariant_conj'
{G : Type u_1}
[measurable_space G]
[group G]
[topological_space G]
[topological_group G]
[borel_space G]
{μ : measure_theory.measure G}
(h : measure_theory.is_right_invariant ⇑μ) :
@[simp]
theorem
measure_theory.is_right_invariant_conj
{G : Type u_1}
[measurable_space G]
[group G]
[topological_space G]
[topological_group G]
[borel_space G]
{μ : measure_theory.measure G} :
@[simp]
theorem
measure_theory.is_left_invariant_conj
{G : Type u_1}
[measurable_space G]
[group G]
[topological_space G]
[topological_group G]
[borel_space G]
{μ : measure_theory.measure G} :