AcceptedLemma · Statement with omitted proof

Residual inequality for Hermitian powers

Powering a Gram matrix controls the original projection residual.

Martinsson & Tropp ↗
Source label: lem:powering

Download Lean file ↓

Formal statement. The assumptions and conclusion are explicit; the theorem proof is omitted (sorry).

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

Powering a Gram matrix controls the original projection residual.

\|(I-P)B\|^{2q}\le\|(I-P)(BB^*)^q\|

Assumptions & context

B is real or complex, P is an orthogonal projector and q ≥ 1 is real.

Source

Martinsson & Tropp. Randomized numerical linear algebra: Foundations and algorithms.

Source label: lem:powering

02 / LEAN REPRESENTATION

Formal statement

Statement with omitted proof. Expand the complete file below to read imports, local definitions and surrounding context.

theorem powering {𝕜 : Type*} [RCLike 𝕜] {m n : ℕ}
    (B : Matrix (Fin m) (Fin n) 𝕜) (P : Matrix (Fin m) (Fin m) 𝕜)
    (hP : IsOrthogonalProjector P) (q : ℝ) (hq : 1 ≤ q) :
    ‖(1 - P) * B‖ ^ (2 * q) ≤
      ‖(1 - P) * hermitianRpow (Matrix.isHermitian_mul_conjTranspose_self B) q‖ := by
  sorry

Complete Lean file and local definitions

import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity

open MeasureTheory
open scoped Matrix
open scoped Matrix.Norms.L2Operator
open scoped BigOperators
open scoped ENNReal

namespace RNLAPhaseB.MT2020.Powering

/-- A square matrix `P` is an orthogonal projector: idempotent and self-adjoint. -/
def IsOrthogonalProjector {𝕜 : Type*} [RCLike 𝕜] {m : Type*} [Fintype m] [DecidableEq m]
    (P : Matrix m m 𝕜) : Prop :=
  P * P = P ∧ Pᴴ = P

/-- The real power `A ^ q` of a Hermitian matrix `A`, defined by the spectral calculus:
`A = U diag(λ) U*` gives `A ^ q = U diag(λ ^ q) U*`. The source applies this to the
positive-semidefinite matrix `B B^*` with real exponent `q ≥ 1`. -/
noncomputable def hermitianRpow {𝕜 : Type*} [RCLike 𝕜] {m : Type*} [Fintype m] [DecidableEq m]
    {A : Matrix m m 𝕜} (hA : A.IsHermitian) (q : ℝ) : Matrix m m 𝕜 :=
  (hA.eigenvectorUnitary : Matrix m m 𝕜) *
    Matrix.diagonal (fun i => ((hA.eigenvalues i ^ q : ℝ) : 𝕜)) *
    star (hA.eigenvectorUnitary : Matrix m m 𝕜)

/-- mt2020 Lemma (lem:powering). For a fixed `B ∈ 𝔽^{m×n}` (𝔽 = ℝ or ℂ), an orthogonal
projector `P ∈ 𝔽^{m×m}`, and any real `q ≥ 1`,
`‖(I - P) B‖^{2q} ≤ ‖(I - P) (B B^*)^q‖`, with `‖·‖` the spectral norm. -/
theorem powering {𝕜 : Type*} [RCLike 𝕜] {m n : ℕ}
    (B : Matrix (Fin m) (Fin n) 𝕜) (P : Matrix (Fin m) (Fin m) 𝕜)
    (hP : IsOrthogonalProjector P) (q : ℝ) (hq : 1 ≤ q) :
    ‖(1 - P) * B‖ ^ (2 * q) ≤
      ‖(1 - P) * hermitianRpow (Matrix.isHermitian_mul_conjTranspose_self B) q‖ := by
  sorry

end RNLAPhaseB.MT2020.Powering

How to read the formalization

Hermitian functional calculus realizes the real matrix power; the result is not limited to integer iteration counts.

← Back to all statements