English
If h is Integrable, then the map from partition to integralSum is Cauchy in the filter toFilteriUnion.
Русский
Если h интегрируемо, отображение из разбиения в integralSum является касательной (Cauchy) в фильтре toFilteriUnion.
LaTeX
$$$\text{Cauchy} ((l.toFilteriUnion I) \map (\text{integralSum } f vol))$$$
Lean4
/-- **Henstock-Sacks inequality**. Let `r₁ r₂ : ℝⁿ → (0, ∞)` be a function such that for any tagged
*partition* of `I` subordinate to `rₖ`, `k=1,2`, the integral sum of `f` over this partition differs
from the integral of `f` by at most `εₖ`. Then for any two tagged *prepartition* `π₁ π₂` subordinate
to `r₁` and `r₂` respectively and covering the same part of `I`, the integral sums of `f` over these
prepartitions differ from each other 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.
See also `BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq` and
`BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet`.
-/
theorem dist_integralSum_le_of_memBaseSet (h : Integrable I l f vol) (hpos₁ : 0 < ε₁) (hpos₂ : 0 < ε₂)
(h₁ : l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁) (h₂ : l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂)
(HU : π₁.iUnion = π₂.iUnion) : dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε₁ + ε₂ :=
by
rcases h₁.exists_common_compl h₂ HU with ⟨π, hπU, hπc₁, hπc₂⟩
set r : ℝⁿ → Ioi (0 : ℝ) := fun x => min (h.convergenceR ε₁ c₁ x) (h.convergenceR ε₂ c₂ x)
set πr := π.toSubordinate r
have H₁ : dist (integralSum f vol (π₁.unionComplToSubordinate π hπU r)) (integral I l f vol) ≤ ε₁ :=
h.dist_integralSum_integral_le_of_memBaseSet hpos₁
(h₁.unionComplToSubordinate (fun _ _ => min_le_left _ _) hπU hπc₁) (isPartition_unionComplToSubordinate _ _ _ _)
rw [HU] at hπU
have H₂ : dist (integralSum f vol (π₂.unionComplToSubordinate π hπU r)) (integral I l f vol) ≤ ε₂ :=
h.dist_integralSum_integral_le_of_memBaseSet hpos₂
(h₂.unionComplToSubordinate (fun _ _ => min_le_right _ _) hπU hπc₂) (isPartition_unionComplToSubordinate _ _ _ _)
simpa [unionComplToSubordinate] using (dist_triangle_right _ _ _).trans (add_le_add H₁ H₂)
