comp_inv — Mathlib

English

If a function f is integrable on G with respect to μ and μ is left-invariant, then the translated function t ↦ f(g t) is integrable with respect to μ for any g in G.

Русский

Если f интегрируема по μ и μ инвариантна слева, то тождественный сдвиг g t сохраняет интегрируемость.

LaTeX

$$$[IsInvInvariant μ] \\Rightarrow \\text{Integrable}(f) \\Rightarrow \\text{Integrable}(f(g\\cdot))$.$$

Lean4

@[to_additive]
theorem comp_inv [IsInvInvariant μ] {f : G → F} {s : Set G} (hf : IntegrableOn f s μ) :
    IntegrableOn (fun x => f x⁻¹) s⁻¹ μ :=
  by
  apply (integrable_map_equiv (MeasurableEquiv.inv G) f).mp
  have : s⁻¹ = MeasurableEquiv.inv G ⁻¹' s := by simp
  rw [this, ← MeasurableEquiv.restrict_map]
  simpa using hf

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