quasiMeasurePreserving_div_of_right_invariant

English

If μ is right‑invariant, the division map (x,y) ↦ x/y is quasi‑measure‑preserving from μ × ν to μ.

Русский

Если μ правосторонне инвариантна, отображение деления (x,y) ↦ x/y является квази‑сохранением меры от μ × ν к μ.

LaTeX

$$$\\mathrm{QuasiMeasurePreserving}\\bigl(\\lambda p:(G\\times G). p_{1}/p_{2}\\bigr)\\; (\\mu \\times \\nu) \\; \\mu$$$

Lean4

@[to_additive]
theorem quasiMeasurePreserving_div_of_right_invariant [IsMulRightInvariant μ] :
    QuasiMeasurePreserving (fun p : G × G => p.1 / p.2) (μ.prod ν) μ :=
  by
  refine QuasiMeasurePreserving.prod_of_left measurable_div (Eventually.of_forall fun y => ?_)
  exact (measurePreserving_div_right μ y).quasiMeasurePreserving

Похожие утверждения