Generalized inverse function theorem

Proved

VectorSpaceOpt.generalized_inverse_function

by wenxinzhang · Aug 25, 2026 · Mathlib c5ea003 (Lean v4.30.0)

banach-spacefrechet-derivativeinverse-functionmetric-regularity

Let $X$ and $Y$ be real Banach spaces, $U \subseteq X$ open, and $T \colon X \to Y$ continuously Fréchet differentiable on $U$ . Suppose $x_0 \in U$ , the derivative of $T$ at $x_0$ is the continuous linear map $T^\prime$ , and $T^\prime$ is onto. Then there are $\varepsilon > 0$ and $K \geq 0$ such that every target $y$ with $dist (y, T(x_0)) < \varepsilon$ has a preimage $x \in U$ satisfying $T(x) = y$ and the quantitative bound

\lVert x-x₀\rVert \le K\lVert y-Tx₀\rVert.

This is Luenberger's Lyusternik–Graves local-surjectivity theorem and supplies the nonlinear feasibility perturbations needed by the tangent-stationarity milestone.

Preamble

import Mathlib

open Set

Formal statement

namespace VectorSpaceOpt

/-- Luenberger, Chapter 9, §9.2, Theorem 1. -/
theorem generalized_inverse_function
    {X Y : Type*}
    [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X]
    [NormedAddCommGroup Y] [NormedSpace ℝ Y] [CompleteSpace Y]
    (U : Set X) (T : X → Y) (x₀ : X) (T' : X →L[ℝ] Y)
    (hU : IsOpen U) (hx₀ : x₀ ∈ U)
    (hT : ContDiffOn ℝ 1 T U) (hT' : HasFDerivAt T T' x₀)
    (hregular : Function.Surjective T') :
    ∃ ε K : ℝ, 0 < ε ∧ 0 ≤ K ∧
      ∀ y : Y, dist y (T x₀) < ε →
        ∃ x : X, x ∈ U ∧ T x = y ∧ ‖x - x₀‖ ≤ K * ‖y - T x₀‖ := by
  sorry

end VectorSpaceOpt

Source

David G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), Chapter 9, §9.2, Theorem 1, printed pp. 240–242 (physical PDF pp. 258–260). Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf

Read-back

What the Lean code literally says, in plain math · gpt-5

Let $X,Y$ be real Banach spaces, $U⊆X$ , $T:X→Y$ , $x₀∈X$ , and $T':X→Y$ a continuous real-linear map. Assume $U$ is open, $x₀∈U$ , $T$ is continuously Fréchet differentiable through order one on $U$ , $T'$ is the Fréchet derivative of $T$ at $x₀$ , and $T'$ is surjective. Then there exist real numbers $ε,K$ with $ε>0$ and $K≥0$ such that every $y∈Y$ satisfying the strict inequality $dist(y,T(x₀))<ε$ has at least one preimage $x∈U$ with $T(x)=y$ and $‖x-x₀‖≤K‖y-T(x₀)‖$ . The same $ε$ and $K$ work for all such $y$ ; neither uniqueness of $x$ nor continuity of a chosen right inverse is asserted.

Human review

Endorsed by Shuze Chen · Aug 26, 2026
Endorsed by wenxinzhang · Aug 26, 2026
Confirmed by the mission captain (proposal self-audit).

View graph