Copyright (c) 2025. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE.

Definitions for Corollary 2.17: μ-PŁ ⟹ μ-MB

Formalization of definitions from: "Fast convergence to non-isolated minima: four equivalent conditions for C² functions" — Rebjock & Boumal

Contents

• localMinSet : set S of local minimizers at a given level
• MuPL : μ-Polyak–Łojasiewicz condition
• MuEB : μ-Error Bound condition
• MuQG : μ-Quadratic Growth condition
• IsLocalSubmanifoldAt: C¹ embedded submanifold at a point
• hessian : second Fréchet derivative (bilinear form)
• hessianKer : kernel of the Hessian
• IsMuMB : μ-Morse–Bott property

def PLAcceleratedNesterovLean.localMinSet {E : Type u_1} [NormedAddCommGroup E] (f : E → ℝ) (x₀ : E) : Set E

The set of local minimizers of f at the same function value as x₀. This is S from equation (4) in the paper: S = {x ∈ M : x is a local minimum of f and f(x) = f_S}

Equations

• PLAcceleratedNesterovLean.localMinSet f x₀ = {x : E | IsLocalMin f x ∧ f x = f x₀}

theorem PLAcceleratedNesterovLean.mem_localMinSet {E : Type u_1} [NormedAddCommGroup E] {f : E → ℝ} {x₀ x : E} : x ∈ localMinSet f x₀ ↔ IsLocalMin f x ∧ f x = f x₀

theorem PLAcceleratedNesterovLean.self_mem_localMinSet {E : Type u_1} [NormedAddCommGroup E] {f : E → ℝ} {x₀ : E} (hmin : IsLocalMin f x₀) : x₀ ∈ localMinSet f x₀

def PLAcceleratedNesterovLean.MuPL {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : E → ℝ) (μ : ℝ) (x₀ : E) : Prop

The μ-Polyak–Łojasiewicz condition (Definition 1.2 in the paper): ∀ x near x₀, f(x) − f(x₀) ≤ (2μ)⁻¹ ‖Df(x)‖² where ‖Df(x)‖ = ‖fderiv ℝ f x‖ equals the gradient norm by Riesz.

Equations

• PLAcceleratedNesterovLean.MuPL f μ x₀ = ∀ᶠ (x : E) in nhds x₀, f x - f x₀ ≤ (2 * μ)⁻¹ * ‖fderiv ℝ f x‖ ^ 2

def PLAcceleratedNesterovLean.MuEB {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : E → ℝ) (μ : ℝ) (x₀ : E) (S : Set E) : Prop

The μ-Error Bound condition (Definition 1.2 in the paper): ∀ x near x₀, μ · dist(x, S) ≤ ‖Df(x)‖

Equations

• PLAcceleratedNesterovLean.MuEB f μ x₀ S = ∀ᶠ (x : E) in nhds x₀, μ * Metric.infDist x S ≤ ‖fderiv ℝ f x‖

def PLAcceleratedNesterovLean.MuQG {E : Type u_1} [NormedAddCommGroup E] (f : E → ℝ) (μ : ℝ) (x₀ : E) (S : Set E) : Prop

The μ-Quadratic Growth condition (Definition 1.2 in the paper): ∀ x near x₀, (μ/2) · dist(x, S)² ≤ f(x) − f(x₀)

Equations

• PLAcceleratedNesterovLean.MuQG f μ x₀ S = ∀ᶠ (x : E) in nhds x₀, μ / 2 * Metric.infDist x S ^ 2 ≤ f x - f x₀

def PLAcceleratedNesterovLean.IsLocalSubmanifoldAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (S : Set E) (x₀ : E) (T : Submodule ℝ E) : Prop

S is a C¹ embedded submanifold of E near x₀ with tangent space T.

There exist a neighborhood U ∋ x₀ and a C¹ function φ : T → Tᗮ with φ(0) = 0 and Dφ(0) = 0, such that for every x ∈ U: x ∈ S ↔ π_{Tᗮ}(x − x₀) = φ(π_T(x − x₀))

Conditions:

• φ(0) = 0 ensures the graph passes through x₀, i.e., x₀ ∈ S.
• Dφ(0) = 0 ensures the tangent space to the graph at x₀ is exactly T.
• ContDiffAt ℝ 1 φ 0 gives C¹ regularity of the chart near the origin.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev PLAcceleratedNesterovLean.hessian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : E → ℝ) (x : E) : E →L[ℝ] E →L[ℝ] ℝ

The Hessian of f at x, as a bilinear form. Type: E →L[ℝ] (E →L[ℝ] ℝ). Applied twice: hessian f x v w : ℝ gives D²f(x)(v,w). For C² functions, this is symmetric and equals ⟨v, Hf(x)w⟩ via Riesz.

Equations

• PLAcceleratedNesterovLean.hessian f x = fderiv ℝ (fderiv ℝ f) x

noncomputable def PLAcceleratedNesterovLean.hessianKer {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : E → ℝ) (x : E) : Submodule ℝ E

The kernel of the Hessian at x, as a submodule of E.

Equations

• PLAcceleratedNesterovLean.hessianKer f x = (↑(PLAcceleratedNesterovLean.hessian f x)).ker

def PLAcceleratedNesterovLean.IsMuMB {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : E → ℝ) (μ : ℝ) (x₀ : E) : Prop

The μ-Morse–Bott property at x₀ (Definition 1.1 in the paper).

A C² function f : E → ℝ satisfies μ-MB at a local minimizer x₀ if:

1. S = localMinSet f x₀ is a C¹ submanifold near x₀ with tangent space T = ker(Hess f(x₀)),
2. The Hessian is μ-coercive on the normal space T⊥: D²f(x₀)(v,v) ≥ μ ‖v‖² for all v ∈ T⊥.

Equations

• One or more equations did not get rendered due to their size.