English
HasIntegral I l f vol y is equivalent to an explicit epsilon-delta condition: for every ε>0 there exists r such that ... the integral sums over partitions within base sets are within ε of y.
Русский
HasIntegral I l f vol y эквивалентно условию ε-δ: для каждого ε>0 существует r такое, что ... интегральные суммы по разбиениям внутри базовых множеств ближе чем ε к y.
LaTeX
$$$\mathrm{HasIntegral}(I, l, f, vol, y) \iff \\ \forall \varepsilon>0,\ \exists r: \mathbb{R}_{\ge 0} \to \mathbb{R}^n \to I^{\mathrm{oi}}(0),\ (\forall c, l.RCond(r(c))) \land \ \forall c\;\pi,\ l.MemBaseSet I c (r(c)) \pi \to \pi \;\mathrm{IsPartition} \to \ \mathrm{dist}(\mathrm{integralSum} f vol \pi, y) \le \varepsilon$$$
Lean4
/-- The `ε`-`δ` definition of `BoxIntegral.HasIntegral`. -/
theorem hasIntegral_iff :
HasIntegral I l f vol y ↔
∀ ε > (0 : ℝ),
∃ r : ℝ≥0 → ℝⁿ → Ioi (0 : ℝ),
(∀ c, l.RCond (r c)) ∧ ∀ c π, l.MemBaseSet I c (r c) π → IsPartition π → dist (integralSum f vol π) y ≤ ε :=
((l.hasBasis_toFilteriUnion_top I).tendsto_iff nhds_basis_closedBall).trans <| by
simp [@forall_swap ℝ≥0 (TaggedPrepartition I)]
