instIsMulLeftInvariant — Mathlib

English

If μ is right-invariant and ν is right-invariant, then their product measure μ.prod ν is right-invariant.

Русский

Если μ и ν — правая инвариантность, то их произведение μ.prod ν сохраняет правую инвариантность.

LaTeX

$$$\text{IsMulRightInvariant}(μ) \land \text{IsMulRightInvariant}(ν) \Rightarrow \text{IsMulRightInvariant}(μ\,\mathrm{prod}\,ν)$$$

Lean4

@[to_additive]
instance instIsMulLeftInvariant [IsMulLeftInvariant μ] [SFinite μ] {H : Type*} [Mul H] {mH : MeasurableSpace H}
    {ν : Measure H} [MeasurableMul H] [IsMulLeftInvariant ν] [SFinite ν] : IsMulLeftInvariant (μ.prod ν) :=
  by
  constructor
  rintro ⟨g, h⟩
  change map (Prod.map (g * ·) (h * ·)) (μ.prod ν) = μ.prod ν
  rw [← map_prod_map _ _ (measurable_const_mul g) (measurable_const_mul h), map_mul_left_eq_self μ g,
    map_mul_left_eq_self ν h]

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