English
If h is integrable on I with respect to l, then for any prepartition π₀, the integral sum f vol along the refinement to I under π₀ converges to the sum of box integrals over π₀.
Русский
Если функция интегрируема на I относительно l, то интегральная сумма по π₀ стремится к сумме интегралов по коробкам π₀ при refinements.
LaTeX
$$$$\\operatorname{Tendsto}\left(\\operatorname{integralSum} f vol\\right)\\left( l.toFilteriUnion I \\pi_0\\right)\\left(\\mathcal{N}\\left(\\sum_{J\\in \\pi_0.boxes} \\int_J l f vol\\right)\\right).$$$$
Lean4
/-- Integral sum of `f` over a tagged prepartition `π` such that `π.Union = π₀.Union` tends to the
sum of integrals of `f` over the boxes of `π₀`. -/
theorem tendsto_integralSum_sum_integral (h : Integrable I l f vol) (π₀ : Prepartition I) :
Tendsto (integralSum f vol) (l.toFilteriUnion I π₀) (𝓝 <| ∑ J ∈ π₀.boxes, integral J l f vol) :=
by
refine ((l.hasBasis_toFilteriUnion I π₀).tendsto_iff nhds_basis_closedBall).2 fun ε ε0 => ?_
refine ⟨h.convergenceR ε, h.convergenceR_cond ε, ?_⟩
simp only [mem_setOf_eq]
rintro π ⟨c, hc, hU⟩
exact h.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq ε0 hc hU
