# mathlibdocumentation

measure_theory.group.basic

# Measures on Groups #

We develop some properties of measures on (topological) groups

• We define properties on measures: left and right invariant measures.
• We define the measure μ.inv : A ↦ μ(A⁻¹) and show that it is right invariant iff μ is left invariant.
• We define a class is_haar_measure μ, requiring that the measure μ is left-invariant, finite on compact sets, and positive on open sets.

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

def measure_theory.is_mul_left_invariant {G : Type u_1} [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
• = ∀ (g : G) {A : set G}, μ ((λ (h : G), g * h) ⁻¹' A) = μ A
def measure_theory.is_add_left_invariant {G : Type u_1} [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
• = ∀ (g : G) {A : set G}, μ ((λ (h : G), g + h) ⁻¹' A) = μ A
def measure_theory.is_add_right_invariant {G : Type u_1} [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
• = ∀ (g : G) {A : set G}, μ ((λ (h : G), h + g) ⁻¹' A) = μ A
def measure_theory.is_mul_right_invariant {G : Type u_1} [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
• = ∀ (g : G) {A : set G}, μ ((λ (h : G), h * g) ⁻¹' A) = μ A
theorem measure_theory.measure.map_add_left_eq_self {G : Type u_1} [has_add G] [borel_space G] {μ : measure_theory.measure G} :
(∀ (g : G), = μ)
theorem measure_theory.measure.map_mul_left_eq_self {G : Type u_1} [has_mul G] [borel_space G] {μ : measure_theory.measure G} :
(∀ (g : G), = μ)
theorem measure_theory.is_mul_left_invariant.measure_preimage_mul {G : Type u_1} [group G] [borel_space G] {μ : measure_theory.measure G} (g : G) (A : set G) :
μ ((λ (h : G), g * h) ⁻¹' A) = μ A
theorem measure_theory.is_add_left_invariant.measure_preimage_add {G : Type u_1} [add_group G] [borel_space G] {μ : measure_theory.measure G} (g : G) (A : set G) :
μ ((λ (h : G), g + h) ⁻¹' A) = μ A
theorem measure_theory.measure.map_add_right_eq_self {G : Type u_1} [has_add G] [borel_space G] {μ : measure_theory.measure G} :
(∀ (g : G), (measure_theory.measure.map (λ (h : G), h + g)) μ = μ)
theorem measure_theory.measure.map_mul_right_eq_self {G : Type u_1} [has_mul G] [borel_space G] {μ : measure_theory.measure G} :
(∀ (g : G), (measure_theory.measure.map (λ (h : G), h * g)) μ = μ)
@[protected]
noncomputable def measure_theory.measure.inv {G : Type u_1} [has_inv G] (μ : measure_theory.measure G) :

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

Equations
@[protected]
noncomputable def measure_theory.measure.neg {G : Type u_1} [has_neg G] (μ : measure_theory.measure G) :

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

Equations
theorem measure_theory.measure.neg_apply {G : Type u_1} [add_group G] [borel_space G] (μ : measure_theory.measure G) (s : set G) :
(μ.neg) s = μ (-s)
theorem measure_theory.measure.inv_apply {G : Type u_1} [group G] [borel_space G] (μ : measure_theory.measure G) (s : set G) :
(μ.inv) s = μ s⁻¹
@[protected, simp]
theorem measure_theory.measure.inv_inv {G : Type u_1} [group G] [borel_space G] (μ : measure_theory.measure G) :
μ.inv.inv = μ
@[protected, simp]
theorem measure_theory.measure.neg_neg {G : Type u_1} [add_group G] [borel_space G] (μ : measure_theory.measure G) :
μ.neg.neg = μ
@[protected, instance]
@[protected, instance]
@[simp]
@[simp]
@[simp]
@[simp]
theorem measure_theory.is_add_left_invariant.measure_pos_of_is_open {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [add_group G] (K : set G) (hK : is_compact K) (h : μ K 0) {U : set G} (hU : is_open U) (h'U : U.nonempty) :
0 < μ U
theorem measure_theory.is_mul_left_invariant.measure_pos_of_is_open {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [group G] (K : set G) (hK : is_compact K) (h : μ K 0) {U : set G} (hU : is_open U) (h'U : U.nonempty) :
0 < μ U

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.

theorem measure_theory.is_add_left_invariant.null_iff_empty {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [add_group G] [μ.regular] (h3μ : μ 0) {s : set G} (hs : is_open s) :
μ s = 0 s =
theorem measure_theory.is_mul_left_invariant.null_iff_empty {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [group G] [μ.regular] (h3μ : μ 0) {s : set G} (hs : is_open s) :
μ s = 0 s =
theorem measure_theory.is_mul_left_invariant.null_iff {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [group G] [μ.regular] {s : set G} (hs : is_open s) :
μ s = 0 s = μ = 0
theorem measure_theory.is_add_left_invariant.null_iff {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [add_group G] [μ.regular] {s : set G} (hs : is_open s) :
μ s = 0 s = μ = 0
theorem measure_theory.is_add_left_invariant.measure_ne_zero_iff_nonempty {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [add_group G] [μ.regular] (h3μ : μ 0) {s : set G} (hs : is_open s) :
theorem measure_theory.is_mul_left_invariant.measure_ne_zero_iff_nonempty {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [group G] [μ.regular] (h3μ : μ 0) {s : set G} (hs : is_open s) :
theorem measure_theory.is_mul_left_invariant.measure_pos_iff_nonempty {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [group G] [μ.regular] (h3μ : μ 0) {s : set G} (hs : is_open s) :
0 < μ s s.nonempty
theorem measure_theory.is_add_left_invariant.measure_pos_iff_nonempty {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [add_group G] [μ.regular] (h3μ : μ 0) {s : set G} (hs : is_open s) :
0 < μ s s.nonempty
theorem measure_theory.is_add_left_invariant.measure_lt_top_of_is_compact {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [add_group G] (U : set G) (hU : is_open U) (h'U : U.nonempty) (h : μ U ) {K : set G} (hK : is_compact K) :
μ K <
theorem measure_theory.is_mul_left_invariant.measure_lt_top_of_is_compact {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [group G] (U : set G) (hU : is_open U) (h'U : U.nonempty) (h : μ U ) {K : set G} (hK : is_compact K) :
μ K <

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

theorem measure_theory.is_add_left_invariant.measure_lt_top_of_is_compact' {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [add_group G] (U : set G) (hU : (interior U).nonempty) (h : μ U ) {K : set G} (hK : is_compact K) :
μ K <
theorem measure_theory.is_mul_left_invariant.measure_lt_top_of_is_compact' {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [group G] (U : set G) (hU : (interior U).nonempty) (h : μ U ) {K : set G} (hK : is_compact K) :
μ K <

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

theorem measure_theory.lintegral_eq_zero_of_is_add_left_invariant {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [add_group G] [μ.regular] (h3μ : μ 0) {f : G → ℝ≥0∞} (hf : continuous f) :
∫⁻ (x : G), f x μ = 0 f = 0
theorem measure_theory.lintegral_eq_zero_of_is_mul_left_invariant {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [group G] [μ.regular] (h3μ : μ 0) {f : G → ℝ≥0∞} (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.

theorem measure_theory.lintegral_mul_left_eq_self {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [group G] (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.

theorem measure_theory.lintegral_add_left_eq_self {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [add_group G] (f : G → ℝ≥0∞) (g : G) :
∫⁻ (x : G), f (g + x) μ = ∫⁻ (x : G), f x μ
theorem measure_theory.lintegral_add_right_eq_self {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [add_group G] (f : G → ℝ≥0∞) (g : G) :
∫⁻ (x : G), f (x + g) μ = ∫⁻ (x : G), f x μ
theorem measure_theory.lintegral_mul_right_eq_self {G : Type u_1} [borel_space G] {μ : measure_theory.measure G} [group G] (f : G → ℝ≥0∞) (g : G) :
∫⁻ (x : G), f (x * g) μ = ∫⁻ (x : G), f x μ

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

@[class]
structure measure_theory.measure.is_haar_measure {G : Type u_2} [group G] (μ : measure_theory.measure G) :
Prop
• to_is_finite_measure_on_compacts :
• left_invariant :
• open_pos : ∀ (U : set G), U.nonempty0 < μ U

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]
structure measure_theory.measure.is_add_haar_measure {G : Type u_2} [add_group G] (μ : measure_theory.measure G) :
Prop
• to_is_finite_measure_on_compacts :
• open_pos : ∀ (U : set G), U.nonempty0 < μ U

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
@[protected, instance]
@[protected, instance]
theorem is_open.add_haar_pos {G : Type u_1} [add_group G] (μ : measure_theory.measure G) {U : set G} (hU : is_open U) (h'U : U.nonempty) :
0 < μ U
theorem is_open.haar_pos {G : Type u_1} [group 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] (μ : measure_theory.measure G) [μ.is_haar_measure] [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] (μ : measure_theory.measure G) [borel_space G] (g : G) (A : set G) :
μ ((λ (h : G), g + h) ⁻¹' A) = μ A
@[simp]
theorem measure_theory.measure.haar_singleton {G : Type u_1} [group G] (μ : measure_theory.measure G) [μ.is_haar_measure] [borel_space G] (g : G) :
μ {g} = μ {1}
@[simp]
theorem measure_theory.measure.add_haar_singleton {G : Type u_1} [add_group G] (μ : measure_theory.measure G) [borel_space G] (g : G) :
μ {g} = μ {0}
@[simp]
theorem measure_theory.measure.haar_preimage_mul_right {G : Type u_1} [comm_group G] (μ : measure_theory.measure G) [μ.is_haar_measure] [borel_space G] (g : G) (A : set G) :
μ ((λ (h : G), h * g) ⁻¹' A) = μ A
@[simp]
theorem measure_theory.measure.add_haar_preimage_add_right {G : Type u_1} (μ : measure_theory.measure G) [borel_space G] (g : G) (A : set G) :
μ ((λ (h : G), h + g) ⁻¹' A) = μ A
theorem measure_theory.measure.is_haar_measure.smul {G : Type u_1} [group G] (μ : measure_theory.measure G) [μ.is_haar_measure] {c : ℝ≥0∞} (cpos : c 0) (ctop : c ) :
theorem measure_theory.measure.is_add_haar_measure.smul {G : Type u_1} [add_group G] (μ : measure_theory.measure G) {c : ℝ≥0∞} (cpos : c 0) (ctop : c ) :
theorem measure_theory.measure.is_haar_measure_of_is_compact_nonempty_interior {G : Type u_1} [group G] [borel_space G] (μ : measure_theory.measure G) (K : set G) (hK : is_compact K) (h'K : (interior K).nonempty) (h : μ K 0) (h' : μ K ) :

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

theorem measure_theory.measure.is_haar_measure_map {G : Type u_1} [group G] (μ : measure_theory.measure G) [μ.is_haar_measure] [borel_space G] {H : Type u_2} [group H] [borel_space H] [t2_space H] (f : G ≃* H) (hf : continuous f) (hfsymm : continuous (f.symm)) :

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

theorem measure_theory.measure.is_add_haar_measure_map {G : Type u_1} [add_group G] (μ : measure_theory.measure G) [borel_space G] {H : Type u_2} [add_group H] [borel_space H] [t2_space H] (f : G ≃+ H) (hf : continuous f) (hfsymm : continuous (f.symm)) :
@[protected, instance]

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

@[protected, instance]
@[protected, 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.

@[protected, instance]