instDistribMulActionDomMulAct — Mathlib

English

For a nonzero g in G₀, the map x ↦ x g is a measurable embedding.

Русский

Для ненулевого g в G₀ отображение x ↦ x g является измеримым вложением.

LaTeX

$$$\\text{measurableEmbedding\_mulRight}_{0}(g)\\;:\\; x \\mapsto x g$$$

Lean4

noncomputable instance : DistribMulAction Gᵈᵐᵃ (Measure A)
    where
  smul g μ := μ.map (DomMulAct.mk.symm g⁻¹ • ·)
  one_smul μ := show μ.map _ = _ by simp
  mul_smul g g'
    μ :=
    show μ.map _ = ((μ.map _).map _) by
      rw [map_map]
      · simp [Function.comp_def, mul_smul]
      · exact measurable_const_smul ..
      · exact measurable_const_smul ..
  smul_zero g := show (0 : Measure A).map _ = 0 by simp
  smul_add g μ ν := show (μ + ν).map _ = μ.map _ + ν.map _ by rw [Measure.map_add]; exact measurable_const_smul ..

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