map_mul_left_ae — Mathlib

English

If μ is left invariant, then the a.e. image under left multiplication agrees with μ.

Русский

Если μ слева инвариантна, то образ на едва точку по левому умножению совпадает с μ почти наверняка.

LaTeX

$$$(\text{μ is left invariant}) \Rightarrow (map (\cdot)_{left} μ)_{ae} = μ_{ae}$$$

Lean4

@[to_additive]
theorem map_mul_left_ae (μ : Measure G) [IsMulLeftInvariant μ] (x : G) : Filter.map (fun h => x * h) (ae μ) = ae μ :=
  ((MeasurableEquiv.mulLeft x).map_ae μ).trans <| congr_arg ae <| map_mul_left_eq_self μ x

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