English
From integrability on I, there exists a subbox J ≤ I and a corresponding y with HasIntegral J for f and tendsto of integralSum to y as partitions refine.
Русский
Из интегрируемости на I существует подпbox J ≤ I и соответствующее y, для которого HasIntegral J f vol y и предел сумм интегралов стремится к y при уточнении разбиений.
LaTeX
$$$\exists y,\ HasIntegral J l f vol y \land \ Tendsto (\text{integralSum } f vol) (l.toFilteriUnion I (Prepartition.single I J hJ)) \ (\mathcal{NHDS} y)$$$
Lean4
/-- If `f` is integrable on a box `I` along `l`, then for any fixed subset `s` of `I` that can be
represented as a finite union of boxes, the integral sums of `f` over tagged prepartitions that
cover exactly `s` form a Cauchy “sequence” along `l`. -/
theorem cauchy_map_integralSum_toFilteriUnion (h : Integrable I l f vol) (π₀ : Prepartition I) :
Cauchy ((l.toFilteriUnion I π₀).map (integralSum f vol)) :=
by
refine ⟨inferInstance, ?_⟩
rw [prod_map_map_eq, ← toFilter_inf_iUnion_eq, ← prod_inf_prod, prod_principal_principal]
exact
h.tendsto_integralSum_toFilter_prod_self_inf_iUnion_eq_uniformity.mono_left
(inf_le_inf_left _ <| principal_mono.2 fun π h => h.1.trans h.2.symm)
