Public main theorem wrappers

def PLAcceleratedNesterovLean.«termPolyakLojasiewicz(_,_)[_]» : Lean.ParserDescr

Local Polyak-Łojasiewicz condition syntax for the public theorem statements.

Equations

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

def PLAcceleratedNesterovLean.«termC2Manifold(_,_)» : Lean.ParserDescr

C² manifold typeclass syntax for the public theorem statements.

Equations

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

def PLAcceleratedNesterovLean.«termC2Embedding(_,_,_)» : Lean.ParserDescr

C² smooth embedding syntax for the public theorem statements.

Equations

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

theorem PLAcceleratedNesterovLean.nesterov_pl_accelerated_rate {d : ℕ} (L μ : NNReal) : ∃ (ρ : ℝ), ∀ (f : EuclideanSpace ℝ (Fin d) → ℝ) (k : ℕ) (M : Type u_1) [inst : TopologicalSpace M] [inst_1 : ChartedSpace (EuclideanSpace ℝ (Fin k)) M] [IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin k))) 2 M] [Nonempty M] (ι : M → EuclideanSpace ℝ (Fin d)), Manifold.IsSmoothEmbedding (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin k))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin d))) 2 ι → Set.range ι = argminSet f → ∀ (U : Set (EuclideanSpace ℝ (Fin d))), IsOpen U → Set.range ι ⊆ U → ContDiffOn ℝ 2 f U → (0 < ↑μ ∧ DifferentiableOn ℝ f U ∧ ∀ x ∈ U, ‖gradient f x‖ ^ 2 ≥ 2 * ↑μ * (f x - fStar f)) → LipschitzOnWith L (gradient f) U → ∃ (Ū : Set (EuclideanSpace ℝ (Fin d))), IsOpen Ū ∧ Set.range ι ⊆ Ū ∧ Ū ⊆ U ∧ ∀ x₀ ∈ Ū, ∀ (t : ℕ), (nesterovSeqGen f (1 / ↑L) ρ { x := x₀, v := 0 } t).x ∈ U ∧ (nesterovSeqGen f (1 / ↑L) ρ { x := x₀, v := 0 } t).lookahead (1 / ↑L) ∈ U ∧ f (nesterovSeqGen f (1 / ↑L) ρ { x := x₀, v := 0 } t).x - fStar f ≤ 2 * Real.exp (-(↑t / √(↑L / ↑μ))) * (f x₀ - fStar f)

Embedded-manifold main theorem.

Assume the minimizer set of f is the range of a nonempty C² embedded k-manifold, U is an open neighborhood of this manifold, f is C² on U, satisfies the local μ-PL inequality on U, and has L-Lipschitz gradient on U. A tubular sub-neighborhood is constructed internally. Then there exists a momentum parameter ρ, depending only on L and μ, such that all sufficiently local starts converge with the explicit accelerated prefactor-two bound.

theorem PLAcceleratedNesterovLean.nesterov_pl_accelerated_rate_c3 {d : ℕ} (L μ : NNReal) : ∃ (ρ : ℝ), ∀ (f : EuclideanSpace ℝ (Fin d) → ℝ) (U : Set (EuclideanSpace ℝ (Fin d))), IsOpen U → argminSet f ⊆ U → ContDiffOn ℝ 3 f U → (0 < ↑μ ∧ DifferentiableOn ℝ f U ∧ ∀ x ∈ U, ‖gradient f x‖ ^ 2 ≥ 2 * ↑μ * (f x - fStar f)) → LipschitzOnWith L (gradient f) U → ∃ (Ū : Set (EuclideanSpace ℝ (Fin d))), IsOpen Ū ∧ argminSet f ⊆ Ū ∧ Ū ⊆ U ∧ ∀ x₀ ∈ Ū, ∀ (t : ℕ), (nesterovSeqGen f (1 / ↑L) ρ { x := x₀, v := 0 } t).x ∈ U ∧ (nesterovSeqGen f (1 / ↑L) ρ { x := x₀, v := 0 } t).lookahead (1 / ↑L) ∈ U ∧ f (nesterovSeqGen f (1 / ↑L) ρ { x := x₀, v := 0 } t).x - fStar f ≤ 2 * Real.exp (-(↑t / √(↑L / ↑μ))) * (f x₀ - fStar f)

C³ main theorem.

Assume U is an open neighborhood of the global minimizer set, f is C³ on U, satisfies the local μ-PL inequality on U, and has L-Lipschitz gradient on U. The minimizer geometry and tubular sub-neighborhood are constructed internally.