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