to_average — Mathlib

English

Let f be integrable with respect to μ. Then f is integrable with respect to the average measure μ_avg := (μ univ)⁻¹ • μ.

Русский

Пусть f интегрируемо по мере μ. Тогда f интегрируемо по усреднённой мере μ_avg := (μ(Ω))⁻¹ μ.

LaTeX

$$$\\text{Integrable } f\\; μ \\;\\Rightarrow\\; \\text{Integrable } f\\;\\big((μ(\\Omega))^{-1}\\,μ\\big)$$$

Lean4

theorem to_average {f : α → ε} (h : Integrable f μ) : Integrable f ((μ univ)⁻¹ • μ) :=
  by
  rcases eq_or_ne μ 0 with (rfl | hne)
  · rwa [smul_zero]
  · apply h.smul_measure
    simpa

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