Proof of Lemma A.1, p. 25 — Tr V = Tr V^∥ + Tr V^⊥

Proved

PhaseCut.Stable.trace_split

by mikedeng1 · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-algebrap2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1phase-retrievaltrace

Let $A \in \mathbb{C}^{n\times p}$ and $P = AA^\dagger$ the orthogonal projector onto $\mathcal{R}(A)$ . For every $V \in \mathbb{C}^{n\times n}$ , with $V^{/\!/} = PVP$ and $V^\perp = (I-P)V(I-P)$ ,

\operatorname{Tr} V = \operatorname{Tr} V^{/\!/} + \operatorname{Tr} V^\perp ,

equivalently $\operatorname{Tr} V^{/\!/} = \operatorname{Tr} V - \operatorname{Tr} V^\perp$ .

In the proof of Lemma A.1 this identity, applied to the minimizer $V_{PC}$ of (13), bounds $\operatorname{Tr} V_{PC}^{/\!/}$ by $\operatorname{Tr} V_{PC} = \||Ax_0| + b_{n,PC}\|_2^2$ .

Formalization Note. The paper states the identity for $V_{PC}$ ; it holds for every square matrix and is stated so.

Preamble

import Mathlib
import Definitions.Def_PhaseCut_Stable_Defs

Formal statement

namespace PhaseCut.Stable

open Matrix
open scoped ComplexOrder


/-- **Trace split**, proof of Lemma A.1 (p. 25): `Tr V = Tr V^∥ + Tr V^⊥`, i.e.
`Tr V^∥ = Tr V − Tr V^⊥`. -/
theorem trace_split {n p : ℕ} (A : Matrix (Fin n) (Fin p) ℂ) (V : Matrix (Fin n) (Fin n) ℂ) :
    V.trace = (Vpar A V).trace + (Vperp A V).trace := by sorry
end PhaseCut.Stable

Source

Waldspurger, d'Aspremont & Mallat, arXiv:1206.0102v3, proof of Lemma A.1, p. 25, first display

Human review

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

View graph