English
Let f be integrable on a box I with integration parameters l and volume vol. For any subbox J ≤ I, the integral sums of f over tagged prepartitions that exactly cover J converge to the integral of f over J with respect to l and vol.
Русский
Пусть f интегрируема на коробке I при параметрах интегрирования l и объеме vol. Для любой подкоробки J ≤ I интегральные суммы f по помеченным предварительным разбиениям, покрывающим точно J, сходятся к интегралу f по J относительно l и vol.
LaTeX
$$$$\\operatorname{Tendsto}\\left(\\operatorname{integralSum} f\\, vol\\right)\\left(l.toFilteriUnion I (\\text{Prepartition.single } I J hJ)\\right)\\left(\\mathcal{N}\\left(\\int_J l f\\, vol\\right)\\right)$$$$
Lean4
/-- If `f` is integrable on a box `I`, then integral sums of `f` over tagged prepartitions
that cover exactly a subbox `J ≤ I` tend to the integral of `f` over `J` along `l`. -/
theorem tendsto_integralSum_toFilteriUnion_single (h : Integrable I l f vol) (hJ : J ≤ I) :
Tendsto (integralSum f vol) (l.toFilteriUnion I (Prepartition.single I J hJ)) (𝓝 <| integral J l f vol) :=
let ⟨_y, h₁, h₂⟩ := h.to_subbox_aux hJ
h₁.integral_eq.symm ▸ h₂
