English
Under hypotheses, the distance between integralSums of two subpartitions is bounded by ε₁ + ε₂.
Русский
При заданных предположениях расстояние между integralSum двух подразбиений ограничено суммой ε₁ и ε₂.
LaTeX
$$$\mathrm{dist}(\text{integralSum } f vol π_1, \text{integralSum } f vol π_2) ≤ ε_1 + ε_2$$$
Lean4
/-- If `f` is integrable on `I` along `l`, then for two sufficiently fine tagged prepartitions
(in the sense of the filter `BoxIntegral.IntegrationParams.toFilter l I`) such that they cover
the same part of `I`, the integral sums of `f` over `π₁` and `π₂` are very close to each other. -/
theorem tendsto_integralSum_toFilter_prod_self_inf_iUnion_eq_uniformity (h : Integrable I l f vol) :
Tendsto (fun π : TaggedPrepartition I × TaggedPrepartition I => (integralSum f vol π.1, integralSum f vol π.2))
((l.toFilter I ×ˢ l.toFilter I) ⊓ 𝓟 {π | π.1.iUnion = π.2.iUnion}) (𝓤 F) :=
by
refine (((l.hasBasis_toFilter I).prod_self.inf_principal _).tendsto_iff uniformity_basis_dist_le).2 fun ε ε0 => ?_
replace ε0 := half_pos ε0
use h.convergenceR (ε / 2), h.convergenceR_cond (ε / 2); rintro ⟨π₁, π₂⟩ ⟨⟨h₁, h₂⟩, hU⟩
rw [← add_halves ε]
exact h.dist_integralSum_le_of_memBaseSet ε0 ε0 h₁.choose_spec h₂.choose_spec hU
