comp_div_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem comp_div_right {f : G → F} [IsMulRightInvariant μ] (hf : Integrable f μ) (g : G) :
    Integrable (fun t => f (t / g)) μ := by
  simp_rw [div_eq_mul_inv]
  exact hf.comp_mul_right g⁻¹

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