measurePreserving_prod_mul_right — Mathlib

English

The product-pair transformation (x,y) ↦ (x, y*x) preserves the product measure μ×ν.

Русский

Преобразование (x,y)↦(x, yx) сохраняет произведенную меру μ×ν.

LaTeX

$$$\text{MeasurePreserving}( (x,y) \mapsto (x, yx) ) (\mu \times \nu) (\mu \times \nu)$$$

Lean4

@[to_additive measurePreserving_prod_add_right]
theorem measurePreserving_prod_mul_right [IsMulRightInvariant ν] :
    MeasurePreserving (fun z : G × G => (z.1, z.2 * z.1)) (μ.prod ν) (μ.prod ν) :=
  MeasurePreserving.skew_product (g := fun x y => y * x) (MeasurePreserving.id μ) (measurable_snd.mul measurable_fst) <|
    Filter.Eventually.of_forall <| map_mul_right_eq_self ν

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