measurePreserving_prod_div — Mathlib

English

The map (x,y) ↦ (y, x / y) is measure-preserving, exchanging μ×ν and ν×μ.

Русский

Отображение (x,y) ↦ (y, x / y) сохраняет меру и переводит μ×ν в ν×μ.

LaTeX

$$$\text{MeasurePreserving}(\lambda z. (z.2, z.1 / z.2),\ (\mu \prod ν), (ν \prod μ))$$$

Lean4

/-- The map `(x, y) ↦ (x, y / x)` is measure-preserving. -/
@[to_additive measurePreserving_prod_sub /-- The map `(x, y) ↦ (x, y - x)` is measure-preserving. -/
    ]
theorem measurePreserving_prod_div [IsMulRightInvariant ν] :
    MeasurePreserving (fun z : G × G => (z.1, z.2 / z.1)) (μ.prod ν) (μ.prod ν) :=
  (measurePreserving_prod_mul_right μ ν).symm (MeasurableEquiv.shearDivRight G).symm

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