English
The map (x, y) ↦ (y, xy) sends μ × ν to ν × μ, i.e., a measure-preserving rearrangement on the product space.
Русский
Отображение (x, y) ↦ (y, xy) переводит μ × ν в ν × μ и сохраняет меру.
LaTeX
$$MeasurePreserving (fun z : G × G => (z.1, z.1 * z.2)) (μ.prod ν) (μ.prod ν)$$
Lean4
/-- 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`. -/
@[to_additive measurePreserving_prod_add /-- The shear mapping `(x, y) ↦ (x, x + y)` preserves the measure `μ × ν`. -/
]
theorem measurePreserving_prod_mul [IsMulLeftInvariant ν] :
MeasurePreserving (fun z : G × G => (z.1, z.1 * z.2)) (μ.prod ν) (μ.prod ν) :=
(MeasurePreserving.id μ).skew_product measurable_mul <| Filter.Eventually.of_forall <| map_mul_left_eq_self ν
