measurePreserving_prod_inv_mul_swap

English

The measure-preserving composition of product-inverse maps shows that inv map of product measure preserves μ × ν.

Русский

Композиция мeр-предержащих отображений (inv) сохраняет меру μ × ν.

LaTeX

$$MeasurePreserving (fun z => (z.2 * z.1, z.1⁻¹)) (μ.prod ν) (μ.prod ν)$$

Lean4

/-- The map `(x, y) ↦ (y, y⁻¹x)` sends `μ × ν` to `ν × μ`.
This is the function `S⁻¹R` in [Halmos, §59],
where `S` is the map `(x, y) ↦ (x, xy)` and `R` is `Prod.swap`. -/
@[to_additive measurePreserving_prod_neg_add_swap /-- The map `(x, y) ↦ (y, - y + x)` sends `μ × ν` to `ν × μ`. -/
    ]
theorem measurePreserving_prod_inv_mul_swap :
    MeasurePreserving (fun z : G × G => (z.2, z.2⁻¹ * z.1)) (μ.prod ν) (ν.prod μ) :=
  (measurePreserving_prod_inv_mul ν μ).comp measurePreserving_swap

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