integrable_approxOn_range — Mathlib

English

If f is integrable, then the range-based approximants are integrable for all n.

Русский

Если f интегрируема, то аппроксимации по диапазону интегрируемы для всех n.

LaTeX

$$$Integrable(f) \\Rightarrow \\forall n,\\; Integrable(approxOn f fmeas (range f \\cup {0}) 0 (by simp) n).$$$

Lean4

theorem integrable_approxOn_range [BorelSpace E] {f : β → E} {μ : Measure β} (fmeas : Measurable f)
    [SeparableSpace (range f ∪ {0} : Set E)] (hf : Integrable f μ) (n : ℕ) :
    Integrable (approxOn f fmeas (range f ∪ {0}) 0 (by simp) n) μ :=
  integrable_approxOn fmeas hf _ (integrable_zero _ _ _) n

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