measurable_measure_mul_right — Mathlib

English

If s is measurable in G, then the map x ↦ μ((y ↦ yx)⁻¹(s)) is measurable in x; i.e., measurability of right-translation measure is preserved.

Русский

Если s измеримо, то карта x ↦ μ((y ↦ yx)⁻¹(s)) измерима по x; сохраняется измеримость правого переноса меры.

LaTeX

$$Measurable fun x => μ (Set.preimage (fun y => y * x) s)$$

Lean4

@[to_additive]
theorem measurable_measure_mul_right (hs : MeasurableSet s) : Measurable fun x => μ ((fun y => y * x) ⁻¹' s) :=
  by
  suffices Measurable fun y => μ ((fun x => (x, y)) ⁻¹' ((fun z : G × G => ((1 : G), z.1 * z.2)) ⁻¹' univ ×ˢ s)) by
    convert this using 1; ext1 x; congr 1 with y : 1; simp
  apply measurable_measure_prodMk_right
  apply measurable_const.prodMk measurable_mul (MeasurableSet.univ.prod hs)
  infer_instance

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