integrable_average — Mathlib

English

If μ is finite, then for any f, f is integrable with respect to μ if and only if f is integrable with respect to the average measure μ_avg = (μ(Ω))⁻¹ • μ.

Русский

Если μ конечна, то для любого f интегрируемость f по μ эквивалентна интегрируемости по усреднённой мере μ_avg = (μ(Ω))⁻¹ μ.

LaTeX

$$$f \\in L^1(μ) \\iff f \\in L^1\\left((μ(Ω))^{-1} μ\\right)$$$

Lean4

theorem integrable_average [IsFiniteMeasure μ] {f : α → ε} : Integrable f ((μ univ)⁻¹ • μ) ↔ Integrable f μ :=
  (eq_or_ne μ 0).by_cases (fun h => by simp [h]) fun h =>
    integrable_smul_measure (ENNReal.inv_ne_zero.2 <| measure_ne_top _ _)
      (ENNReal.inv_ne_top.2 <| mt Measure.measure_univ_eq_zero.1 h)

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