mathlib documentation

measure_theory.group

Measures on Groups

We develop some properties of measures on (topological) groups

def measure_theory.is_mul_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 the measure of left translations of a set are equal to the measure of the set itself. To left translate sets we use preimage under left multiplication, since preimages are nicer to work with than images.

Equations
def measure_theory.is_add_left_invariant {G : Type u_1} [measurable_space G] [has_add G] (μ : set Gennreal) :
Prop

A measure on a topological group is left invariant if the measure of left translations of a set are equal to the measure of the set itself. To left translate sets we use preimage under left addition, since preimages are nicer to work with than images.

def measure_theory.is_add_right_invariant {G : Type u_1} [measurable_space G] [has_add G] (μ : set Gennreal) :
Prop

A measure on a topological group is right invariant if the measure of right translations of a set are equal to the measure of the set itself. To right translate sets we use preimage under right addition, since preimages are nicer to work with than images.

def measure_theory.is_mul_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 the measure of right translations of a set are equal to the measure of the set itself. To right translate sets we use preimage under right multiplication, since preimages are nicer to work with than images.

Equations

The measure A ↦ μ (A⁻¹), where A⁻¹ is the pointwise inverse of A.

Equations

The measure A ↦ μ (- A), where - A is the pointwise negation of A.

Properties of regular left invariant measures

theorem measure_theory.lintegral_eq_zero_of_is_mul_left_invariant {G : Type u_1} [measurable_space G] [topological_space G] [borel_space G] {μ : measure_theory.measure G} [group G] [topological_group G] (hμ : μ.regular) (h2μ : measure_theory.is_mul_left_invariant μ) (h3μ : μ 0) {f : G → ennreal} (hf : continuous f) :
∫⁻ (x : G), f x μ = 0 f = 0

For nonzero regular left invariant measures, the integral of a continuous nonnegative function f is 0 iff f is 0.