isMulLeftInvariant — Mathlib

English

If each μ_i is a left-invariant measure under a group structure, then the Pi-product is left-invariant under the corresponding product group action.

Русский

Если каждая μ_i является лево-инвариантной мерой относительно группы, то произведение Pi инвариантно слева по произведению групп.

LaTeX

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

Lean4

@[to_additive]
instance isMulLeftInvariant [∀ i, Group (α i)] [∀ i, MeasurableMul (α i)] [∀ i, IsMulLeftInvariant (μ i)] :
    IsMulLeftInvariant (Measure.pi μ) :=
  by
  refine ⟨fun v => (pi_eq fun s hs => ?_).symm⟩
  rw [map_apply (measurable_const_mul _) (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]

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