English
The inversion map is quasi-measure-preserving: it is measurable and its pushforward of μ×μ is absolutely continuous w.r.t μ×μ.
Русский
Отображение инверсии является квазимеропереносимым: измеримо и образ μ×μ липок относительно μ×μ.
LaTeX
$$QuasiMeasurePreserving Inv.inv μ μ$$
Lean4
@[to_additive (attr := fun_prop)]
theorem quasiMeasurePreserving_inv : QuasiMeasurePreserving (Inv.inv : G → G) μ μ :=
by
refine ⟨measurable_inv, AbsolutelyContinuous.mk fun s hsm hμs => ?_⟩
rw [map_apply measurable_inv hsm, inv_preimage]
have hf : Measurable fun z : G × G => (z.2 * z.1, z.1⁻¹) :=
(measurable_snd.mul measurable_fst).prodMk measurable_fst.inv
suffices map (fun z : G × G => (z.2 * z.1, z.1⁻¹)) (μ.prod μ) (s⁻¹ ×ˢ s⁻¹) = 0 by
simpa only [(measurePreserving_mul_prod_inv μ μ).map_eq, prod_prod, mul_eq_zero (M₀ := ℝ≥0∞), or_self_iff] using
this
have hsm' : MeasurableSet (s⁻¹ ×ˢ s⁻¹) := hsm.inv.prod hsm.inv
simp_rw [map_apply hf hsm', prod_apply_symm (μ := μ) (ν := μ) (hf hsm'), preimage_preimage, mk_preimage_prod,
inv_preimage, inv_inv, measure_mono_null inter_subset_right hμs, lintegral_zero]
