isMulRightInvariant — Mathlib

English

There is a corresponding right-invariance for the product measure under the product group action.

Русский

Существует соответствующая правая инвариантность произведения меры под действием произведения групп.

LaTeX

$$$(\\mathrm{pi}\\; μ).IsMulRightInvariant$$$

Lean4

@[to_additive]
instance isMulRightInvariant [∀ i, Group (α i)] [∀ i, MeasurableMul (α i)] [∀ i, IsMulRightInvariant (μ i)] :
    IsMulRightInvariant (Measure.pi μ) :=
  by
  refine ⟨fun v => (pi_eq fun s hs => ?_).symm⟩
  rw [map_apply (measurable_mul_const _) (MeasurableSet.univ_pi hs),
    show (· * v) ⁻¹' univ.pi s = univ.pi fun i => (· * v i) ⁻¹' s i by rfl, pi_pi]
  simp_rw [measure_preimage_mul_right]

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