RadialInnerCompactness.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform C¹ subsequence extraction for the inner amplitudes.

theorem OAI.DefocusingNLS.radial_inner_jet_subsequence line 16

Source documentation

The exact bounds proved for inner profiles give compactness of their amplitude/derivative pairs in the uniform topology.

theorem radial_inner_jet_subsequence (R : ℝ) (_hR : 1 ≤ R) (hR2 : R^2 ≤ 11)
    (H : ℕ → ℝ → ℝ) (hH : ∀ n, Differentiable ℝ (H n))
    (hDC : ∀ n, ContinuousOn (deriv (H n)) (Icc 0 R))
    (hB : ∀ n r, r ∈ Icc 0 R → ‖H n r‖ ≤ 1 ∧ ‖deriv (H n) r‖ ≤ r/24)
    (hL : ∀ n, LipschitzOnWith 1 (deriv (H n)) (Icc 0 R)) :
    ∃ J : (Icc (0 : ℝ) R) →ᵇ ℝ × ℝ, ∃ φ : ℕ → ℕ, StrictMono φ ∧
      TendstoUniformly (fun n (r : Icc (0 : ℝ) R) =>
        (H (φ n) r, deriv (H (φ n)) r)) J atTop := by
…