English
For Countable ι, hf and hp, almost everywhere we have ∀ i, aeSeq hf p i a = (hf i).mk (f i) a.
Русский
Для счетного ι, hf и hp почти при любом a выполняется ∀ i, aeSeq hf p i a = (hf i).mk (f i) a.
LaTeX
$$$ \forall^\! a \partial\mu,\ \forall i,\ aeSeq\, hf\, p\, i\, a = (hf i)\, . mk\, (f i)\, a $$$
Lean4
/-- `AbsolutelyContinuousOnInterval f a b`: A function `f` is *absolutely continuous* on `uIcc a b`
if the function which (intuitively) maps `uIoc (a i) (b i)`, `i < n` to
`∑ i ∈ Finset.range n, dist (f (a i)) (f (b i))` tendsto `𝓝 0` wrt `totalLengthFilter` restricted
to `disjWithin a b`. This is equivalent to the traditional `ε`-`δ` definition: 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)) < ε`. -/
def _root_.AbsolutelyContinuousOnInterval (f : ℝ → X) (a b : ℝ) :=
Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
(𝓝 0)
