Prove2Me

Coercive self-adjoint operators are bijective

Proved
VectorSpaceOpt.coercive_selfadjoint_bijective

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

bijectivecoercive-operatorhilbert-spaceself-adjoint

Let H be a real Hilbert space and Q : H →L[ℝ] H a bounded self-adjoint operator. Suppose a constant m > 0 and an upper constant M satisfy the two-sided quadratic estimate

m‖x‖2≤⟨x,Qx⟩≤M‖x‖2m‖x‖² ≤ ⟨x,Qx⟩ ≤ M‖x‖²

for every x ∈ H. Then Q is bijective. In particular, every right-hand side b has one and only one solution of Q x = b. This result is recorded by Luenberger as Chapter 10, Problem 10 and is used implicitly when the conjugate-gradient theorem names Q⁻¹ b. The milestone makes solvability explicit before any algorithmic convergence claim and is reusable for other coercive quadratic methods.

Preamble
import Definitions.Def_VectorSpaceOpt_conjugate_gradient
Formal statement
namespace VectorSpaceOpt

/-- The operator-invertibility fact recorded as Chapter 10, Problem 10. -/
theorem coercive_selfadjoint_bijective
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (Q : H →L[ℝ] H) (m M : ℝ) (hm : 0 < m)
    (hself : IsRealSelfAdjoint Q) (hbounds : IsCoerciveBetween Q m M) :
    Function.Bijective Q := by
  sorry

end VectorSpaceOpt
Source
David G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), Chapter 10, Problem 10, printed p. 309 (physical PDF p. 327), used by §10.8, Theorem 1. 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 HH be a complete real inner-product space and Q:H→HQ:H→H a continuous real-linear map. For arbitrary m,M∈Rm,M∈ℝ, assume m>0m>0, assume QQ is self-adjoint, and assume every x∈Hx∈H satisfies m‖x‖2≤⟨x,Qx⟩≤M‖x‖2m‖x‖²≤⟨x,Qx⟩≤M‖x‖². Then the underlying function of QQ is bijective: it is both injective and surjective. There is no separately stated hypothesis m≤Mm≤M or M>0M>0; in a nonzero space these are constrained by the quadratic bounds, while the zero-dimensional space is also included.

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