English
A left‑invariant measure μ is quasi‑preserved by right multiplication: the map h ↦ h g is quasi‑measure‑preserving from μ to μ for any g.
Русский
Левая инвариантная мера μ сохраняется под правым умножением: отображение h ↦ h g — квази‑сохранение меры в отношении μ.
LaTeX
$$$\\mathrm{QuasiMeasurePreserving}\\bigl(\\lambda h:G,\\; h g\\bigr)\\; \\mu\\; \\mu$$$
Lean4
/-- A *left*-invariant measure is quasi-preserved by *right*-multiplication.
This should not be confused with `(measurePreserving_mul_right μ g).quasiMeasurePreserving`. -/
@[to_additive (attr := fun_prop) /-- A *left*-invariant measure is quasi-preserved by *right*-addition.
This should not be confused with `(measurePreserving_add_right μ g).quasiMeasurePreserving`. -/
]
theorem quasiMeasurePreserving_mul_right [IsMulLeftInvariant μ] (g : G) :
QuasiMeasurePreserving (fun h : G => h * g) μ μ :=
by
refine ⟨measurable_mul_const g, AbsolutelyContinuous.mk fun s hs => ?_⟩
rw [map_apply (measurable_mul_const g) hs, measure_mul_right_null]; exact id
