English
The filter on finite sequences of uIoc intervals induced by the total length is defined by mapping E to the total length ∑ dist of its endpoints, and pulling back along nhds(0).
Русский
Фильтр на конечные последовательности интервалов uIoc, заданный через общую длину ∑dist концов интервалов и отображение назад в nhds(0).
LaTeX
$$$ \text{totalLengthFilter} := \text{Filter.comap}\big( E \mapsto \sum_{i< E.1} \operatorname{dist}((E.2 i).1, (E.2 i).2) \big) (\mathcal{N}(0)) $$$
Lean4
/-- 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)`, `G` convergence 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.
-/
def totalLengthFilter : Filter (ℕ × (ℕ → X × X)) :=
Filter.comap (fun E ↦ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2) (𝓝 0)
