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 Gℝ≥0∞) :
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 Gℝ≥0∞) :
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 Gℝ≥0∞) :
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 Gℝ≥0∞) :
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

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

theorem measure_theory.lintegral_mul_left_eq_self {G : Type u_1} [measurable_space G] [topological_space G] [borel_space G] {μ : measure_theory.measure G} [group G] [has_continuous_mul G] (hμ : measure_theory.is_mul_left_invariant μ) (f : G → ℝ≥0∞) (g : G) :
∫⁻ (x : G), f (g * x) μ = ∫⁻ (x : G), f x μ

Translating a function by left-multiplication does not change its lintegral with respect to a left-invariant measure.

Translating a function by right-multiplication does not change its lintegral with respect to a right-invariant measure.