Rigidez da compressão pela igualdade da soma de quadrados

Proved

HilbertCompression.quadratic_identity_reduces

by BrunoDCDO · Sep 23, 2026 · Mathlib c5ea003 (Lean v4.30.0)

functional-analysishilbert-spacesoperator-theory

Let $H$ be a complete complex Hilbert space, let $X,Y\in\mathcal B(H)$ be bounded self-adjoint operators, and let $P\in\mathcal B(H)$ be an orthogonal projection. If

P(X^2+Y^2)P=(PXP)^2+(PYP)^2,

then

PX=XP,\qquad PY=YP.

The criterion shows that the projected subspace simultaneously reduces two operators from a single quadratic identity. It holds in arbitrary dimension, including the zero space, and requires neither positivity nor commutativity of $X,Y$ .

This is a derived algebraic lemma for CUHK-Shenzhen Problem 2. The source's question for every continuous strictly convex function remains separate.

Preamble

import Mathlib.Analysis.InnerProductSpace.Adjoint
set_option autoImplicit false

Formal statement

theorem HilbertCompression.quadratic_identity_reduces
    (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (X Y P : H →L[ℂ] H)
    (hX : star X = X) (hY : star Y = Y)
    (hP : star P = P) (hPP : P * P = P)
    (hquadrado : P * (X * X + Y * Y) * P =
      (P * X * P) * (P * X * P) + (P * Y * P) * (P * Y * P)) :
    P * X = X * P ∧ P * Y = Y * P := by sorry

Source

Derived algebraic compression criterion supporting CUHK-Shenzhen AI Math Problems, Problem 2, https://rybindmitry.github.io/problems/2.html, displayed compression equality and reduction question. The source poses the general strictly convex problem; this supporting quadratic criterion is not stated separately there.

View graph