mathlib documentation

measure_theory.group.basic

Measures on Groups #

We develop some properties of measures on (topological) groups

We also give analogues of all these notions in the additive world.

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.

Equations
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.

Equations
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.

Equations

If a left-invariant measure gives positive mass to a compact set, then it gives positive mass to any open set.

A nonzero left-invariant regular measure gives positive mass to any open set.

If a left-invariant measure gives finite mass to a nonempty open set, then it gives finite mass to any compact set.

If a left-invariant measure gives finite mass to a set with nonempty interior, then it gives finite mass to any compact set.

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.

@[class]

A measure on a group is a Haar measure if it is left-invariant, and gives finite mass to compact sets and positive mass to open sets.

Instances
@[class]

A measure on an additive group is an additive Haar measure if it is left-invariant, and gives finite mass to compact sets and positive mass to open sets.

Instances
theorem is_compact.haar_lt_top {G : Type u_1} [group G] [measurable_space G] [topological_space G] (μ : measure_theory.measure G) [μ.is_haar_measure] {K : set G} (hK : is_compact K) :
μ K <
theorem is_open.add_haar_pos {G : Type u_1} [add_group G] [measurable_space G] [topological_space G] (μ : measure_theory.measure G) [μ.is_add_haar_measure] {U : set G} (hU : is_open U) (h'U : U.nonempty) :
0 < μ U
theorem is_open.haar_pos {G : Type u_1} [group G] [measurable_space G] [topological_space G] (μ : measure_theory.measure G) [μ.is_haar_measure] {U : set G} (hU : is_open U) (h'U : U.nonempty) :
0 < μ U
@[simp]
theorem measure_theory.measure.haar_preimage_mul {G : Type u_1} [group G] [measurable_space G] [topological_space G] (μ : measure_theory.measure G) [μ.is_haar_measure] [topological_group G] [borel_space G] (g : G) (A : set G) :
μ ((λ (h : G), g * h) ⁻¹' A) = μ A
@[simp]
theorem measure_theory.measure.add_haar_preimage_add {G : Type u_1} [add_group G] [measurable_space G] [topological_space G] (μ : measure_theory.measure G) [μ.is_add_haar_measure] [topological_add_group G] [borel_space G] (g : G) (A : set G) :
μ ((λ (h : G), g + h) ⁻¹' A) = μ A
@[simp]
theorem measure_theory.measure.haar_preimage_mul_right {G : Type u_1} [comm_group G] [measurable_space G] [topological_space G] (μ : measure_theory.measure G) [μ.is_haar_measure] [topological_group G] [borel_space G] (g : G) (A : set G) :
μ ((λ (h : G), h * g) ⁻¹' A) = μ A

If a left-invariant measure gives positive mass to some compact set with nonempty interior, then it is a Haar measure

The image of a Haar measure under a group homomorphism which is also a homeomorphism is again a Haar measure.

@[instance]

A Haar measure on a sigma-compact space is sigma-finite.

@[instance]

If the neutral element of a group is not isolated, then a Haar measure on this group has no atom.

This applies in particular to show that an additive Haar measure on a nontrivial finite-dimensional real vector space has no atom.