integrable_approxOn — Mathlib

English

If f is integrable, then every approximant approxOn(f) is integrable for all n.

Русский

Если f интегрируема, то каждое приближение approxOn(f) интегрируемо для всех n.

LaTeX

$$$\\text{Integrable}(f) \\Rightarrow \\forall n,\\; Integrable(approxOn f hf s y_0 h_0 n).$$$

Lean4

theorem integrable_approxOn [BorelSpace E] {f : β → E} {μ : Measure β} (fmeas : Measurable f) (hf : Integrable f μ)
    {s : Set E} {y₀ : E} (h₀ : y₀ ∈ s) [SeparableSpace s] (hi₀ : Integrable (fun _ => y₀) μ) (n : ℕ) :
    Integrable (approxOn f fmeas s y₀ h₀ n) μ :=
  by
  rw [← memLp_one_iff_integrable] at hf hi₀ ⊢
  exact memLp_approxOn fmeas hf h₀ hi₀ n

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