quasiMeasurePreserving_div — Mathlib

English

For a left‑invariant μ, the map (x,y) ↦ x/y is quasi‑measure‑preserving with respect to (μ, ν) and μ.

Русский

Для левой инвариантной меры μ отображение деления (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 [IsMulLeftInvariant μ] :
    QuasiMeasurePreserving (fun p : G × G => p.1 / p.2) (μ.prod ν) μ :=
  (quasiMeasurePreserving_div_of_right_invariant μ.inv ν).mono
    ((absolutelyContinuous_inv μ).prod AbsolutelyContinuous.rfl) (inv_absolutelyContinuous μ)

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