Convexity of Positive Semidefinite Quadratics

This proves convexity of a quadratic with positive semidefinite matrix.

Let $n\in\mathbb N$, let $A$ be a real $n\times n$ matrix indexed by Fin n, and assume $A$ is positive semidefinite. For any $x_0,b\in\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin}n)$ and $c\in\mathbb R$, the function quadraticAt A x₀ b c is convex on the whole space:

This is a finite-dimensional algebraic lemma for constructing convex quadratic potentials. No positivity or dimension restriction on $n$ is assumed.

Original Lean declaration header

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

theorem convexOn_quadraticAt {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} (hA : A.PosSemidef)
    (x₀ b : EuclideanSpace ℝ (Fin n)) (c : ℝ) : ConvexOn ℝ univ (quadraticAt A x₀ b c)

Module navigation

Module: Analysis/Convex/Alexandrov.

Previous: quadraticAt_subgradient_iff · Next: volume_subgradientImage_quadraticAt_aux.

Source excerpt, lines 1585–1586 · Frozen source 408915f.