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 μ(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
.
The map (x, y) ↦ (x, xy)
as a measurable_equiv
. This is a shear mapping.
Equations
- measurable_equiv.shear_mul_right G = {to_equiv := {to_fun := ((equiv.refl G).prod_shear equiv.mul_left).to_fun, inv_fun := ((equiv.refl G).prod_shear equiv.mul_left).inv_fun, left_inv := _, right_inv := _}, measurable_to_fun := _, measurable_inv_fun := _}
The map (x, y) ↦ (x, x + y)
as a measurable_equiv
.
This is a shear mapping.
Equations
- measurable_equiv.shear_add_right G = {to_equiv := {to_fun := ((equiv.refl G).prod_shear equiv.add_left).to_fun, inv_fun := ((equiv.refl G).prod_shear equiv.add_left).inv_fun, left_inv := _, right_inv := _}, measurable_to_fun := _, measurable_inv_fun := _}
An additive shear mapping preserves the measure μ.prod ν
.
A shear mapping preserves the measure μ.prod ν
.
This condition is part of the definition of a measurable group in [Halmos, §59].
There, the map in this lemma is called S
.
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
.
The function we are mapping along is S⁻¹
in [Halmos, §59],
where S
is the map in map_prod_mul_eq
.
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
.
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
.
This is the computation performed in the proof of [Halmos, §60 Th. A].
Any two nonzero left-invariant measures are absolutely continuous w.r.t. each other.
Any two nonzero left-invariant measures are absolutely continuous w.r.t. each other.
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 μ
.
Note: There is 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 the second inequality is
not justified. We prove this inequality for almost all x
in
measure_theory.ae_measure_preimage_mul_right_lt_top_of_ne_zero
.
Left invariant Borel measures on an additive measurable group are unique (up to a scalar).
Left invariant Borel measures on a measurable group are unique (up to a scalar).