English
Let h be integrable on I, and π be a prepartition with iUnion = that of π₀. Then the distance between the integral sum over π and the sum of box integrals over π₀ is bounded by ε.
Русский
Пусть h интегрируем на I, а предварительно разбиение π имеет то же объединение, что и π₀. Тогда расстояние между интегральной суммой по π и суммой интегралов по коробкам π₀ ограничено ε.
LaTeX
$$$$\\operatorname{dist}\\left(\\operatorname{integralSum} f vol\\, π, \\sum_{J\\in π_0.boxes} \\operatorname{integral} J\\, l\\, f vol\\right) \\le \\varepsilon.$$$$
Lean4
/-- **Henstock-Sacks inequality**. Let `r : ℝⁿ → (0, ∞)` be a function such that for any tagged
*partition* of `I` subordinate to `r`, the integral sum of `f` over this partition differs from the
integral of `f` by at most `ε`. Then for any tagged *prepartition* `π` subordinate to `r`, the
integral sum of `f` over this prepartition differs from the integral of `f` over the part of `I`
covered by `π` by at most `ε`.
The actual statement
- uses `BoxIntegral.Integrable.convergenceR` instead of a predicate assumption on `r`;
- uses `BoxIntegral.IntegrationParams.MemBaseSet` instead of “subordinate to `r`” to
account for additional requirements like being a Henstock partition or having a bounded
distortion;
-/
theorem dist_integralSum_sum_integral_le_of_memBaseSet (h : Integrable I l f vol) (h0 : 0 < ε)
(hπ : l.MemBaseSet I c (h.convergenceR ε c) π) :
dist (integralSum f vol π) (∑ J ∈ π.boxes, integral J l f vol) ≤ ε :=
h.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq h0 hπ rfl
