comp_div_left — Mathlib

English

Let μ be a measure invariant under both inversion and left multiplication. If f: G → E is integrable, then for any g ∈ G the function t ↦ f(g/t) is integrable with respect to μ.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem comp_div_left {f : G → F} [IsInvInvariant μ] [IsMulLeftInvariant μ] (hf : Integrable f μ) (g : G) :
    Integrable (fun t => f (g / t)) μ :=
  ((measurePreserving_div_left μ g).integrable_comp hf.aestronglyMeasurable).mpr hf

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