English
Let μ be a left-invariant measure on a group; then the almost-everywhere inversion map leaves the a.e. measure unchanged, i.e. the a.e. measure is invariant under taking inverses.
Русский
Пусть μ — слева инвариантная мера на группе. Тогда отображение на обращение элементов не меняет эквивалентность по мере почти всюду, то есть ae μ инвариантно по отношению к операциям взятия обратного.
LaTeX
$$$(\mathrm{ae}\,\mu)^{-1} = \mathrm{ae}\,\mu$$$
Lean4
@[to_additive (attr := simp)]
theorem inv_ae : (ae μ)⁻¹ = ae μ :=
by
refine le_antisymm (quasiMeasurePreserving_inv μ).tendsto_ae ?_
nth_rewrite 1 [← inv_inv (ae μ)]
exact Filter.map_mono (quasiMeasurePreserving_inv μ).tendsto_ae
