English
If μ is left invariant, the division map on pairs is quasi-preserving with respect to μ and μ.
Русский
Если μ левоинвариантна, отображение деления на парах сохраняет меру в смысле квази‑сохранения.
LaTeX
$$$\\mathrm{QuasiMeasurePreserving}\\bigl(\\lambda p:(G\\times G). p_{1}/p_{2}\\bigr)\\; (\\mu \\times \\mu) \\; \\mu$$$
Lean4
/-- A *right*-invariant measure is quasi-preserved by *left*-multiplication.
This should not be confused with `(measurePreserving_mul_left μ g).quasiMeasurePreserving`. -/
@[to_additive (attr := fun_prop) /-- A *right*-invariant measure is quasi-preserved by *left*-addition.
This should not be confused with `(measurePreserving_add_left μ g).quasiMeasurePreserving`. -/
]
theorem quasiMeasurePreserving_mul_left [IsMulRightInvariant μ] (g : G) :
QuasiMeasurePreserving (fun h : G => g * h) μ μ :=
by
have :=
(quasiMeasurePreserving_mul_right μ.inv g⁻¹).mono (inv_absolutelyContinuous μ.inv) (absolutelyContinuous_inv μ.inv)
rw [μ.inv_inv] at this
have :=
(quasiMeasurePreserving_inv_of_right_invariant μ).comp (this.comp (quasiMeasurePreserving_inv_of_right_invariant μ))
simp_rw [Function.comp_def, mul_inv_rev, inv_inv] at this
exact this
