absolutelyContinuous_map_mul_right

English

Right-multiplication by a fixed element g preserves absolute continuity of μ with respect to its pushforward by right multiplication by g.

Русский

Правое умножение на фиксированный элемент g сохраняет абсолютную непрерывность по отношению к преобразованию меры по правому умножению.

LaTeX

$$$\mu \ll \operatorname{map}(\cdot \mapsto \cdot g)\mu$$$

Lean4

@[to_additive]
theorem absolutelyContinuous_map_mul_right (g : G) : μ ≪ map (· * g) μ :=
  by
  refine AbsolutelyContinuous.mk fun s hs => ?_
  rw [map_apply (measurable_mul_const g) hs, measure_mul_right_null]; exact id

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