LipschitzCompactSubsequence.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform compactness of transferred Lipschitz data

theorem OAI.RegularPointCoordinates.exists_uniform_lipschitz_subsequence line 15

theorem OAI.RegularPointCoordinates.exists_lipschitz_subsequence_on_compact line 43

Source documentation

On a fixed compact region, the limit retains a global Lipschitz extension.

theorem exists_lipschitz_subsequence_on_compact {Z : Type*} [MetricSpace Z]
    {s : Set Z} (hs : IsCompact s) (f : ℕ → Z → ℝ) (L : ℝ≥0) (A : ℝ)
    (hl : ∀ k, LipschitzWith L (f k)) (hb : ∀ k z, z∈s → |f k z|≤A) :
    ∃ (g : Z → ℝ) (a : ℕ → ℕ), StrictMono a ∧ LipschitzWith L g ∧
      (∀ z∈s, |g z|≤A) ∧
      ∀ ε : ℝ, 0<ε → ∀ᶠ k in atTop, ∀ z∈s, |f (a k) z-g z|<ε := by
…