Subgradient Characterization of a Positive Semidefinite Quadratic

This is a technical characterization of subgradients of the quadratic function quadraticAt.

Let $n\in\mathbb N$, let $A$ be a positive semidefinite real matrix indexed by $\operatorname{Fin}(n)$, and let $x_0,b,x,p\in\operatorname{EuclideanSpace}\,\mathbb R\,(\operatorname{Fin}(n))$. For $c\in\mathbb R$, the following are equivalent:

1. for every $y$,

where $q(z)=\operatorname{quadraticAt}(A,x_0,b,c,z)$; 2. $p=b+A(x-x_0)$, with $A$ interpreted through Matrix.toEuclideanLin.

Thus,

The lemma gives the exact affine formula for every subgradient of this positive semidefinite quadratic, including the degenerate case.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

private lemma quadraticAt_subgradient_iff {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ}
    (hA : A.PosSemidef) (x₀ b : EuclideanSpace ℝ (Fin n)) (c : ℝ)
    (x p : EuclideanSpace ℝ (Fin n)) :
    (∀ y, quadraticAt A x₀ b c x + ⟪p, y - x⟫ ≤ quadraticAt A x₀ b c y) ↔
      p = b + Matrix.toEuclideanLin A (x - x₀)

Module navigation

Module: Analysis/Convex/Alexandrov.

Previous: exists_pos_alexandrov_maximum_principle · Next: convexOn_quadraticAt.

Source excerpt, lines 1470–1474 · Frozen source 408915f.