Measure theory in the product of groups

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

These lemmas show the uniqueness of left invariant measures on measurable 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 μ(t) = c * μ(s) for two sets s and t, where c is a constant that does not depend on μ. Let e and f be the characteristic functions of s and t. Assume that μ and ν are left-invariant measures. Then the map (x, y) ↦ (y * x, x⁻¹) preserves the measure μ × ν, 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⁻¹ / ν ((fun h ↦ h * y⁻¹) ⁻¹' s), we can rewrite the RHS to μ(t), and the LHS to c * μ(s), where c = c(ν) does not depend on μ. Applying this to μ and to ν gives μ (t) / μ (s) = ν (t) / ν (s), which is the uniqueness up to scalar multiplication.

The proof in [Halmos] seems to contain an omission in §60 Th. A, see MeasureTheory.measure_lintegral_div_measure.

Note that this theory only applies in measurable groups, i.e., when multiplication and inversion are measurable. This is not the case in general in locally compact groups, or even in compact groups, when the topology is not second-countable. For arguments along the same line, but using continuous functions instead of measurable sets and working in the general locally compact setting, see the file MeasureTheory.Measure.Haar.Unique.lean.

theorem MeasurableEquiv.shearAddRight.proof_1 (G : Type u_1) [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] : Measurable fun (a : G × G) => (a.1, (Equiv.addLeft a.1) a.2)

def MeasurableEquiv.shearAddRight (G : Type u_1) [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] : G × G ≃ᵐ G × G

The map (x, y) ↦ (x, x + y) as a MeasurableEquiv.

Equations

• MeasurableEquiv.shearAddRight G = let __src := (Equiv.refl G).prodShear Equiv.addLeft; { toEquiv := __src, measurable_toFun := ⋯, measurable_invFun := ⋯ }

theorem MeasurableEquiv.shearAddRight.proof_2 (G : Type u_1) [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] : Measurable fun (a : G × G) => (a.1, (Equiv.symm (Equiv.addLeft ((Equiv.refl G).symm a.1))) a.2)

def MeasurableEquiv.shearMulRight (G : Type u_1) [MeasurableSpace G] [Group G] [MeasurableMul₂ G] [MeasurableInv G] : G × G ≃ᵐ G × G

The map (x, y) ↦ (x, xy) as a MeasurableEquiv.

Equations

• MeasurableEquiv.shearMulRight G = let __src := (Equiv.refl G).prodShear Equiv.mulLeft; { toEquiv := __src, measurable_toFun := ⋯, measurable_invFun := ⋯ }

theorem MeasurableEquiv.shearSubRight.proof_2 (G : Type u_1) [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] : Measurable fun (a : G × G) => (a.1, (Equiv.subRight ((Equiv.refl G).symm a.1)).symm a.2)

theorem MeasurableEquiv.shearSubRight.proof_1 (G : Type u_1) [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] : Measurable fun (a : G × G) => (a.1, (Equiv.subRight a.1) a.2)

def MeasurableEquiv.shearSubRight (G : Type u_1) [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] : G × G ≃ᵐ G × G

The map (x, y) ↦ (x, y - x) as a MeasurableEquiv with as inverse (x, y) ↦ (x, y + x).

Equations

• MeasurableEquiv.shearSubRight G = let __src := (Equiv.refl G).prodShear Equiv.subRight; { toEquiv := __src, measurable_toFun := ⋯, measurable_invFun := ⋯ }

def MeasurableEquiv.shearDivRight (G : Type u_1) [MeasurableSpace G] [Group G] [MeasurableMul₂ G] [MeasurableInv G] : G × G ≃ᵐ G × G

The map (x, y) ↦ (x, y / x) as a MeasurableEquiv with as inverse (x, y) ↦ (x, yx)

Equations

• MeasurableEquiv.shearDivRight G = let __src := (Equiv.refl G).prodShear Equiv.divRight; { toEquiv := __src, measurable_toFun := ⋯, measurable_invFun := ⋯ }

theorem MeasureTheory.measurePreserving_prod_add {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [ν.IsAddLeftInvariant] : MeasureTheory.MeasurePreserving (fun (z : G × G) => (z.1, z.1 + z.2)) (μ.prod ν) (μ.prod ν)

The shear mapping (x, y) ↦ (x, x + y) preserves the measure μ × ν.

theorem MeasureTheory.measurePreserving_prod_mul {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [ν.IsMulLeftInvariant] : MeasureTheory.MeasurePreserving (fun (z : G × G) => (z.1, z.1 * z.2)) (μ.prod ν) (μ.prod ν)

The multiplicative shear mapping (x, y) ↦ (x, xy) preserves the measure μ × ν. This condition is part of the definition of a measurable group in [Halmos, §59]. There, the map in this lemma is called S.

theorem MeasureTheory.measurePreserving_prod_add_swap {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [μ.IsAddLeftInvariant] : MeasureTheory.MeasurePreserving (fun (z : G × G) => (z.2, z.2 + z.1)) (μ.prod ν) (ν.prod μ)

The map (x, y) ↦ (y, y + x) sends the measure μ × ν to ν × μ.

theorem MeasureTheory.measurePreserving_prod_mul_swap {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [μ.IsMulLeftInvariant] : MeasureTheory.MeasurePreserving (fun (z : G × G) => (z.2, z.2 * z.1)) (μ.prod ν) (ν.prod μ)

The map (x, y) ↦ (y, yx) sends the measure μ × ν to ν × μ. This is the map SR in [Halmos, §59]. S is the map (x, y) ↦ (x, xy) and R is Prod.swap.

theorem MeasureTheory.measurable_measure_add_right {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] {s : Set G} (hs : MeasurableSet s) : Measurable fun (x : G) => μ ((fun (y : G) => y + x) ⁻¹' s)

theorem MeasureTheory.measurable_measure_mul_right {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] {s : Set G} (hs : MeasurableSet s) : Measurable fun (x : G) => μ ((fun (y : G) => y * x) ⁻¹' s)

theorem MeasureTheory.measurePreserving_prod_neg_add {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableNeg G] [ν.IsAddLeftInvariant] : MeasureTheory.MeasurePreserving (fun (z : G × G) => (z.1, -z.1 + z.2)) (μ.prod ν) (μ.prod ν)

The map (x, y) ↦ (x, - x + y) is measure-preserving.

theorem MeasureTheory.measurePreserving_prod_inv_mul {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableInv G] [ν.IsMulLeftInvariant] : MeasureTheory.MeasurePreserving (fun (z : G × G) => (z.1, z.1⁻¹ * z.2)) (μ.prod ν) (μ.prod ν)

The map (x, y) ↦ (x, x⁻¹y) is measure-preserving. This is the function S⁻¹ in [Halmos, §59], where S is the map (x, y) ↦ (x, xy).

theorem MeasureTheory.measurePreserving_prod_neg_add_swap {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant] : MeasureTheory.MeasurePreserving (fun (z : G × G) => (z.2, -z.2 + z.1)) (μ.prod ν) (ν.prod μ)

The map (x, y) ↦ (y, - y + x) sends μ × ν to ν × μ.

theorem MeasureTheory.measurePreserving_prod_inv_mul_swap {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant] : MeasureTheory.MeasurePreserving (fun (z : G × G) => (z.2, z.2⁻¹ * z.1)) (μ.prod ν) (ν.prod μ)

The map (x, y) ↦ (y, y⁻¹x) sends μ × ν to ν × μ. This is the function S⁻¹R in [Halmos, §59], where S is the map (x, y) ↦ (x, xy) and R is Prod.swap.

theorem MeasureTheory.measurePreserving_add_prod_neg {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant] [ν.IsAddLeftInvariant] : MeasureTheory.MeasurePreserving (fun (z : G × G) => (z.2 + z.1, -z.1)) (μ.prod ν) (μ.prod ν)

The map (x, y) ↦ (y + x, - x) is measure-preserving.

theorem MeasureTheory.measurePreserving_mul_prod_inv {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant] [ν.IsMulLeftInvariant] : MeasureTheory.MeasurePreserving (fun (z : G × G) => (z.2 * z.1, z.1⁻¹)) (μ.prod ν) (μ.prod ν)

The map (x, y) ↦ (yx, x⁻¹) is measure-preserving. This is the function S⁻¹RSR in [Halmos, §59], where S is the map (x, y) ↦ (x, xy) and R is Prod.swap.

theorem MeasureTheory.quasiMeasurePreserving_neg {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant] : MeasureTheory.Measure.QuasiMeasurePreserving Neg.neg μ μ

theorem MeasureTheory.quasiMeasurePreserving_inv {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant] : MeasureTheory.Measure.QuasiMeasurePreserving Inv.inv μ μ

@[simp]

theorem MeasureTheory.measure_neg_null {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] {s : Set G} [MeasurableNeg G] [μ.IsAddLeftInvariant] : μ (-s) = 0 ↔ μ s = 0

@[simp]

theorem MeasureTheory.measure_inv_null {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] {s : Set G} [MeasurableInv G] [μ.IsMulLeftInvariant] : μ s⁻¹ = 0 ↔ μ s = 0

@[simp]

theorem MeasureTheory.neg_ae {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant] : -MeasureTheory.ae μ = MeasureTheory.ae μ

@[simp]

theorem MeasureTheory.inv_ae {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant] : (MeasureTheory.ae μ)⁻¹ = MeasureTheory.ae μ

@[simp]

theorem MeasureTheory.eventuallyConst_neg_set_ae {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] {s : Set G} [MeasurableNeg G] [μ.IsAddLeftInvariant] : Filter.EventuallyConst (-s) (MeasureTheory.ae μ) ↔ Filter.EventuallyConst s (MeasureTheory.ae μ)

@[simp]

theorem MeasureTheory.eventuallyConst_inv_set_ae {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] {s : Set G} [MeasurableInv G] [μ.IsMulLeftInvariant] : Filter.EventuallyConst s⁻¹ (MeasureTheory.ae μ) ↔ Filter.EventuallyConst s (MeasureTheory.ae μ)

theorem MeasureTheory.neg_absolutelyContinuous {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant] : μ.neg.AbsolutelyContinuous μ

theorem MeasureTheory.inv_absolutelyContinuous {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant] : μ.inv.AbsolutelyContinuous μ

theorem MeasureTheory.absolutelyContinuous_neg {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant] : μ.AbsolutelyContinuous μ.neg

theorem MeasureTheory.absolutelyContinuous_inv {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant] : μ.AbsolutelyContinuous μ.inv

theorem MeasureTheory.lintegral_lintegral_add_neg {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant] [ν.IsAddLeftInvariant] (f : G → G → ENNReal) (hf : AEMeasurable (Function.uncurry f) (μ.prod ν)) : ∫⁻ (x : G), ∫⁻ (y : G), f (y + x) (-x) ∂ν ∂μ = ∫⁻ (x : G), ∫⁻ (y : G), f x y ∂ν ∂μ

theorem MeasureTheory.lintegral_lintegral_mul_inv {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant] [ν.IsMulLeftInvariant] (f : G → G → ENNReal) (hf : AEMeasurable (Function.uncurry f) (μ.prod ν)) : ∫⁻ (x : G), ∫⁻ (y : G), f (y * x) x⁻¹ ∂ν ∂μ = ∫⁻ (x : G), ∫⁻ (y : G), f x y ∂ν ∂μ

theorem MeasureTheory.measure_add_right_null {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] {s : Set G} [MeasurableNeg G] [μ.IsAddLeftInvariant] (y : G) : μ ((fun (x : G) => x + y) ⁻¹' s) = 0 ↔ μ s = 0

theorem MeasureTheory.measure_mul_right_null {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] {s : Set G} [MeasurableInv G] [μ.IsMulLeftInvariant] (y : G) : μ ((fun (x : G) => x * y) ⁻¹' s) = 0 ↔ μ s = 0

theorem MeasureTheory.measure_add_right_ne_zero {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] {s : Set G} [MeasurableNeg G] [μ.IsAddLeftInvariant] (h2s : μ s ≠ 0) (y : G) : μ ((fun (x : G) => x + y) ⁻¹' s) ≠ 0

theorem MeasureTheory.measure_mul_right_ne_zero {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] {s : Set G} [MeasurableInv G] [μ.IsMulLeftInvariant] (h2s : μ s ≠ 0) (y : G) : μ ((fun (x : G) => x * y) ⁻¹' s) ≠ 0

theorem MeasureTheory.absolutelyContinuous_map_add_right {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant] (g : G) : μ.AbsolutelyContinuous (MeasureTheory.Measure.map (fun (x : G) => x + g) μ)

theorem MeasureTheory.absolutelyContinuous_map_mul_right {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant] (g : G) : μ.AbsolutelyContinuous (MeasureTheory.Measure.map (fun (x : G) => x * g) μ)

theorem MeasureTheory.absolutelyContinuous_map_sub_left {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant] (g : G) : μ.AbsolutelyContinuous (MeasureTheory.Measure.map (fun (h : G) => g - h) μ)

theorem MeasureTheory.absolutelyContinuous_map_div_left {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant] (g : G) : μ.AbsolutelyContinuous (MeasureTheory.Measure.map (fun (h : G) => g / h) μ)

theorem MeasureTheory.measure_add_lintegral_eq {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {s : Set G} [MeasurableNeg G] [μ.IsAddLeftInvariant] [ν.IsAddLeftInvariant] (sm : MeasurableSet s) (f : G → ENNReal) (hf : Measurable f) : μ s * ∫⁻ (y : G), f y ∂ν = ∫⁻ (x : G), ν ((fun (z : G) => z + x) ⁻¹' s) * f (-x) ∂μ

This is the computation performed in the proof of [Halmos, §60 Th. A].

theorem MeasureTheory.measure_mul_lintegral_eq {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {s : Set G} [MeasurableInv G] [μ.IsMulLeftInvariant] [ν.IsMulLeftInvariant] (sm : MeasurableSet s) (f : G → ENNReal) (hf : Measurable f) : μ s * ∫⁻ (y : G), f y ∂ν = ∫⁻ (x : G), ν ((fun (z : G) => z * x) ⁻¹' s) * f x⁻¹ ∂μ

This is the computation performed in the proof of [Halmos, §60 Th. A].

theorem MeasureTheory.absolutelyContinuous_of_isAddLeftInvariant {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant] [ν.IsAddLeftInvariant] (hν : ν ≠ 0) : μ.AbsolutelyContinuous ν

Any two nonzero left-invariant measures are absolutely continuous w.r.t. each other.

theorem MeasureTheory.absolutelyContinuous_of_isMulLeftInvariant {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant] [ν.IsMulLeftInvariant] (hν : ν ≠ 0) : μ.AbsolutelyContinuous ν

Any two nonzero left-invariant measures are absolutely continuous w.r.t. each other.

theorem MeasureTheory.ae_measure_preimage_add_right_lt_top {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] {s : Set G} [MeasurableNeg G] (μ' : MeasureTheory.Measure G) (ν' : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ'] [MeasureTheory.SigmaFinite ν'] [μ'.IsAddLeftInvariant] [ν'.IsAddLeftInvariant] (hμs : μ' s ≠ ⊤) : ∀ᵐ (x : G) ∂μ', ν' ((fun (x_1 : G) => x_1 + x) ⁻¹' s) < ⊤

theorem MeasureTheory.ae_measure_preimage_mul_right_lt_top {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] {s : Set G} [MeasurableInv G] (μ' : MeasureTheory.Measure G) (ν' : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ'] [MeasureTheory.SigmaFinite ν'] [μ'.IsMulLeftInvariant] [ν'.IsMulLeftInvariant] (hμs : μ' s ≠ ⊤) : ∀ᵐ (x : G) ∂μ', ν' ((fun (x_1 : G) => x_1 * x) ⁻¹' s) < ⊤

theorem MeasureTheory.ae_measure_preimage_add_right_lt_top_of_ne_zero {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] {s : Set G} [MeasurableNeg G] (μ' : MeasureTheory.Measure G) (ν' : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ'] [MeasureTheory.SigmaFinite ν'] [μ'.IsAddLeftInvariant] [ν'.IsAddLeftInvariant] (h2s : ν' s ≠ 0) (h3s : ν' s ≠ ⊤) : ∀ᵐ (x : G) ∂μ', ν' ((fun (y : G) => y + x) ⁻¹' s) < ⊤

theorem MeasureTheory.ae_measure_preimage_mul_right_lt_top_of_ne_zero {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] {s : Set G} [MeasurableInv G] (μ' : MeasureTheory.Measure G) (ν' : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ'] [MeasureTheory.SigmaFinite ν'] [μ'.IsMulLeftInvariant] [ν'.IsMulLeftInvariant] (h2s : ν' s ≠ 0) (h3s : ν' s ≠ ⊤) : ∀ᵐ (x : G) ∂μ', ν' ((fun (y : G) => y * x) ⁻¹' s) < ⊤

theorem MeasureTheory.measure_lintegral_sub_measure {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] {s : Set G} [MeasurableNeg G] (μ' : MeasureTheory.Measure G) (ν' : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ'] [MeasureTheory.SigmaFinite ν'] [μ'.IsAddLeftInvariant] [ν'.IsAddLeftInvariant] (sm : MeasurableSet s) (h2s : ν' s ≠ 0) (h3s : ν' s ≠ ⊤) (f : G → ENNReal) (hf : Measurable f) : μ' s * ∫⁻ (y : G), f (-y) / ν' ((fun (x : G) => x + -y) ⁻¹' s) ∂ν' = ∫⁻ (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 t this states that μ t = c * μ s for a constant c that does not depend on μ.

Note: There is a gap in the last step of the proof in [Halmos]. In the last line, the equality g(-x) + ν(s - x) = f(x) holds if we can prove that 0 < ν(s - x) < ∞. The first inequality follows from §59, Th. D, but the second inequality is not justified. We prove this inequality for almost all x in MeasureTheory.ae_measure_preimage_add_right_lt_top_of_ne_zero.

theorem MeasureTheory.measure_lintegral_div_measure {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] {s : Set G} [MeasurableInv G] (μ' : MeasureTheory.Measure G) (ν' : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ'] [MeasureTheory.SigmaFinite ν'] [μ'.IsMulLeftInvariant] [ν'.IsMulLeftInvariant] (sm : MeasurableSet s) (h2s : ν' s ≠ 0) (h3s : ν' s ≠ ⊤) (f : G → ENNReal) (hf : Measurable f) : μ' s * ∫⁻ (y : G), f y⁻¹ / ν' ((fun (x : G) => x * y⁻¹) ⁻¹' s) ∂ν' = ∫⁻ (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 t this states that μ t = c * μ s for a constant c that does not depend on μ.

Note: There is a gap in the last step of the proof in [Halmos]. In the last line, the equality g(x⁻¹)ν(sx⁻¹) = f(x) holds if we can prove that 0 < ν(sx⁻¹) < ∞. The first inequality follows from §59, Th. D, but the second inequality is not justified. We prove this inequality for almost all x in MeasureTheory.ae_measure_preimage_mul_right_lt_top_of_ne_zero.

theorem MeasureTheory.measure_add_measure_eq {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] (μ' : MeasureTheory.Measure G) (ν' : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ'] [MeasureTheory.SigmaFinite ν'] [μ'.IsAddLeftInvariant] [ν'.IsAddLeftInvariant] (s : Set G) (t : Set G) (h2s : ν' s ≠ 0) (h3s : ν' s ≠ ⊤) : μ' s * ν' t = ν' s * μ' t

theorem MeasureTheory.measure_mul_measure_eq {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] [MeasurableInv G] (μ' : MeasureTheory.Measure G) (ν' : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ'] [MeasureTheory.SigmaFinite ν'] [μ'.IsMulLeftInvariant] [ν'.IsMulLeftInvariant] (s : Set G) (t : Set G) (h2s : ν' s ≠ 0) (h3s : ν' s ≠ ⊤) : μ' s * ν' t = ν' s * μ' t

theorem MeasureTheory.measure_eq_sub_vadd {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] {s : Set G} [MeasurableNeg G] (μ' : MeasureTheory.Measure G) (ν' : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ'] [MeasureTheory.SigmaFinite ν'] [μ'.IsAddLeftInvariant] [ν'.IsAddLeftInvariant] (h2s : ν' s ≠ 0) (h3s : ν' s ≠ ⊤) : μ' = (μ' s / ν' s) • ν'

Left invariant Borel measures on an additive measurable group are unique (up to a scalar).

theorem MeasureTheory.measure_eq_div_smul {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] {s : Set G} [MeasurableInv G] (μ' : MeasureTheory.Measure G) (ν' : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ'] [MeasureTheory.SigmaFinite ν'] [μ'.IsMulLeftInvariant] [ν'.IsMulLeftInvariant] (h2s : ν' s ≠ 0) (h3s : ν' s ≠ ⊤) : μ' = (μ' s / ν' s) • ν'

Left invariant Borel measures on a measurable group are unique (up to a scalar).

theorem MeasureTheory.measurePreserving_prod_add_right {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [ν.IsAddRightInvariant] : MeasureTheory.MeasurePreserving (fun (z : G × G) => (z.1, z.2 + z.1)) (μ.prod ν) (μ.prod ν)

theorem MeasureTheory.measurePreserving_prod_mul_right {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [ν.IsMulRightInvariant] : MeasureTheory.MeasurePreserving (fun (z : G × G) => (z.1, z.2 * z.1)) (μ.prod ν) (μ.prod ν)

theorem MeasureTheory.measurePreserving_prod_add_swap_right {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [μ.IsAddRightInvariant] : MeasureTheory.MeasurePreserving (fun (z : G × G) => (z.2, z.1 + z.2)) (μ.prod ν) (ν.prod μ)

The map (x, y) ↦ (y, x + y) sends the measure μ × ν to ν × μ.

theorem MeasureTheory.measurePreserving_prod_mul_swap_right {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [μ.IsMulRightInvariant] : MeasureTheory.MeasurePreserving (fun (z : G × G) => (z.2, z.1 * z.2)) (μ.prod ν) (ν.prod μ)

The map (x, y) ↦ (y, xy) sends the measure μ × ν to ν × μ.

theorem MeasureTheory.measurePreserving_add_prod {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [μ.IsAddRightInvariant] : MeasureTheory.MeasurePreserving (fun (z : G × G) => (z.1 + z.2, z.2)) (μ.prod ν) (μ.prod ν)

The map (x, y) ↦ (x + y, y) preserves the measure μ × ν.

theorem MeasureTheory.measurePreserving_mul_prod {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [μ.IsMulRightInvariant] : MeasureTheory.MeasurePreserving (fun (z : G × G) => (z.1 * z.2, z.2)) (μ.prod ν) (μ.prod ν)

The map (x, y) ↦ (xy, y) preserves the measure μ × ν.

theorem MeasureTheory.measurePreserving_prod_sub {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableNeg G] [ν.IsAddRightInvariant] : MeasureTheory.MeasurePreserving (fun (z : G × G) => (z.1, z.2 - z.1)) (μ.prod ν) (μ.prod ν)

The map (x, y) ↦ (x, y - x) is measure-preserving.

theorem MeasureTheory.measurePreserving_prod_div {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableInv G] [ν.IsMulRightInvariant] : MeasureTheory.MeasurePreserving (fun (z : G × G) => (z.1, z.2 / z.1)) (μ.prod ν) (μ.prod ν)

The map (x, y) ↦ (x, y / x) is measure-preserving.

theorem MeasureTheory.measurePreserving_prod_sub_swap {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddRightInvariant] : MeasureTheory.MeasurePreserving (fun (z : G × G) => (z.2, z.1 - z.2)) (μ.prod ν) (ν.prod μ)

The map (x, y) ↦ (y, x - y) sends μ × ν to ν × μ.

theorem MeasureTheory.measurePreserving_prod_div_swap {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulRightInvariant] : MeasureTheory.MeasurePreserving (fun (z : G × G) => (z.2, z.1 / z.2)) (μ.prod ν) (ν.prod μ)

The map (x, y) ↦ (y, x / y) sends μ × ν to ν × μ.

theorem MeasureTheory.measurePreserving_sub_prod {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddRightInvariant] : MeasureTheory.MeasurePreserving (fun (z : G × G) => (z.1 - z.2, z.2)) (μ.prod ν) (μ.prod ν)

The map (x, y) ↦ (x - y, y) preserves the measure μ × ν.

theorem MeasureTheory.measurePreserving_div_prod {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulRightInvariant] : MeasureTheory.MeasurePreserving (fun (z : G × G) => (z.1 / z.2, z.2)) (μ.prod ν) (μ.prod ν)

The map (x, y) ↦ (x / y, y) preserves the measure μ × ν.

theorem MeasureTheory.measurePreserving_add_prod_neg_right {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddRightInvariant] [ν.IsAddRightInvariant] : MeasureTheory.MeasurePreserving (fun (z : G × G) => (z.1 + z.2, -z.1)) (μ.prod ν) (μ.prod ν)

The map (x, y) ↦ (x + y, - x) is measure-preserving.

theorem MeasureTheory.measurePreserving_mul_prod_inv_right {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulRightInvariant] [ν.IsMulRightInvariant] : MeasureTheory.MeasurePreserving (fun (z : G × G) => (z.1 * z.2, z.1⁻¹)) (μ.prod ν) (μ.prod ν)

The map (x, y) ↦ (xy, x⁻¹) is measure-preserving.

theorem MeasureTheory.quasiMeasurePreserving_neg_of_right_invariant {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddRightInvariant] : MeasureTheory.Measure.QuasiMeasurePreserving Neg.neg μ μ

theorem MeasureTheory.quasiMeasurePreserving_inv_of_right_invariant {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulRightInvariant] : MeasureTheory.Measure.QuasiMeasurePreserving Inv.inv μ μ

theorem MeasureTheory.quasiMeasurePreserving_sub_left {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant] (g : G) : MeasureTheory.Measure.QuasiMeasurePreserving (fun (h : G) => g - h) μ μ

theorem MeasureTheory.quasiMeasurePreserving_div_left {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant] (g : G) : MeasureTheory.Measure.QuasiMeasurePreserving (fun (h : G) => g / h) μ μ

theorem MeasureTheory.quasiMeasurePreserving_sub_left_of_right_invariant {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddRightInvariant] (g : G) : MeasureTheory.Measure.QuasiMeasurePreserving (fun (h : G) => g - h) μ μ

theorem MeasureTheory.quasiMeasurePreserving_div_left_of_right_invariant {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulRightInvariant] (g : G) : MeasureTheory.Measure.QuasiMeasurePreserving (fun (h : G) => g / h) μ μ

theorem MeasureTheory.quasiMeasurePreserving_sub_of_right_invariant {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddRightInvariant] : MeasureTheory.Measure.QuasiMeasurePreserving (fun (p : G × G) => p.1 - p.2) (μ.prod ν) μ

theorem MeasureTheory.quasiMeasurePreserving_div_of_right_invariant {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulRightInvariant] : MeasureTheory.Measure.QuasiMeasurePreserving (fun (p : G × G) => p.1 / p.2) (μ.prod ν) μ

theorem MeasureTheory.quasiMeasurePreserving_sub {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant] : MeasureTheory.Measure.QuasiMeasurePreserving (fun (p : G × G) => p.1 - p.2) (μ.prod ν) μ

theorem MeasureTheory.quasiMeasurePreserving_div {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant] : MeasureTheory.Measure.QuasiMeasurePreserving (fun (p : G × G) => p.1 / p.2) (μ.prod ν) μ

theorem MeasureTheory.quasiMeasurePreserving_add_right {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant] (g : G) : MeasureTheory.Measure.QuasiMeasurePreserving (fun (h : G) => h + g) μ μ

A left-invariant measure is quasi-preserved by right-addition. This should not be confused with (measurePreserving_add_right μ g).quasiMeasurePreserving.

theorem MeasureTheory.quasiMeasurePreserving_mul_right {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant] (g : G) : MeasureTheory.Measure.QuasiMeasurePreserving (fun (h : G) => h * g) μ μ

A left-invariant measure is quasi-preserved by right-multiplication. This should not be confused with (measurePreserving_mul_right μ g).quasiMeasurePreserving.

theorem MeasureTheory.quasiMeasurePreserving_add_left {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddRightInvariant] (g : G) : MeasureTheory.Measure.QuasiMeasurePreserving (fun (h : G) => g + h) μ μ

A right-invariant measure is quasi-preserved by left-addition. This should not be confused with (measurePreserving_add_left μ g).quasiMeasurePreserving.

theorem MeasureTheory.quasiMeasurePreserving_mul_left {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulRightInvariant] (g : G) : MeasureTheory.Measure.QuasiMeasurePreserving (fun (h : G) => g * h) μ μ

A right-invariant measure is quasi-preserved by left-multiplication. This should not be confused with (measurePreserving_mul_left μ g).quasiMeasurePreserving.