Equicontinuous curves in ℓ² without compact closure

The Arzelà–Ascoli theorem ArzelaAscoli.isCompact_closure_range_of_equicontinuous asks that the values of the maps at each point lie in a common compact set. This hypothesis cannot be replaced by equicontinuity and a common starting point when the target is not proper. The curves γₙ(t) = t • eₙ, t ∈ [0, 1], along the standard basis vectors of ℓ² are 1-Lipschitz and all start at 0, but no subsequence converges uniformly, because the endpoints eₙ stay at distance at least 1 from each other.

Main results

• TauCeti.exists_lipschitzWith_one_not_isCompact_closure_range: the curves t • eₙ in ℓ².

theorem TauCeti.exists_lipschitzWith_one_not_isCompact_closure_range : ∃ (γ : ℕ → C(↑(Set.Icc 0 1), ↥(lp (fun (x : ℕ) => ℝ) 2))), (∀ (n : ℕ), LipschitzWith 1 ⇑(γ n)) ∧ (∀ (n : ℕ), (γ n) ⟨0, ⋯⟩ = 0) ∧ ¬IsCompact (closure (Set.range γ))

Equicontinuity and a common starting point do not give compactness. The curves γₙ(t) = t • eₙ, t ∈ [0, 1], along the standard basis vectors eₙ of ℓ² are 1-Lipschitz and all start at 0, but they form a set without compact closure in C([0, 1], ℓ²), because their endpoints are at distance at least 1 from each other. The pointwise compactness hypothesis of ArzelaAscoli.isCompact_closure_range_of_equicontinuous therefore cannot be dropped.