C¹ compactness for functions with bounded first and second derivatives

If a sequence of smooth functions on ℝ × ℝ and its gradients are uniformly bounded on a convex compact set K, and the second derivatives are also uniformly bounded on K, then a subsequence converges uniformly on K together with its gradients, and the limit is differentiable on the interior of K with derivative the limit of the gradients.

The two derivative bounds make both the functions and their gradients uniformly Lipschitz on K (via the mean value inequality), hence equicontinuous; Arzelà–Ascoli then extracts a uniformly convergent subsequence of the functions, and a further subsequence along which the gradients also converge uniformly. Identifying the limit of the gradients as the derivative of the limit function is the content of the uniform-limit differentiation theorem.

theorem CIV.exists_subseq_tendstoUniformlyOn_c1 (K : Set (ℝ × ℝ)) (hK : IsCompact K) (hKconv : Convex ℝ K) (V : ℕ → ℝ × ℝ → ℝ) (L : ℝ) (hL : 0 ≤ L) (hsmooth : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (V n)) (hV : ∀ (n : ℕ), ∀ y ∈ K, |V n y| ≤ L) (hDV : ∀ (n : ℕ), ∀ y ∈ K, ‖fderiv ℝ (V n) y‖ ≤ L) (hD2V : ∀ (n : ℕ), ∀ y ∈ K, ‖fderiv ℝ (fderiv ℝ (V n)) y‖ ≤ L) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (Vlim : ℝ × ℝ → ℝ) (DVlim : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ), TendstoUniformlyOn (fun (n : ℕ) => V (φ n)) Vlim Filter.atTop K ∧ TendstoUniformlyOn (fun (n : ℕ) => fderiv ℝ (V (φ n))) DVlim Filter.atTop K ∧ (∀ y ∈ K, |Vlim y| ≤ L) ∧ (∀ y ∈ K, ‖DVlim y‖ ≤ L) ∧ ∀ y ∈ interior K, HasFDerivAt Vlim (DVlim y) y

A subsequence along which a uniformly L-bounded, C²-bounded sequence of functions on ℝ × ℝ converges together with its gradients, uniformly on a convex compact set K, to a limit function which is differentiable on the interior of K with derivative the limit of the gradients.