Theorems · Definition · real analysis

AbsolutelyContinuousOnInterval.totalLengthFilter

{X : Type u_1} → [PseudoMetricSpace X] → Filter (ℕ × (ℕ → X × X))

The filter on the collection of all the finite sequences of uIoc intervals induced by the function that maps the finite sequence of the intervals to the total length of the intervals. Details: 1. Technically the filter is on ℕ × (ℕ → X × X). A finite sequence uIoc (a i) (b i), i < n is represented by any E : ℕ × (ℕ → X × X) which satisfies E.1 = n and E.2 i = (a i, b i) for i < n. Its total length is ∑ i ∈ Finset.range n, dist (a i) (b i). 2. For a sequence G : ℕ → ℕ × (ℕ → X × X), convergence of G along totalLengthFilter means that the total length of G j, i.e., ∑ i ∈ Finset.range (G j).1, dist ((G j).2 i).1 ((G j).2 i).2), tends to 0 as j tends to infinity.

Defined in

Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Cited by

13 results in Mathlib

Foundations

Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpace