tendsto_setIntegral_nhds_zero — Mathlib

English

If f has finite integral, then ∫_{s} f tends to 0 as μ(s) → 0.

Русский

Если f имеет конечный интеграл, то ∫_{s} f → 0 при μ(s) → 0.

LaTeX

$$$\\text{HasFiniteIntegral } f μ \\Rightarrow \\lim_{μ(s)\\to 0} \\int x \\in s, f x \\partial μ = 0$$$

Lean4

/-- If `f` is integrable, then `∫ x in s, f x ∂μ` is absolutely continuous in `s`: it tends
to zero as `μ s` tends to zero. -/
theorem tendsto_setIntegral_nhds_zero {ι} {f : α → G} (hf : Integrable f μ) {l : Filter ι} {s : ι → Set α}
    (hs : Tendsto (μ ∘ s) l (𝓝 0)) : Tendsto (fun i => ∫ x in s i, f x ∂μ) l (𝓝 0) :=
  hf.2.tendsto_setIntegral_nhds_zero hs

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