comp_mul_right — Mathlib

English

Let μ be a measure on a group G that is invariant under right translations. If f: G → E is integrable with respect to μ, then for every g ∈ G the function t ↦ f(tg) is integrable with respect to μ.

Русский

Пусть μ — мера на группе G, инвариантная относительно правого переноса. Если f: G → E интегрируема по μ, то для каждого g ∈ G функция t ↦ f(tg) интегрируема по μ.

LaTeX

$$$$ \\mathrm{Integrable}(f, \\mu) \\Rightarrow \\forall g \\in G, \\; \\mathrm{Integrable}(t \\mapsto f(tg), \\mu). $$$$

Lean4

@[to_additive]
theorem comp_mul_right {f : G → F} [IsMulRightInvariant μ] (hf : Integrable f μ) (g : G) :
    Integrable (fun t => f (t * g)) μ :=
  (hf.mono_measure (map_mul_right_eq_self μ g).le).comp_measurable <| measurable_mul_const g

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