Corollary 5, p.4 — Hessian accuracy implies uniformly bounded model Hessians

Let $f:\mathbb R^d\to\mathbb R$ be $C^2$, $x_0\in\mathbb R^d$, $\bar\Delta>0$. If the class of models $\{\tilde f_\Delta\}_{(0,\bar\Delta]}$ provides order-$N$ Hessian accuracy of $f$ at $x_0$, then the class $\{\|\nabla^2\tilde f_\Delta\|\}_{(0,\bar\Delta]}$ is uniformly bounded at $x_0$. If it provides order-$N$ Hessian accuracy of $f$ near $x_0$, then $\{\|\nabla^2\tilde f_\Delta\|\}_{(0,\bar\Delta]}$ is uniformly bounded near $x_0$.

This is the Hessian analogue of the function and gradient statements of the corollary.

Differences from the source:

• encoding: the space ℝ^d, the closed ball B_Δ(x₀), a class of models {f̃_Δ}_{(0,Δ̄]} → EuclideanSpace ℝ (Fin d), Metric.closedBall x0 Δ, a map ℝ → E → ℝ used only on Set.Ioc 0 Δbar; reason: Lean convention; same instances
• encoding: the Hessian ∇²f as a matrix → fderiv ℝ (fderiv ℝ f) as a bilinear map; reason: the matrix and the second derivative determine each other; same instances
• reading: ‖·‖ on Hessians is unspecified → the operator norm of E →L[ℝ] E →L[ℝ] ℝ; reason: the spectral norm is the standard matrix norm in this literature and the one the proof's ‖ab^⊤‖ = ‖a‖‖b‖ uses; on a matrix it equals the operator norm of the bilinear map
• encoding: provides order-N accuracy: ∃ κ ≥ 0, in the hypothesis of an implication → κ universally quantified over the implication; reason: (∀ κ, P κ → Q) is equivalent to ((∃ κ, P κ) → Q)
• generalization: ∇f̃_Δ (resp. ∇²f̃_Δ) is assumed to exist → no regularity of the models is assumed; reason: the bound holds for fderiv as a total function, so the statement for differentiable models is a special case