Prove2Me

(2.9) — polarization identity for the L2(Π)L_2(\Pi) inner product

Proved
KLTNuclear.Oracle.eq_2_9

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

l2-geometrymatrix-estimationp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1

For a sample with square-integrable design entries and any m1×m2m_1\times m_2 matrices BB, AA, A0A_0,

2⟨B−A0,B−A⟩L2(Π)=∥B−A0∥L2(Π)2+∥B−A∥L2(Π)2−∥A−A0∥L2(Π)2.2\langle B-A_0,B-A\rangle_{L_2(\Pi)}=\|B-A_0\|^2_{L_2(\Pi)}+\|B-A\|^2_{L_2(\Pi)}-\|A-A_0\|^2_{L_2(\Pi)}.

In the proof of Theorem 1 it is applied with B=A^λB=\hat A^\lambda to turn the cross term of (2.8) into the three squared distances of (2.11).

Formalization Note The paper states it with B=A^λB=\hat A^\lambda; the identity holds for every BB and is stated so. Square integrability of the design entries is what makes ⟨⋅,⋅⟩L2(Π)\langle\cdot,\cdot\rangle_{L_2(\Pi)} bilinear.

Preamble
import Mathlib
import Definitions.Def_KLTNuclear_Oracle_Model

open MeasureTheory MatrixCompletion
Formal statement
namespace KLTNuclear.Oracle

/-- (2.9) (p. 8): polarization identity for the L₂(Π) inner product, stated for arbitrary
matrices B (in the paper B = Â^λ), A and A₀. -/
theorem eq_2_9 {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    {n m₁ m₂ : ℕ} (hn : 0 < n)
    (X : Fin n → Ω → RealMatrix m₁ m₂) (Y : Fin n → Ω → ℝ)
    (hreg : SampleRegularity P X Y)
    (B A A₀ : RealMatrix m₁ m₂) :
    2 * l2Inner P X (B - A₀) (B - A) =
      l2NormSq P X (B - A₀) + l2NormSq P X (B - A) - l2NormSq P X (A - A₀) := by sorry

end KLTNuclear.Oracle
Source
Koltchinskii, Lounici, Tsybakov, Nuclear-Norm Penalization and Optimal Rates for Noisy Low-Rank Matrix Completion, arXiv:1011.6256v4, p. 8, (2.9)
Human review

  • Endorsed by Shuze Chen · Oct 7, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 7, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph