English
The ε-δ definition of absolutely continuous on an interval is equivalent to a statement involving the disjoints within a b and the total length of the intervals.
Русский
Эквивалентность ε-δ определения абсолютной непрерывности на интервале через разбиение на непересекающиеся отрезки и суммарную длину интервалов.
LaTeX
$$$ \text{absolutelyContinuousOnInterval\_iff}(f,a,b) :\; \ AbsolutelyContinuousOnInterval f a b \iff \text{(ε-δ condition with disjoint intervals)} $$$
Lean4
/-- The traditional `ε`-`δ` definition of absolutely continuous: A function `f` is
*absolutely continuous* on `uIcc a b` if for any `ε > 0`, there is `δ > 0` such that for
any finite disjoint collection of intervals `uIoc (a i) (b i)` for `i < n` where `a i`, `b i` are
all in `uIcc a b` for `i < n`, if `∑ i ∈ range n, dist (a i) (b i) < δ`, then
`∑ i ∈ range n, dist (f (a i)) (f (b i)) < ε`. -/
theorem _root_.absolutelyContinuousOnInterval_iff (f : ℝ → X) (a b : ℝ) :
AbsolutelyContinuousOnInterval f a b ↔
∀ ε > (0 : ℝ),
∃ δ > (0 : ℝ),
∀ E,
E ∈ disjWithin a b →
∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε :=
by
simp [AbsolutelyContinuousOnInterval, Metric.tendsto_nhds,
Filter.HasBasis.eventually_iff (hasBasis_totalLengthFilter.inf_principal _), imp.swap,
abs_of_nonneg (Finset.sum_nonneg (fun _ _ ↦ dist_nonneg))]
