mathlib documentation

measure_theory.group.measure

Measures on Groups #

We develop some properties of measures on (topological) groups

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

@[class]

A measure μ on a measurable additive group is right invariant if the measure of right translations of a set are equal to the measure of the set itself.

Instances of this typeclass
@[class]

A measure μ on a measurable group is right invariant if the measure of right translations of a set are equal to the measure of the set itself.

Instances of this typeclass
theorem measure_theory.map_add_right_eq_self {G : Type u_1} [measurable_space G] [has_add G] (μ : measure_theory.measure G) [μ.is_add_right_invariant] (g : G) :
measure_theory.measure.map (λ (_x : G), _x + g) μ = μ
theorem measure_theory.map_mul_right_eq_self {G : Type u_1} [measurable_space G] [has_mul G] (μ : measure_theory.measure G) [μ.is_mul_right_invariant] (g : G) :
measure_theory.measure.map (λ (_x : G), _x * g) μ = μ
theorem measure_theory.forall_measure_preimage_add_iff {G : Type u_1} [measurable_space G] [has_add G] [has_measurable_add G] (μ : measure_theory.measure G) :
(∀ (g : G) (A : set G), measurable_set Aμ ((λ (h : G), g + h) ⁻¹' A) = μ A) μ.is_add_left_invariant

An alternative way to prove that μ is left invariant under addition.

theorem measure_theory.forall_measure_preimage_mul_iff {G : Type u_1} [measurable_space G] [has_mul G] [has_measurable_mul G] (μ : measure_theory.measure G) :
(∀ (g : G) (A : set G), measurable_set Aμ ((λ (h : G), g * h) ⁻¹' A) = μ A) μ.is_mul_left_invariant

An alternative way to prove that μ is left invariant under multiplication.

theorem measure_theory.forall_measure_preimage_mul_right_iff {G : Type u_1} [measurable_space G] [has_mul G] [has_measurable_mul G] (μ : measure_theory.measure G) :
(∀ (g : G) (A : set G), measurable_set Aμ ((λ (h : G), h * g) ⁻¹' A) = μ A) μ.is_mul_right_invariant

An alternative way to prove that μ is right invariant under multiplication.

theorem measure_theory.forall_measure_preimage_add_right_iff {G : Type u_1} [measurable_space G] [has_add G] [has_measurable_add G] (μ : measure_theory.measure G) :
(∀ (g : G) (A : set G), measurable_set Aμ ((λ (h : G), h + g) ⁻¹' A) = μ A) μ.is_add_right_invariant

An alternative way to prove that μ is right invariant under addition.

theorem measure_theory.map_div_right_eq_self {G : Type u_1} [measurable_space G] [group G] (μ : measure_theory.measure G) [μ.is_mul_right_invariant] (g : G) :
measure_theory.measure.map (λ (_x : G), _x / g) μ = μ
@[simp]
theorem measure_theory.measure_preimage_add {G : Type u_1} [measurable_space G] [add_group G] [has_measurable_add G] (μ : measure_theory.measure G) [μ.is_add_left_invariant] (g : G) (A : set G) :
μ ((λ (h : G), g + h) ⁻¹' A) = μ A

We shorten this from measure_preimage_add_left, since left invariant is the preferred option for measures in this formalization.

@[simp]
theorem measure_theory.measure_preimage_mul {G : Type u_1} [measurable_space G] [group G] [has_measurable_mul G] (μ : measure_theory.measure G) [μ.is_mul_left_invariant] (g : G) (A : set G) :
μ ((λ (h : G), g * h) ⁻¹' A) = μ A

We shorten this from measure_preimage_mul_left, since left invariant is the preferred option for measures in this formalization.

@[simp]
theorem measure_theory.measure_preimage_add_right {G : Type u_1} [measurable_space G] [add_group G] [has_measurable_add G] (μ : measure_theory.measure G) [μ.is_add_right_invariant] (g : G) (A : set G) :
μ ((λ (h : G), h + g) ⁻¹' A) = μ A
@[simp]
theorem measure_theory.measure_preimage_mul_right {G : Type u_1} [measurable_space G] [group G] [has_measurable_mul G] (μ : measure_theory.measure G) [μ.is_mul_right_invariant] (g : G) (A : set G) :
μ ((λ (h : G), h * g) ⁻¹' A) = μ A
theorem measure_theory.map_mul_left_ae {G : Type u_1} [measurable_space G] [group G] [has_measurable_mul G] (μ : measure_theory.measure G) [μ.is_mul_left_invariant] (x : G) :
filter.map (λ (h : G), x * h) μ.ae = μ.ae
theorem measure_theory.map_add_left_ae {G : Type u_1} [measurable_space G] [add_group G] [has_measurable_add G] (μ : measure_theory.measure G) [μ.is_add_left_invariant] (x : G) :
filter.map (λ (h : G), x + h) μ.ae = μ.ae
theorem measure_theory.map_mul_right_ae {G : Type u_1} [measurable_space G] [group G] [has_measurable_mul G] (μ : measure_theory.measure G) [μ.is_mul_right_invariant] (x : G) :
filter.map (λ (h : G), h * x) μ.ae = μ.ae
theorem measure_theory.map_add_right_ae {G : Type u_1} [measurable_space G] [add_group G] [has_measurable_add G] (μ : measure_theory.measure G) [μ.is_add_right_invariant] (x : G) :
filter.map (λ (h : G), h + x) μ.ae = μ.ae
theorem measure_theory.map_sub_right_ae {G : Type u_1} [measurable_space G] [add_group G] [has_measurable_add G] (μ : measure_theory.measure G) [μ.is_add_right_invariant] (x : G) :
filter.map (λ (t : G), t - x) μ.ae = μ.ae
theorem measure_theory.map_div_right_ae {G : Type u_1} [measurable_space G] [group G] [has_measurable_mul G] (μ : measure_theory.measure G) [μ.is_mul_right_invariant] (x : G) :
filter.map (λ (t : G), t / x) μ.ae = μ.ae
@[class]
  • neg_eq_self : μ.neg = μ

A measure is invariant under negation if - μ = μ. Equivalently, this means that for all measurable A we have μ (- A) = μ A, where - A is the pointwise negation of A.

Instances of this typeclass
@[class]
  • inv_eq_self : μ.inv = μ

A measure is invariant under inversion if μ⁻¹ = μ. Equivalently, this means that for all measurable A we have μ (A⁻¹) = μ A, where A⁻¹ is the pointwise inverse of A.

Instances of this typeclass
@[simp]
@[simp]
@[simp]
@[protected, simp]
@[protected, simp]

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

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.

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

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

@[protected, instance]

In an abelian additive group every left invariant measure is also right-invariant. We don't declare the converse as an instance, since that would loop type-class inference, and we use is_add_left_invariant as default hypotheses in abelian groups.

@[protected, instance]

In an abelian group every left invariant measure is also right-invariant. We don't declare the converse as an instance, since that would loop type-class inference, and we use is_mul_left_invariant as default hypotheses in abelian groups.

@[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 of this typeclass
@[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 of this typeclass
@[protected, instance]

Record that a Haar measure on a locally compact space is locally finite. This is needed as the fact that a measure which is finite on compacts is locally finite is not registered as an instance, to avoid an instance loop.

See Note [lower instance priority].

@[protected, instance]

Record that an additive Haar measure on a locally compact space is locally finite. This is needed as the fact that a measure which is finite on compacts is locally finite is not registered as an instance, to avoid an instance loop.

See Note [lower instance priority]

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

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

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

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

@[protected, instance]

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

See Note [lower instance priority]

@[protected, instance]

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

The additive version of this instance applies in particular to show that an additive Haar measure on a nontrivial finite-dimensional real vector space has no atom.

@[protected, instance]

If the zero element of an additive group is not isolated, then an additive Haar measure on this group has no atoms.

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