Local Geometry Step 1: Hessian Bounds via Continuity #

Normal Hessian (from Morse-Bott) #

On M, D²f(m) ≥ μ in normal directions (PL ⟹ Morse-Bott). By continuity of D²f and compactness, this extends to U₊ with constant μ'.

Since D²f(m) ≥ 0 for m ∈ M (minimizer) and D²f is continuous, D²f(x) ≥ -εI on a neighborhood, with ε arbitrarily small.

Both arguments use: continuous function ≥ threshold on compact set ⟹ ≥ (threshold - δ) on a neighborhood.

theorem PLAcceleratedNesterovLean.continuous_pos_lower_bound_compact {X : Type u_1} [TopologicalSpace X] (g : X → ℝ) (K : Set X) (hK : IsCompact K) (hK_ne : K.Nonempty) (hg : Continuous g) (hpos : ∀ x ∈ K, 0 < g x) :

∃ (c : ℝ), 0 < c ∧ ∀ x ∈ K, c ≤ g x

A continuous function that is positive on a compact set is bounded below by a positive constant.

theorem PLAcceleratedNesterovLean.continuous_lower_bound_neighborhood {X : Type u_1} [TopologicalSpace X] [T2Space X] (g : X → ℝ) (K : Set X) (_hK : IsCompact K) (hg : Continuous g) (c : ℝ) (hc : ∀ x ∈ K, c ≤ g x) (δ : ℝ) (hδ : 0 < δ) :

∃ (V : Set X), IsOpen V ∧ K ⊆ V ∧ ∀ x ∈ V, c - δ ≤ g x

If g is continuous and g ≥ c on a compact set K, then g ≥ c - δ on a neighborhood of K for any δ > 0. (Open set version.)

theorem PLAcceleratedNesterovLean.hessian_psd_at_minimizer {d : ℕ} (f : E d → ℝ) (m : E d) (hmin : ∀ (y : E d), f m ≤ f y) (hf : ContDiffAt ℝ 2 f m) (ξ : E d) :

PSD at minimizers: if m is a global minimizer of a function f that is C² at m, then D²f(m) ≥ 0.