integrable_comp_div_left — Mathlib

English

For a measure μ that is invariant under inversion and left multiplication, and for any g ∈ G, Integrable(f, μ) holds if and only if Integrable(t ↦ f(g/t), μ).

Русский

Для меры μ, инвариантной относительно инверсии и левого умножения, для любого g ∈ G выполняется: Integrable(f, μ) тогда и только тогда, когда Integrable(t ↦ f(g/t), μ).

LaTeX

$$$$ \\mathrm{Integrable}(f, \\mu) \\iff \\mathrm{Integrable}(t \\mapsto f(g/t), \\mu). $$$$

Lean4

@[to_additive]
theorem integrable_comp_div_left (f : G → F) [IsInvInvariant μ] [IsMulLeftInvariant μ] (g : G) :
    Integrable (fun t => f (g / t)) μ ↔ Integrable f μ :=
  by
  refine ⟨fun h => ?_, fun h => h.comp_div_left g⟩
  convert h.comp_inv.comp_mul_left g⁻¹
  simp_rw [div_inv_eq_mul, mul_inv_cancel_left]

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