measurePreserving_mul_prod_inv_right

English

The map (x,y) ↦ (xy,y) preserves μ×ν, i.e., μ.prod ν is invariant under this right-multiplication swap.

Русский

Отображение (x,y) ↦ (xy,y) сохраняет μ×ν.

LaTeX

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

Lean4

/-- The map `(x, y) ↦ (xy, x⁻¹)` is measure-preserving. -/
@[to_additive measurePreserving_add_prod_neg_right /-- The map `(x, y) ↦ (x + y, - x)` is measure-preserving. -/
    ]
theorem measurePreserving_mul_prod_inv_right [IsMulRightInvariant μ] [IsMulRightInvariant ν] :
    MeasurePreserving (fun z : G × G => (z.1 * z.2, z.1⁻¹)) (μ.prod ν) (μ.prod ν) :=
  by
  convert (measurePreserving_prod_div_swap ν μ).comp (measurePreserving_prod_mul_swap_right μ ν) using 1
  ext1 ⟨x, y⟩
  simp_rw [Function.comp_apply, div_mul_eq_div_div_swap, div_self', one_div]

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