Classical DFP under Wolfe conditions

The formalization covers a strong Wolfe nonconvergence counterexample, its sharp one-half Hölder Hessian regularity, and planar convergence under a locally Lipschitz Hessian.

API documentation · Theorem dependency map · Lean source

These reading pages show the original Lean statements and proofs of the principal results and their regularity arguments. The API documentation covers the full imported module closure.

Reading guide

Main counterexample and convergence theorems
Global convergence predicates
Level-set convergence predicates
Hölder regularity and identity initialization
Sharpness of the one-half Hölder exponent
General planar secant degeneration
Planar convergence proof and C³ consequences
Hessian Hölder calculus

Formalization

Zichen Wang. Lean 4.32.0. Apache License 2.0.