mathlib documentation

measure_theory.group

Measures on Groups

We develop some properties of measures on (topological) groups

def measure_theory.is_left_invariant {G : Type u_1} [measurable_space G] [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
def measure_theory.is_right_invariant {G : Type u_1} [measurable_space G] [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

The conjugate of a measure on a topological group. Defined to be A ↦ μ (A⁻¹), where A⁻¹ is the pointwise inverse of A.

Equations