Shared definitions for external theorem compatibility

These mirror definitions from the source project so external theorems can be stated and proved using the same types.

Ambient space

@[reducible, inline]

abbrev PLAcceleratedNesterovLean.Ed (d : ℕ) : Type

The ambient Euclidean space ℝ^d (matching PLAcceleratedNesterovLean).

Equations

• PLAcceleratedNesterovLean.Ed d = EuclideanSpace ℝ (Fin d)

Tubular neighborhoods

structure PLAcceleratedNesterovLean.IsTubularNeighborhood {E : Type u_1} [PseudoMetricSpace E] (S U : Set E) : Prop

A tubular neighborhood of S is an open set U ⊇ S such that every point in U has a unique nearest point in S.

• isOpen : IsOpen U
• subset : S ⊆ U
• uniqueProj (x : E) : x ∈ U → ∃! p : E, p ∈ S ∧ dist x p = Metric.infDist x S

Optimization definitions

def PLAcceleratedNesterovLean.Ext.argminSet {E : Type u_1} (f : E → ℝ) : Set E

The set of global minimizers of f.

Equations

• PLAcceleratedNesterovLean.Ext.argminSet f = {x : E | ∀ (y : E), f x ≤ f y}

noncomputable def PLAcceleratedNesterovLean.Ext.fStar {E : Type u_1} (f : E → ℝ) : ℝ

The infimal value f⋆ = inf_x f(x).

Equations

• PLAcceleratedNesterovLean.Ext.fStar f = ⨅ (x : E), f x

def PLAcceleratedNesterovLean.Ext.PolyakLojasiewicz {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : E → ℝ) (μ : ℝ) (U : Set E) : Prop

μ-PŁ condition using ‖fderiv‖ (PLMB compatibility layer).

Equations

• PLAcceleratedNesterovLean.Ext.PolyakLojasiewicz f μ U = (0 < μ ∧ ∀ x ∈ U, ‖fderiv ℝ f x‖ ^ 2 ≥ 2 * μ * (f x - PLAcceleratedNesterovLean.Ext.fStar f))

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

The gradient of f at x (Riesz representative of fderiv ℝ f x).

Equations

• PLAcceleratedNesterovLean.Ext.gradient f x = (InnerProductSpace.toDual ℝ E).symm (fderiv ℝ f x)

noncomputable def PLAcceleratedNesterovLean.Ext.hessianQuadForm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : E → ℝ) (x ξ : E) : ℝ

The Hessian quadratic form ξᵀ D²f(x) ξ = ⟨D(∇f)(x)·ξ, ξ⟩.

Equations

• PLAcceleratedNesterovLean.Ext.hessianQuadForm f x ξ = inner ℝ ((fderiv ℝ (PLAcceleratedNesterovLean.Ext.gradient f) x) ξ) ξ