Hilbert projection theorem

TheoremExistence and uniqueness of the nearest point#✓fully proved

Let \(K\) be a nonempty complete convex subset of a real inner product space \(F\). For every \(x \in F\) there is exactly one \(p \in K\) with \(\|x - p\| = \inf_{w \in K} \|x - w\|\), that is, exactly one point of \(K\) nearest to \(x\).

theorem exists_unique_nearest_point_of_complete_convex {K : Set F}
    (hKne : K.Nonempty) (hKc : IsComplete K) (hKv : Convex ℝ K) (x : F) :
    ∃! p, p ∈ K ∧ ‖x - p‖ = ⨅ w : K, ‖x - w‖

TheoremTotalized existence of the convex projection#✓fully proved

For every subset \(K\) of a real inner product space \(F\) and every \(x \in F\), there is a point \(p \in F\) such that, if \(K\) is nonempty, complete and convex, then \(p \in K\) and \(\|x - p\| = \inf_{w \in K} \|x - w\|\).

theorem exists_convexProjection_spec (K : Set F) (x : F) :
    ∃ p : F, (K.Nonempty → IsComplete K → Convex ℝ K →
      p ∈ K ∧ ‖x - p‖ = ⨅ w : K, ‖x - w‖)

Used by 2

Used byNearest-point projection onto a convex set · Defining property of the convex projection

DefinitionNearest-point projection onto a convex set#✓fully proved

For a subset \(K\) of a real inner product space \(F\) and a point \(x \in F\), the nearest-point projection \(P_K(x)\) is a chosen point of \(F\) such that, whenever \(K\) is nonempty, complete and convex, \(P_K(x) \in K\) and \(\|x - P_K(x)\| = \inf_{w \in K} \|x - w\|\); it is then the unique point of \(K\) nearest to \(x\). When \(K\) fails one of these hypotheses, the value of \(P_K(x)\) is unspecified.

noncomputable def convexProjection (K : Set F) (x : F) : F :=
  Classical.choose (exists_convexProjection_spec K x)

Uses 1 · Used by 17

Statement usesTotalized existence of the convex projection

Used byVariational characterization of projection onto a convex cone · Variational characterization determines the cone projection · Cone projection residual pairs nonpositively with the cone · Cone projection residual is orthogonal to the projection · Moreau decomposition, polar form · Moreau decomposition · Cone projection residual lies in the negative polar · Stampacchia's theorem, operator form · Nearest points coincide with the convex projection · The convex projection fixes the points of the set · Firm nonexpansiveness of the convex projection · Idempotence of the convex projection · The convex projection lies in the set · The convex projection minimizes the distance to the set · Defining property of the convex projection · Variational inequality for the convex projection · The convex projection is \(1\)-Lipschitz

TheoremDefining property of the convex projection#✓fully proved

Let \(K\) be a nonempty complete convex subset of a real inner product space \(F\), and let \(P_K\) be the nearest-point projection onto \(K\). For every \(x \in F\), \(P_K(x) \in K\) and \(\|x - P_K(x)\| = \inf_{w \in K} \|x - w\|\).

theorem convexProjection_spec {K : Set F} (hKne : K.Nonempty) (hKc : IsComplete K)
    (hKv : Convex ℝ K) (x : F) :
    convexProjection K x ∈ K ∧ ‖x - convexProjection K x‖ = ⨅ w : K, ‖x - w‖

Uses 2 · Used by 2

Statement usesNearest-point projection onto a convex set

Proof usesTotalized existence of the convex projection

Used byThe convex projection lies in the set · The convex projection minimizes the distance to the set

TheoremThe convex projection lies in the set#✓fully proved

Let \(K\) be a nonempty complete convex subset of a real inner product space \(F\), and let \(P_K\) be the nearest-point projection onto \(K\). Then \(P_K(x) \in K\) for every \(x \in F\).

theorem convexProjection_mem {K : Set F} (hKne : K.Nonempty) (hKc : IsComplete K)
    (hKv : Convex ℝ K) (x : F) : convexProjection K x ∈ K

Uses 2 · Used by 9

Statement usesNearest-point projection onto a convex set

Proof usesDefining property of the convex projection

Used byCone projection residual pairs nonpositively with the cone · Cone projection residual is orthogonal to the projection · Moreau decomposition, polar form · Stampacchia's theorem, operator form · Nearest points coincide with the convex projection · Firm nonexpansiveness of the convex projection · Idempotence of the convex projection · Variational inequality for the convex projection · The convex projection is \(1\)-Lipschitz

TheoremThe convex projection minimizes the distance to the set#✓fully proved

Let \(K\) be a nonempty complete convex subset of a real inner product space \(F\), and let \(P_K\) be the nearest-point projection onto \(K\). Then \(\|x - P_K(x)\| = \inf_{w \in K} \|x - w\|\) for every \(x \in F\).

theorem convexProjection_norm_eq_iInf {K : Set F} (hKne : K.Nonempty)
    (hKc : IsComplete K) (hKv : Convex ℝ K) (x : F) :
    ‖x - convexProjection K x‖ = ⨅ w : K, ‖x - w‖

Uses 2 · Used by 4

Statement usesNearest-point projection onto a convex set

Proof usesDefining property of the convex projection

Used byNearest points coincide with the convex projection · Firm nonexpansiveness of the convex projection · Variational inequality for the convex projection · The convex projection is \(1\)-Lipschitz

TheoremVariational inequality for the convex projection#✓fully proved

Let \(K\) be a nonempty complete convex subset of a real inner product space \(F\), and let \(P_K\) be the nearest-point projection onto \(K\). For every \(x \in F\) and every \(w \in K\), \(\langle x - P_K(x), w - P_K(x) \rangle \le 0\).

theorem convexProjection_variational {K : Set F} (hKne : K.Nonempty)
    (hKc : IsComplete K) (hKv : Convex ℝ K) (x : F) :
    ∀ w ∈ K, ⟪x - convexProjection K x, w - convexProjection K x⟫_ℝ ≤ 0

Uses 3 · Used by 2

Statement usesNearest-point projection onto a convex set

Proof usesThe convex projection lies in the set · The convex projection minimizes the distance to the set

Used byVariational characterization of projection onto a convex cone · Stampacchia's theorem, operator form

TheoremNearest points coincide with the convex projection#✓fully proved

Let \(K\) be a nonempty complete convex subset of a real inner product space \(F\), let \(P_K\) be the nearest-point projection onto \(K\), and let \(x \in F\). If \(p \in K\) satisfies \(\|x - p\| = \inf_{w \in K} \|x - w\|\), then \(P_K(x) = p\).

theorem convexProjection_eq_of_isNearestPoint {K : Set F} (hKne : K.Nonempty)
    (hKc : IsComplete K) (hKv : Convex ℝ K) {x p : F} (hpK : p ∈ K)
    (hp : ‖x - p‖ = ⨅ w : K, ‖x - w‖) : convexProjection K x = p

Uses 3 · Used by 2

Statement usesNearest-point projection onto a convex set

Proof usesThe convex projection lies in the set · The convex projection minimizes the distance to the set

Used byVariational characterization of projection onto a convex cone · The convex projection fixes the points of the set

TheoremThe convex projection fixes the points of the set#✓fully proved

Let \(K\) be a nonempty complete convex subset of a real inner product space \(F\), and let \(P_K\) be the nearest-point projection onto \(K\). Then \(P_K(x) = x\) for every \(x \in K\).

theorem convexProjection_eq_self_of_mem {K : Set F} (hKne : K.Nonempty)
    (hKc : IsComplete K) (hKv : Convex ℝ K) {x : F} (hx : x ∈ K) :
    convexProjection K x = x

Uses 2 · Used by 1

Statement usesNearest-point projection onto a convex set

Proof usesNearest points coincide with the convex projection

Used byIdempotence of the convex projection

TheoremIdempotence of the convex projection#✓fully proved

Let \(K\) be a nonempty complete convex subset of a real inner product space \(F\), and let \(P_K\) be the nearest-point projection onto \(K\). Then \(P_K(P_K(x)) = P_K(x)\) for every \(x \in F\).

theorem convexProjection_idem {K : Set F} (hKne : K.Nonempty) (hKc : IsComplete K)
    (hKv : Convex ℝ K) (x : F) :
    convexProjection K (convexProjection K x) = convexProjection K x

Uses 3

Statement usesNearest-point projection onto a convex set

Proof usesThe convex projection fixes the points of the set · The convex projection lies in the set

TheoremNonexpansiveness of nearest-point selection#✓fully proved

Let \(K\) be a convex subset of a real inner product space \(F\), let \(x, y \in F\), and let \(p, q \in K\) satisfy \(\|x - p\| = \inf_{w \in K} \|x - w\|\) and \(\|y - q\| = \inf_{w \in K} \|y - w\|\), so that \(p\) is a point of \(K\) nearest to \(x\) and \(q\) is a point of \(K\) nearest to \(y\). Then \(\|p - q\| \le \|x - y\|\).

theorem norm_sub_le_of_isNearestPoint {K : Set F} (hKv : Convex ℝ K)
    {x y p q : F} (hpK : p ∈ K) (hqK : q ∈ K)
    (hp : ‖x - p‖ = ⨅ w : K, ‖x - w‖)
    (hq : ‖y - q‖ = ⨅ w : K, ‖y - w‖) :
    ‖p - q‖ ≤ ‖x - y‖

Used by 1

Used byThe convex projection is \(1\)-Lipschitz

TheoremFirm nonexpansiveness of nearest-point selection#✓fully proved

Let \(K\) be a convex subset of a real inner product space \(F\), let \(x, y \in F\), and let \(p, q \in K\) satisfy \(\|x - p\| = \inf_{w \in K} \|x - w\|\) and \(\|y - q\| = \inf_{w \in K} \|y - w\|\), so that \(p\) is a point of \(K\) nearest to \(x\) and \(q\) is a point of \(K\) nearest to \(y\). Then \(\|p - q\|^2 + \|(x - p) - (y - q)\|^2 \le \|x - y\|^2\).

theorem norm_sub_sq_add_norm_sub_sq_le_of_isNearestPoint {K : Set F}
    (hKv : Convex ℝ K) {x y p q : F} (hpK : p ∈ K) (hqK : q ∈ K)
    (hp : ‖x - p‖ = ⨅ w : K, ‖x - w‖)
    (hq : ‖y - q‖ = ⨅ w : K, ‖y - w‖) :
    ‖p - q‖ ^ 2 + ‖(x - p) - (y - q)‖ ^ 2 ≤ ‖x - y‖ ^ 2

Used by 1

Used byFirm nonexpansiveness of the convex projection

TheoremThe convex projection is \(1\)-Lipschitz#✓fully proved

Let \(K\) be a nonempty complete convex subset of a real inner product space \(F\), and let \(P_K\) be the nearest-point projection onto \(K\). Then \(\|P_K x - P_K y\| \le \|x - y\|\) for all \(x, y \in F\), that is, \(P_K\) is \(1\)-Lipschitz.

theorem lipschitzWith_convexProjection {K : Set F} (hKne : K.Nonempty)
    (hKc : IsComplete K) (hKv : Convex ℝ K) :
    LipschitzWith 1 (convexProjection K)

Uses 4 · Used by 1

Statement usesNearest-point projection onto a convex set

Proof usesThe convex projection lies in the set · The convex projection minimizes the distance to the set · Nonexpansiveness of nearest-point selection

Used byStampacchia's theorem, operator form

TheoremFirm nonexpansiveness of the convex projection#✓fully proved

Let \(K\) be a nonempty complete convex subset of a real inner product space \(F\), and let \(P_K\) be the nearest-point projection onto \(K\). For all \(x, y \in F\), \(\|P_K(x) - P_K(y)\|^2 + \|(x - P_K(x)) - (y - P_K(y))\|^2 \le \|x - y\|^2\).

theorem convexProjection_firmly_nonexpansive {K : Set F} (hKne : K.Nonempty)
    (hKc : IsComplete K) (hKv : Convex ℝ K) (x y : F) :
    ‖convexProjection K x - convexProjection K y‖ ^ 2 +
        ‖(x - convexProjection K x) - (y - convexProjection K y)‖ ^ 2
      ≤ ‖x - y‖ ^ 2

Uses 4

Statement usesNearest-point projection onto a convex set

Proof usesThe convex projection lies in the set · The convex projection minimizes the distance to the set · Firm nonexpansiveness of nearest-point selection

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.