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

PLMBBridge — Adapter/Bridge Lemmas for PLAcceleratedNesterovLeans Integration

Overview

This file provides adapter/bridge lemmas connecting PLMB's generic Morse–Bott and tubular-neighborhood theory (over an arbitrary finite-dimensional real inner-product space E) to the concrete setting used by PLAcceleratedNesterovLeans (where E d := EuclideanSpace ℝ (Fin d)).

Bridge classification table

Bridge	Difficulty	Mechanism
IsTubNeighSub.toIsTubularNeighborhood	Trivial	Field-for-field
IsTubNeighSub.shrink	Short proof	Restriction to open subset
IsTubNeighSub.radius	Short proof	Per-point ball from openness
tubularProj @ Ed d	Trivial	Type specialization
tubular_neighborhood_projection @ Ed d	Trivial	Type specialization
‖Ext.gradient f x‖ = ‖fderiv ℝ f x‖	One-liner	LinearIsometryEquiv.norm_map
Ext.PL → MuPL	Already in Thm3	ExternalThm3.pl_to_muPL
hessian f x ξ ξ = Ext.hessianQuadForm	Already in Thm3	hessianQuadForm_eq_hessian
Ext.PL + argmin → IsMuMB	Composition	Pipeline of above bridges
muPL_implies_muMB @ Ed d	Trivial	Type specialization

References

• Rebjock & Boumal, "Fast convergence to non-isolated minima: four equivalent conditions for C² functions"
• PLAcceleratedNesterovLeans: PLAcceleratedNesterovLean/Core/Defs.lean, PLAcceleratedNesterovLean/Convergence/LocalGeometry/Main.lean

theorem PLAcceleratedNesterovLean.IsTubularNeighborhoodOfSubmanifold.toIsTubularNeighborhood {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S U : Set E} (h : IsTubularNeighborhoodOfSubmanifold S U) : IsTubularNeighborhood S U

theorem PLAcceleratedNesterovLean.IsTubularNeighborhoodOfSubmanifold.shrink {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S U : Set E} (h : IsTubularNeighborhoodOfSubmanifold S U) {U' : Set E} (hU'_open : IsOpen U') (hSU' : S ⊆ U') (hU'U : U' ⊆ U) : IsTubularNeighborhoodOfSubmanifold S U'

theorem PLAcceleratedNesterovLean.IsTubularNeighborhoodOfSubmanifold.radius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S U : Set E} (h : IsTubularNeighborhoodOfSubmanifold S U) (m : E) : m ∈ S → ∃ r > 0, Metric.ball m r ⊆ U

@[reducible, inline]

noncomputable abbrev PLAcceleratedNesterovLean.tubularProjEd {d : ℕ} {S U : Set (Ed d)} (hTN : IsTubularNeighborhoodOfSubmanifold S U) (hne : S.Nonempty) : Ed d → Ed d

Nearest-point projection specialized to the Euclidean ambient space Ed d.

Equations

• PLAcceleratedNesterovLean.tubularProjEd hTN hne = PLAcceleratedNesterovLean.tubularProj hTN hne

theorem PLAcceleratedNesterovLean.tubular_neighborhood_projection_Ed {d : ℕ} {S U : Set (Ed d)} (hTN : IsTubularNeighborhoodOfSubmanifold S U) (hne : S.Nonempty) : ∃ (π : Ed d → Ed d), (∀ x ∈ U, π x ∈ S ∧ ‖x - π x‖ = Metric.infDist x S) ∧ (∀ x ∈ S, π x = x) ∧ (∀ (x : Ed d), π x ∈ S) ∧ (∀ m ∈ S, ∀ x ∈ U, ‖x - π x‖ ≤ ‖x - m‖) ∧ (∀ m ∈ S, ∃ δ > 0, ∀ x ∈ U, x ∈ Metric.ball m δ → ∀ t ∈ Set.Icc 0 1, (1 - t) • π x + t • x ∈ U) ∧ (∀ x ∈ U, ∀ t ∈ Set.Icc 0 1, have y := (1 - t) • π x + t • x; ‖y - π x‖ = Metric.infDist y S) ∧ (∀ x ∈ U, (fderiv ℝ π (π x)) (x - π x) = 0) ∧ (∀ m ∈ S, DifferentiableAt ℝ π m) ∧ (∀ m ∈ S, ∀ (u v : Ed d), inner ℝ ((fderiv ℝ π m) u) v = inner ℝ u ((fderiv ℝ π m) v)) ∧ ∀ m ∈ S, ContDiffAt ℝ 1 π m

theorem PLAcceleratedNesterovLean.norm_gradient_eq_norm_fderiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : E → ℝ) (x : E) : ‖ExternalThm3.gradient f x‖ = ‖fderiv ℝ f x‖

The norm of the gradient equals the operator norm of the Fréchet derivative. This follows from toDual ℝ E being a linear isometry.

theorem PLAcceleratedNesterovLean.norm_extGradient_eq_norm_fderiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : E → ℝ) (x : E) : ‖Ext.gradient f x‖ = ‖fderiv ℝ f x‖

Variant with Ext.gradient (BridgeDefs.lean).

theorem PLAcceleratedNesterovLean.norm_sq_gradient_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : E → ℝ) (x : E) : ‖ExternalThm3.gradient f x‖ ^ 2 = ‖fderiv ℝ f x‖ ^ 2

Squared norms version.

theorem PLAcceleratedNesterovLean.externalThm3_gradient_eq_gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : E → ℝ) (x : E) : ExternalThm3.gradient f x = gradient f x

Connection to Mathlib's gradient (from Analysis.Calculus.Gradient.Basic).

Mathlib defines gradient 𝕜 f x := (toDual 𝕜 E).symm (fderiv 𝕜 f x). Our ExternalThm3.gradient has the same definition (specialized to ℝ). They are definitionally equal.

theorem PLAcceleratedNesterovLean.ext_gradient_eq_gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : E → ℝ) (x : E) : Ext.gradient f x = gradient f x

Connection between Ext.gradient and Mathlib's gradient.

theorem PLAcceleratedNesterovLean.norm_mathlibGradient_eq_norm_fderiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : E → ℝ) (x : E) : ‖gradient f x‖ = ‖fderiv ℝ f x‖

Norm bridge for Mathlib's gradient.

theorem PLAcceleratedNesterovLean.muPL_implies_muMB_Ed {d : ℕ} (f : Ed d → ℝ) (μ : ℝ) (x₀ : Ed d) (hμ : 0 < μ) (hf : ContDiffAt ℝ 2 f x₀) (hmin : IsLocalMin f x₀) (hPL : MuPL f μ x₀) : IsMuMB f μ x₀

Corollary 2.17 at Ed d: μ-PŁ ⟹ μ-Morse–Bott.

theorem PLAcceleratedNesterovLean.MuPL.implies_submanifold_Ed {d : ℕ} (f : Ed d → ℝ) (μ : ℝ) (x₀ : Ed d) (hμ : 0 < μ) (hf : ContDiffAt ℝ 2 f x₀) (hmin : IsLocalMin f x₀) (hPL : MuPL f μ x₀) : IsLocalSubmanifoldAt (localMinSet f x₀) x₀ (hessianKer f x₀)

Theorem 2.16 at Ed d: μ-PŁ ⟹ local-min set is a C¹ submanifold.

theorem PLAcceleratedNesterovLean.hessian_coercive_Ed {d : ℕ} (f : Ed d → ℝ) (μ : ℝ) (x₀ : Ed d) (hμ : 0 < μ) (hf : ContDiffAt ℝ 2 f x₀) (hmin : IsLocalMin f x₀) (hPL : MuPL f μ x₀) (v : Ed d) : v ∈ (hessianKer f x₀)ᗮ → ((hessian f x₀) v) v ≥ μ * ‖v‖ ^ 2

Hessian coercivity at Ed d: PŁ ⟹ D²f(x₀) ≥ μ on ker(Hess)⊥.

theorem PLAcceleratedNesterovLean.globalPL_implies_muMB_Ed {d : ℕ} (f : Ed d → ℝ) (μ : ℝ) (U : Set (Ed d)) (x₀ : Ed d) (hμ : 0 < μ) (hf : ContDiffAt ℝ 2 f x₀) (hPL : ExternalThm3.PolyakLojasiewicz f μ U) (hU : U ∈ nhds x₀) (hmin : x₀ ∈ ExternalThm3.argminSet f) : IsMuMB f μ x₀

Full pipeline at Ed d: global PL + global minimizer ⟹ μ-MB.

Given:

• f : Ed d → ℝ is C²
• f satisfies the Polyak–Łojasiewicz condition on U with constant μ
• x₀ is a global minimizer (i.e. x₀ ∈ ExternalThm3.argminSet f)
• U ∈ 𝓝 x₀ (x₀ is in the interior of U)

Conclude: f satisfies μ-Morse–Bott at x₀.

This is the bridge lemma that PLAcceleratedNesterovLeans' local_fiberwise_geometry can use to invoke PLMB's structural results.

theorem PLAcceleratedNesterovLean.globalPL_implies_submanifold_Ed {d : ℕ} (f : Ed d → ℝ) (μ : ℝ) (U : Set (Ed d)) (x₀ : Ed d) (hμ : 0 < μ) (hf : ContDiffAt ℝ 2 f x₀) (hPL : ExternalThm3.PolyakLojasiewicz f μ U) (hU : U ∈ nhds x₀) (hmin : x₀ ∈ ExternalThm3.argminSet f) : IsLocalSubmanifoldAt (localMinSet f x₀) x₀ (hessianKer f x₀)

Submanifold conclusion via global PL + tubular neighborhood. Under the same hypotheses, localMinSet f x₀ is a C¹ submanifold with tangent space hessianKer f x₀.

theorem PLAcceleratedNesterovLean.ext_argminSet_eq {E : Type u_1} (f : E → ℝ) : Ext.argminSet f = ExternalThm3.argminSet f

theorem PLAcceleratedNesterovLean.ext_fStar_eq {E : Type u_1} (f : E → ℝ) : Ext.fStar f = ExternalThm3.fStar f

theorem PLAcceleratedNesterovLean.ext_gradient_eq_externalThm3 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : E → ℝ) (x : E) : Ext.gradient f x = ExternalThm3.gradient f x

theorem PLAcceleratedNesterovLean.ext_hessianQuadForm_eq_externalThm3 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : E → ℝ) (x ξ : E) : Ext.hessianQuadForm f x ξ = ExternalThm3.hessianQuadForm f x ξ