PhysicalGuideCompactness.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform subsequence compactness for the physical guide curves. A common speed bound and bounded starting points put the entire family in one compact disk; Arzelà–Ascoli then gives a uniformly convergent subsequence on the fixed interval.

theorem OAI.SLEExactGauge.PhysicalGuideCompactness.exists_uniform_subsequence line 20

Source documentation

A common Lipschitz bound and bounded tips suffice for uniform subsequence compactness of the physical guides. The limit retains the same speed bound.

theorem exists_uniform_subsequence
    (αₙ : ℕ → ℝ → ℂ) {T R : ℝ} (hT : 0 ≤ T) (C : ℝ≥0)
    (hL : ∀ n, LipschitzOnWith C (αₙ n) (Icc 0 T))
    (htip : ∀ n, ‖αₙ n 0‖ ≤ R) :
    ∃ α : ℝ → ℂ, ∃ φ : ℕ → ℕ, StrictMono φ ∧
      TendstoUniformlyOn (fun n => αₙ (φ n)) α atTop (Icc 0 T) ∧
      LipschitzOnWith C α (Icc 0 T) ∧ ContinuousOn α (Icc 0 T) ∧ ‖α 0‖ ≤ R := by
…

theorem OAI.SLEExactGauge.PhysicalGuideCompactness.lower_chord_bound_of_uniform_limit line 69

Source documentation

The fixed lower chord bound of a guide patch passes to its uniform limit.

theorem lower_chord_bound_of_uniform_limit
    {αₙ : ℕ → ℝ → ℂ} {α : ℝ → ℂ} {I : Set ℝ} {c : ℝ}
    (hu : TendstoUniformlyOn αₙ α atTop I)
    (hchord : ∀ n s, s ∈ I → ∀ t, t ∈ I →
      c * |s - t| ≤ dist (αₙ n s) (αₙ n t)) :
    ∀ s ∈ I, ∀ t ∈ I, c * |s - t| ≤ dist (α s) (α t) := by
…

theorem OAI.SLEExactGauge.PhysicalGuideCompactness.injective_of_lower_chord_bound line 80

Source documentation

Positive lower chord bounds force a guide to be simple.

theorem injective_of_lower_chord_bound
    {α : ℝ → ℂ} {I : Set ℝ} {c : ℝ} (hc : 0 < c)
    (hchord : ∀ s ∈ I, ∀ t ∈ I, c * |s - t| ≤ dist (α s) (α t)) :
    InjOn α I := by
…

theorem OAI.SLEExactGauge.PhysicalGuideCompactness.exists_simple_uniform_subsequence line 92

Source documentation

Bi-Lipschitz physical guide patches have simple, uniformly convergent subsequential limits with the same two chord constants.

theorem exists_simple_uniform_subsequence
    (αₙ : ℕ → ℝ → ℂ) {T R c : ℝ} (hT : 0 ≤ T) (C : ℝ≥0) (hc : 0 < c)
    (hL : ∀ n, LipschitzOnWith C (αₙ n) (Icc 0 T))
    (htip : ∀ n, ‖αₙ n 0‖ ≤ R)
    (hchord : ∀ n s, s ∈ Icc 0 T → ∀ t, t ∈ Icc 0 T →
      c * |s - t| ≤ dist (αₙ n s) (αₙ n t)) :
    ∃ α : ℝ → ℂ, ∃ φ : ℕ → ℕ, StrictMono φ ∧
      TendstoUniformlyOn (fun n => αₙ (φ n)) α atTop (Icc 0 T) ∧
      LipschitzOnWith C α (Icc 0 T) ∧ ContinuousOn α (Icc 0 T) ∧ ‖α 0‖ ≤ R ∧
      (∀ s ∈ Icc 0 T, ∀ t ∈ Icc 0 T, c * |s - t| ≤ dist (α s) (α t)) ∧
      InjOn α (Icc 0 T) := by
…