English
If the measure of sets s_i tends to zero, then the integral over s_i tends to zero for integrable f.
Русский
Если мере множества s_i стремится к нулю, то интеграл по s_i стремится к нулю.
LaTeX
$$$\text{Tendsto } (\int x \in s_i, f x \partial μ) \to 0 \, \text{при } μ(s_i) \to 0$$$
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_setIntegral_nhds_zero {ι} {f : α → G} (hf : HasFiniteIntegral f μ) {l : Filter ι} {s : ι → Set α}
(hs : Tendsto (μ ∘ s) l (𝓝 0)) : Tendsto (fun i => ∫ x in s i, f x ∂μ) l (𝓝 0) :=
by
rw [tendsto_zero_iff_norm_tendsto_zero]
simp_rw [← coe_nnnorm, ← NNReal.coe_zero, NNReal.tendsto_coe, ← ENNReal.tendsto_coe, ENNReal.coe_zero]
exact
tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds (tendsto_setLIntegral_zero (ne_of_lt hf) hs)
(fun i => zero_le _) fun i => enorm_integral_le_lintegral_enorm _
