English
Let μ be a left-invariant measure on G and ν a finite measure on G. The map (x, y) ↦ y x from G × G to G is quasi-measure-preserving from μ × ν to μ.
Русский
Пусть μ — слева инвариантное распределение на G, ν — конечное распределение на G. Отображение (x, y) ↦ y x из G × G в G сохраняет меру в смысле квазипредохранения: (μ × ν) переносится к μ.
LaTeX
$$$\\mathrm{QuasiMeasurePreserving}((x,y)\\mapsto yx)\\; (\\mu \\otimes \\nu)\\; \\mu$$$
Lean4
/-- The map `(x, y) ↦ y * x` is quasi-measure-preserving. -/
@[to_additive (attr := fun_prop) /-- The map `(x, y) ↦ y + x` is quasi-measure-preserving. -/
]
theorem quasiMeasurePreserving_mul_swap [IsMulLeftInvariant μ] :
QuasiMeasurePreserving (fun p ↦ p.2 * p.1) (μ.prod ν) μ :=
quasiMeasurePreserving_snd.comp (measurePreserving_prod_mul_swap _ _).quasiMeasurePreserving
