English
Alternative epsilon-delta form of HasIntegral with a slightly different indexing setup, still characterizing HasIntegral via base sets and partitions.
Русский
Альтернативная ε-δ форма HasIntegral с немного иной индексацией, всё та же характеристика HasIntegral через базовые множества и разбиения.
LaTeX
$$$\mathrm{HasIntegral}(I, l, f, vol, y) \iff \forall ε>0, \exists r, \text{... same structure with partition indices ...}$$$
Lean4
/-- Quite often it is more natural to prove an estimate of the form `a * ε`, not `ε` in the RHS of
`BoxIntegral.hasIntegral_iff`, so we provide this auxiliary lemma. -/
theorem of_mul (a : ℝ)
(h :
∀ ε : ℝ,
0 < ε →
∃ r : ℝ≥0 → ℝⁿ → Ioi (0 : ℝ),
(∀ c, l.RCond (r c)) ∧
∀ c π, l.MemBaseSet I c (r c) π → IsPartition π → dist (integralSum f vol π) y ≤ a * ε) :
HasIntegral I l f vol y := by
refine hasIntegral_iff.2 fun ε hε => ?_
rcases exists_pos_mul_lt hε a with ⟨ε', hε', ha⟩
rcases h ε' hε' with ⟨r, hr, H⟩
exact ⟨r, hr, fun c π hπ hπp => (H c π hπ hπp).trans ha.le⟩
