Lemma 8 — generalized projections onto a convex set do not increase A-distances to points of the set

Proved

LogRegretOCO.ONS.gen_proj_ineq

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

convex-analysisgeneralized-projectionp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $\mathcal P\subseteq\mathbb R^n$ be convex, let $A$ be a positive semidefinite $n\times n$ matrix, let $y\in\mathbb R^n$ , and let $z=\Pi^{A}_{\mathcal P}(y)$ be a generalized projection of $y$ onto $\mathcal P$ with respect to $A$ , i.e. $z\in\mathcal P$ minimises $(y-x)^\top A(y-x)$ over $x\in\mathcal P$ . Then for every $a\in\mathcal P$ ,

(y-a)^\top A\,(y-a)\ \ge\ (z-a)^\top A\,(z-a).

This is the generalized Pythagorean inequality; in the analysis of the Online Newton Step it shows that the projection step can only decrease the $A_t$ -distance to the comparator.

Formalization Note "Positive semidefinite" is Mathlib's Matrix.PosSemidef (symmetric with nonnegative quadratic form). The paper's display defines $\Pi^A_{\mathcal P}[y]$ with "min"; it means the minimising point (argmin), which is what the predicate encodes. No existence or uniqueness of the projection is assumed: the conclusion holds for every minimiser.

Preamble

import Mathlib
import Definitions.Def_LogRegretOCO_ONS_Basic

Formal statement

namespace LogRegretOCO.ONS

/-- Lemma 8 (folklore; Hazan–Agarwal–Kale 2007, p. 188). Let `P ⊆ ℝⁿ` be convex, `A` positive
semidefinite, `y ∈ ℝⁿ`, and `z` a generalized projection of `y` onto `P` with respect to `A`.
Then `(y − a)ᵀ A (y − a) ≥ (z − a)ᵀ A (z − a)` for every `a ∈ P`. -/
theorem gen_proj_ineq {n : ℕ} (P : Set (EuclideanSpace ℝ (Fin n))) (hP : Convex ℝ P)
    (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.PosSemidef)
    (y z : EuclideanSpace ℝ (Fin n)) (hz : IsGenProj P A y z) :
    ∀ a ∈ P, quadForm A (z - a) ≤ quadForm A (y - a) := by sorry

end LogRegretOCO.ONS

Source

Hazan, Agarwal, Kale, Logarithmic regret algorithms for online convex optimization, Mach Learn 69 (2007), p. 188, Lemma 8

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting. Let $n\in\mathbb{N}$ and let $P\subseteq\mathbb{R}^n$ be convex. Let $A$ be a real $n\times n$ matrix that is positive semidefinite, meaning both:

$A$ is symmetric;
$v^\top A v\ge 0$ for all $v$ .

Let $y,z\in\mathbb{R}^n$ .

Hypothesis. $z$ is a generalized projection of $y$ onto $P$ with respect to $A$ . That is:

$z\in P$ ;
$(y-z)^\top A(y-z)\le (y-w)^\top A(y-w)$ for every $w\in P$ .

Conclusion. For every $a\in P$ ,

(z-a)^\top A\,(z-a)\;\le\;(y-a)^\top A\,(y-a).

Assumptions not made: closedness or boundedness of $P$ is not assumed. The existence of the minimizer $z$ is itself a hypothesis.

Degenerate cases:

$P$ empty: the projection hypothesis cannot hold, so the statement is vacuous.
$y\in P$ : then $z$ attains $(y-z)^\top A (y-z)\le 0$ . With $a=y$ the conclusion says $(z-y)^\top A(z-y)\le 0$ .
$A=0$ :
- every point of $P$ is a generalized projection;
- the conclusion is $0\le 0$ .
$n=0$ : both sides are $0$ .

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph