English
If f is integrable on I with respect to l, and π is a base-set partition subordinate to a bound B on the subboxes, then for any π₀ with the same union, the distance between the integral sum over π and the sum of box integrals over π₀ is at most ε.
Русский
Если f интегрируема на I относительно l и существует неотрицательная функция B, такая что для любой подчасти есть подстановки, тогда для любых π₀ с тем же объединением расстояние между суммой интегральных сумм по π и суммой интегралов по каждому блоку π₀ не превосходит ε.
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;
- takes an extra argument `π₀ : prepartition I` and an assumption `π.Union = π₀.Union` instead of
using `π.to_prepartition`.
-/
theorem dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq (h : Integrable I l f vol) (h0 : 0 < ε)
(hπ : l.MemBaseSet I c (h.convergenceR ε c) π) {π₀ : Prepartition I} (hU : π.iUnion = π₀.iUnion) :
dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε := by
-- Let us prove that the distance is less than or equal to `ε + δ` for all positive `δ`.
refine
le_of_forall_pos_le_add fun δ δ0 =>
?_
-- First we choose some constants.
set δ' : ℝ := δ / (#π₀.boxes + 1)
have H0 : 0 < (#π₀.boxes + 1 : ℝ) := Nat.cast_add_one_pos _
have δ'0 : 0 < δ' := div_pos δ0 H0
set C := max π₀.distortion π₀.compl.distortion
have :
∀ J ∈ π₀,
∃ πi : TaggedPrepartition J,
πi.IsPartition ∧
dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧ l.MemBaseSet J C (h.convergenceR δ' C) πi :=
by
intro J hJ
have Hle : J ≤ I := π₀.le_of_mem hJ
have HJi : Integrable J l f vol := h.to_subbox Hle
set r := fun x => min (h.convergenceR δ' C x) (HJi.convergenceR δ' C x)
have hJd : J.distortion ≤ C := le_trans (Finset.le_sup hJ) (le_max_left _ _)
rcases l.exists_memBaseSet_isPartition J hJd r with ⟨πJ, hC, hp⟩
have hC₁ : l.MemBaseSet J C (HJi.convergenceR δ' C) πJ := by refine hC.mono J le_rfl le_rfl fun x _ => ?_;
exact min_le_right _ _
have hC₂ : l.MemBaseSet J C (h.convergenceR δ' C) πJ := by refine hC.mono J le_rfl le_rfl fun x _ => ?_;
exact min_le_left _ _
exact
⟨πJ, hp, HJi.dist_integralSum_integral_le_of_memBaseSet δ'0 hC₁ hp, hC₂⟩
/- Now we combine these tagged partitions into a tagged prepartition of `I` that covers the
same part of `I` as `π₀` and apply `BoxIntegral.dist_integralSum_le_of_memBaseSet` to
`π` and this prepartition. -/
choose! πi hπip hπiδ' hπiC using this
have : l.MemBaseSet I C (h.convergenceR δ' C) (π₀.biUnionTagged πi) :=
biUnionTagged_memBaseSet hπiC hπip fun _ => le_max_right _ _
have hU' : π.iUnion = (π₀.biUnionTagged πi).iUnion := hU.trans (Prepartition.iUnion_biUnion_partition _ hπip).symm
have := h.dist_integralSum_le_of_memBaseSet h0 δ'0 hπ this hU'
rw [integralSum_biUnionTagged] at this
calc
dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤
dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integralSum f vol (πi J)) +
dist (∑ J ∈ π₀.boxes, integralSum f vol (πi J)) (∑ J ∈ π₀.boxes, integral J l f vol) :=
dist_triangle _ _ _
_ ≤ ε + δ' + ∑ _J ∈ π₀.boxes, δ' := (add_le_add this (dist_sum_sum_le_of_le _ hπiδ'))
_ = ε + δ := by simp [field, δ']; ring
