comp_mul_left — Mathlib

English

If μ is invariant under right-multiplication, integrals are preserved under translating f by right-multiplication.

Русский

Если μ инвариантна относительно правого умножения, интегралы сохраняются при сдвиге функции правым умножением.

LaTeX

$$$[IsMulRightInvariant μ] \\Rightarrow \\int_G f(x) dx = \\int_G f(xg) dx$ for all g ∈ G.$$

Lean4

@[to_additive]
theorem comp_mul_left {f : G → F} [IsMulLeftInvariant μ] (hf : Integrable f μ) (g : G) :
    Integrable (fun t => f (g * t)) μ :=
  (hf.mono_measure (map_mul_left_eq_self μ g).le).comp_measurable <| measurable_const_mul g

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