English
If ∫ f dμ ≠ ∞, then for any ε > 0 there exists δ > 0 such that μ(s) < δ implies ∫_s f dμ < ε.
Русский
Если интеграл конечен, то для каждого ε>0 существует δ>0, чтобы μ(s)<δ ⇒ ∫_s f dμ < ε.
LaTeX
$$$\\exists \\delta>0, \\forall s, μ(s) < \\delta \\Rightarrow \\int_s f \\, d\\mu < \\varepsilon$$$
Lean4
/-- If `f` has finite integral, then `∫⁻ x in s, f x ∂μ` is absolutely continuous in `s`: it tends
to zero as `μ s` tends to zero. -/
theorem tendsto_setLIntegral_zero {ι} {f : α → ℝ≥0∞} (h : ∫⁻ x, f x ∂μ ≠ ∞) {l : Filter ι} {s : ι → Set α}
(hl : Tendsto (μ ∘ s) l (𝓝 0)) : Tendsto (fun i => ∫⁻ x in s i, f x ∂μ) l (𝓝 0) :=
by
simp only [ENNReal.nhds_zero, tendsto_iInf, tendsto_principal, mem_Iio, ← pos_iff_ne_zero] at hl ⊢
intro ε ε0
rcases exists_pos_setLIntegral_lt_of_measure_lt h ε0.ne' with ⟨δ, δ0, hδ⟩
exact (hl δ δ0).mono fun i => hδ _
