# mathlibdocumentation

measure_theory.group

# 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} [has_mul G] :
(set Gennreal) → 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
• = ∀ (g : G) {A : set G}, μ ((λ (h : G), g * h) ⁻¹' A) = μ A
def measure_theory.is_right_invariant {G : Type u_1} [has_mul G] :
(set Gennreal) → 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
• = ∀ (g : G) {A : set G}, μ ((λ (h : G), h * g) ⁻¹' A) = μ A
theorem measure_theory.measure.map_mul_left_eq_self {G : Type u_1} [has_mul G] [borel_space G] {μ : measure_theory.measure G} :
(∀ (g : G), = μ)

theorem measure_theory.measure.map_mul_right_eq_self {G : Type u_1} [has_mul G] [borel_space G] {μ : measure_theory.measure G} :
(∀ (g : G), (measure_theory.measure.map (λ (h : G), h * g)) μ = μ)

def measure_theory.measure.conj {G : Type u_1} [group 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} [group G] [borel_space G] (μ : measure_theory.measure G) {s : set G} :
(μ.conj) s = μ s⁻¹

@[simp]
theorem measure_theory.measure.conj_conj {G : Type u_1} [group G] [borel_space G] (μ : measure_theory.measure G) :
μ.conj.conj = μ

@[simp]

@[simp]

@[simp]