# mathlibdocumentation

measure_theory.prod_group

# Measure theory in the product of groups #

In this file we show properties about measure theory in products of topological groups and properties of iterated integrals in topological groups.

These lemmas show the uniqueness of left invariant measures on locally compact groups, up to scaling. In this file we follow the proof and refer to the book Measure Theory by Paul Halmos.

The idea of the proof is to use the translation invariance of measures to prove μ(F) = c * μ(E) for two sets E and F, where c is a constant that does not depend on μ. Let e and f be the characteristic functions of E and F. Assume that μ and ν are left-invariant measures. Then the map (x, y) ↦ (y * x, x⁻¹) preserves the measure μ.prod ν, which means that

  ∫ x, ∫ y, h x y ∂ν ∂μ = ∫ x, ∫ y, h (y * x) x⁻¹ ∂ν ∂μ


If we apply this to h x y := e x * f y⁻¹ / ν ((λ h, h * y⁻¹) ⁻¹' E), we can rewrite the RHS to μ(F), and the LHS to c * μ(E), where c = c(ν) does not depend on μ. Applying this to μ and to ν gives μ (F) / μ (E) = ν (F) / ν (E), which is the uniqueness up to scalar multiplication.

The proof in [Halmos] seems to contain an omission in §60 Th. A, see measure_theory.measure_lintegral_div_measure and https://math.stackexchange.com/questions/3974485/does-right-translation-preserve-finiteness-for-a-left-invariant-measure

theorem measure_theory.map_prod_sum_eq {G : Type u_1} [borel_space G] [add_group G] {μ ν : measure_theory.measure G}  :
(measure_theory.measure.map (λ (z : G × G), (z.fst, z.fst + z.snd))) (μ.prod ν) = μ.prod ν
theorem measure_theory.map_prod_mul_eq {G : Type u_1} [borel_space G] [group G] {μ ν : measure_theory.measure G}  :
(measure_theory.measure.map (λ (z : G × G), (z.fst, (z.fst) * z.snd))) (μ.prod ν) = μ.prod ν

This condition is part of the definition of a measurable group in [Halmos, §59]. There, the map in this lemma is called S.

theorem measure_theory.map_prod_add_eq_swap {G : Type u_1} [borel_space G] [add_group G] {μ ν : measure_theory.measure G}  :
(measure_theory.measure.map (λ (z : G × G), (z.snd, z.snd + z.fst))) (μ.prod ν) = ν.prod μ
theorem measure_theory.map_prod_mul_eq_swap {G : Type u_1} [borel_space G] [group G] {μ ν : measure_theory.measure G}  :
(measure_theory.measure.map (λ (z : G × G), (z.snd, (z.snd) * z.fst))) (μ.prod ν) = ν.prod μ

The function we are mapping along is SR in [Halmos, §59], where S is the map in map_prod_mul_eq and R is prod.swap.

theorem measure_theory.map_prod_neg_add_eq {G : Type u_1} [borel_space G] [add_group G] {μ ν : measure_theory.measure G}  :
(measure_theory.measure.map (λ (z : G × G), (z.fst, -z.fst + z.snd))) (μ.prod ν) = μ.prod ν
theorem measure_theory.map_prod_inv_mul_eq {G : Type u_1} [borel_space G] [group G] {μ ν : measure_theory.measure G}  :
(measure_theory.measure.map (λ (z : G × G), (z.fst, (z.fst)⁻¹ * z.snd))) (μ.prod ν) = μ.prod ν

The function we are mapping along is S⁻¹ in [Halmos, §59], where S is the map in map_prod_mul_eq.

theorem measure_theory.map_prod_inv_mul_eq_swap {G : Type u_1} [borel_space G] [group G] {μ ν : measure_theory.measure G}  :
(measure_theory.measure.map (λ (z : G × G), (z.snd, (z.snd)⁻¹ * z.fst))) (μ.prod ν) = ν.prod μ

The function we are mapping along is S⁻¹R in [Halmos, §59], where S is the map in map_prod_mul_eq and R is prod.swap.

theorem measure_theory.map_prod_neg_add_eq_swap {G : Type u_1} [borel_space G] [add_group G] {μ ν : measure_theory.measure G}  :
(measure_theory.measure.map (λ (z : G × G), (z.snd, -z.snd + z.fst))) (μ.prod ν) = ν.prod μ
theorem measure_theory.map_prod_mul_inv_eq {G : Type u_1} [borel_space G] [group G] {μ ν : measure_theory.measure G}  :
(measure_theory.measure.map (λ (z : G × G), ((z.snd) * z.fst, (z.fst)⁻¹))) (μ.prod ν) = μ.prod ν

The function we are mapping along is S⁻¹RSR in [Halmos, §59], where S is the map in map_prod_mul_eq and R is prod.swap.

theorem measure_theory.map_prod_add_neg_eq {G : Type u_1} [borel_space G] [add_group G] {μ ν : measure_theory.measure G}  :
(measure_theory.measure.map (λ (z : G × G), (z.snd + z.fst, -z.fst))) (μ.prod ν) = μ.prod ν
theorem measure_theory.measure_null_of_measure_inv_null {G : Type u_1} [borel_space G] [group G] {μ : measure_theory.measure G} {E : set G} (hE : measurable_set E) (h2E : μ ((λ (x : G), x⁻¹) ⁻¹' E) = 0) :
μ E = 0
theorem measure_theory.measure_null_of_measure_neg_null {G : Type u_1} [borel_space G] [add_group G] {μ : measure_theory.measure G} {E : set G} (hE : measurable_set E) (h2E : μ ((λ (x : G), -x) ⁻¹' E) = 0) :
μ E = 0
theorem measure_theory.measure_neg_null {G : Type u_1} [borel_space G] [add_group G] {μ : measure_theory.measure G} {E : set G} (hE : measurable_set E) :
μ ((λ (x : G), -x) ⁻¹' E) = 0 μ E = 0
theorem measure_theory.measure_inv_null {G : Type u_1} [borel_space G] [group G] {μ : measure_theory.measure G} {E : set G} (hE : measurable_set E) :
μ ((λ (x : G), x⁻¹) ⁻¹' E) = 0 μ E = 0
theorem measure_theory.measurable_measure_add_right {G : Type u_1} [borel_space G] [add_group G] {μ : measure_theory.measure G} {E : set G} (hE : measurable_set E) :
measurable (λ (x : G), μ ((λ (y : G), y + x) ⁻¹' E))
theorem measure_theory.measurable_measure_mul_right {G : Type u_1} [borel_space G] [group G] {μ : measure_theory.measure G} {E : set G} (hE : measurable_set E) :
measurable (λ (x : G), μ ((λ (y : G), y * x) ⁻¹' E))
theorem measure_theory.lintegral_lintegral_mul_inv {G : Type u_1} [borel_space G] [group G] {μ ν : measure_theory.measure G} (f : G → G → ℝ≥0∞) (hf : (μ.prod ν)) :
∫⁻ (x : G), ∫⁻ (y : G), f (y * x) x⁻¹ ν μ = ∫⁻ (x : G), ∫⁻ (y : G), f x y ν μ
theorem measure_theory.lintegral_lintegral_add_neg {G : Type u_1} [borel_space G] [add_group G] {μ ν : measure_theory.measure G} (f : G → G → ℝ≥0∞) (hf : (μ.prod ν)) :
∫⁻ (x : G), ∫⁻ (y : G), f (y + x) (-x) ν μ = ∫⁻ (x : G), ∫⁻ (y : G), f x y ν μ
theorem measure_theory.measure_mul_right_null {G : Type u_1} [borel_space G] [group G] {μ : measure_theory.measure G} {E : set G} (hE : measurable_set E) (y : G) :
μ ((λ (x : G), x * y) ⁻¹' E) = 0 μ E = 0
theorem measure_theory.measure_add_right_null {G : Type u_1} [borel_space G] [add_group G] {μ : measure_theory.measure G} {E : set G} (hE : measurable_set E) (y : G) :
μ ((λ (x : G), x + y) ⁻¹' E) = 0 μ E = 0
theorem measure_theory.measure_add_right_ne_zero {G : Type u_1} [borel_space G] [add_group G] {μ : measure_theory.measure G} {E : set G} (hE : measurable_set E) (h2E : μ E 0) (y : G) :
μ ((λ (x : G), x + y) ⁻¹' E) 0
theorem measure_theory.measure_mul_right_ne_zero {G : Type u_1} [borel_space G] [group G] {μ : measure_theory.measure G} {E : set G} (hE : measurable_set E) (h2E : μ E 0) (y : G) :
μ ((λ (x : G), x * y) ⁻¹' E) 0
theorem measure_theory.measure_lintegral_div_measure {G : Type u_1} [borel_space G] [group G] {μ ν : measure_theory.measure G} [t2_space G] [ν.regular] {E : set G} (hE : is_compact E) (h2E : ν E 0) (f : G → ℝ≥0∞) (hf : measurable f) :
(μ E) * ∫⁻ (y : G), f y⁻¹ / ν ((λ (h : G), h * y⁻¹) ⁻¹' E) ν = ∫⁻ (x : G), f x μ

A technical lemma relating two different measures. This is basically [Halmos, §60 Th. A]. Note that if f is the characteristic function of a measurable set F this states that μ F = c * μ E for a constant c that does not depend on μ. There seems to be a gap in the last step of the proof in [Halmos]. In the last line, the equality g(x⁻¹)ν(Ex⁻¹) = f(x) holds if we can prove that 0 < ν(Ex⁻¹) < ∞. The first inequality follows from §59, Th. D, but I couldn't find the second inequality. For this reason, we use a compact E instead of a measurable E as in [Halmos], and additionally assume that ν is a regular measure (we only need that it is finite on compact sets).

theorem measure_theory.measure_lintegral_sub_measure {G : Type u_1} [borel_space G] [add_group G] {μ ν : measure_theory.measure G} [t2_space G] [ν.regular] {E : set G} (hE : is_compact E) (h2E : ν E 0) (f : G → ℝ≥0∞) (hf : measurable f) :
(μ E) * ∫⁻ (y : G), f (-y) / ν ((λ (h : G), h + -y) ⁻¹' E) ν = ∫⁻ (x : G), f x μ
theorem measure_theory.measure_mul_measure_eq {G : Type u_1} [borel_space G] [group G] {μ ν : measure_theory.measure G} [t2_space G] [ν.regular] {E F : set G} (hE : is_compact E) (hF : measurable_set F) (h2E : ν E 0) :
(μ E) * ν F = (ν E) * μ F

This is roughly the uniqueness (up to a scalar) of left invariant Borel measures on a second countable locally compact group. The uniqueness of Haar measure is proven from this in measure_theory.measure.haar_measure_unique

theorem measure_theory.measure_add_measure_eq {G : Type u_1} [borel_space G] [add_group G] {μ ν : measure_theory.measure G} [t2_space G] [ν.regular] {E F : set G} (hE : is_compact E) (hF : measurable_set F) (h2E : ν E 0) :
(μ E) * ν F = (ν E) * μ F