Prove2Me

Theorem 5.1 — solutions of GQVI(K, f) are the fixed points x∗=PK(x∗)(x∗−y∗)x^*=P_{K(x^*)}(x^*-y^*), y∗∈f(x∗)y^*\in f(x^*)

Proved
ChanPangGQVI.Contraction.theorem_5_1

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

fixed-pointp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1projectionvariational-inequality

Let ff and KK be point-to-set mappings of Rn\mathbb R^n into itself such that K(x)K(x) is a closed convex set for every xx. For a set SS and a point zz write PS(z)P_S(z) for the projection of zz on SS, the nearest point of SS to zz in the Euclidean norm. Then a pair (x∗,y∗)(x^*,y^*) solves the generalized quasi-variational inequality GQVI(K,f)\mathrm{GQVI}(K,f) if and only if

x∗=PK(x∗)(x∗−y∗)andy∗∈f(x∗).x^*=P_{K(x^*)}(x^*-y^*)\qquad\text{and}\qquad y^*\in f(x^*).

The theorem turns the GQVI into a fixed-point problem for a projection map. In this mission it is applied with λf\lambda f in place of ff to read the fixed point of Fλ(x)=PK(x)(x−λf(x))F_\lambda(x)=P_{K(x)}(x-\lambda f(x)) as a solution of the GQVI.

Formalization Note The equation x∗=PK(x∗)(x∗−y∗)x^*=P_{K(x^*)}(x^*-y^*) is stated relationally: x∗∈K(x∗)x^*\in K(x^*) and ∥x∗−(x∗−y∗)∥≤∥q−(x∗−y∗)∥\|x^*-(x^*-y^*)\|\le\|q-(x^*-y^*)\| for every q∈K(x∗)q\in K(x^*). For a closed convex set the nearest point is unique, so this is the paper's equation, and no junk value of a projection function is involved when K(x∗)K(x^*) is empty.

Preamble
import Mathlib
import Definitions.Def_ChanPangGQVI_Shared_GQVI
import Definitions.Def_ChanPangGQVI_Shared_Projection

open scoped RealInnerProductSpace
Formal statement
namespace ChanPangGQVI.Contraction

/-- **Theorem 5.1** (Chan and Pang 1982, p. 220). Let `f` and `K` be point-to-set mappings of
`ℝⁿ` into itself with `K(x)` closed and convex for all `x`. Then `(x*, y*)` solves `GQVI(K, f)`
if and only if `x* = P_{K(x*)}(x* - y*)` and `y* ∈ f(x*)`.

The equation `x* = P_{K(x*)}(x* - y*)` is written relationally, `IsProj (K x*) (x* - y*) x*`
("`x*` is a nearest point of `K(x*)` to `x* - y*`"), so that no junk value of a projection
function enters when `K(x*)` is empty; for a closed convex set the nearest point is unique, so
this is the paper's equation. -/
theorem theorem_5_1 {n : ℕ}
    (K f : EuclideanSpace ℝ (Fin n) → Set (EuclideanSpace ℝ (Fin n)))
    (hK_closed : ∀ x, IsClosed (K x)) (hK_convex : ∀ x, Convex ℝ (K x))
    (xs ys : EuclideanSpace ℝ (Fin n)) :
    ChanPangGQVI.Shared.IsGQVISolution K f xs ys ↔
      (ChanPangGQVI.Shared.IsProj (K xs) (xs - ys) xs ∧ ys ∈ f xs) := by sorry

end ChanPangGQVI.Contraction
Source
Chan and Pang, The generalized quasi-variational inequality problem, Math. Oper. Res. 7 (1982), p. 220, Theorem 5.1
Human review

  • Endorsed by Shuze Chen · Oct 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph