AcceptedLemma · Statement with omitted proof

Pythagoras identity for matrices

Orthogonal matrix components have additive squared Frobenius norms.

Drineas & Mahoney ↗
Source label: l_pyth

Download Lean file ↓

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

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

Orthogonal matrix components have additive squared Frobenius norms.

\|A+B\|_F^2=\|A\|_F^2+\|B\|_F^2

Assumptions & context

A and B have the same real matrix dimensions and satisfy AᵀB = 0.

Source

Drineas & Mahoney. Lectures on randomized numerical linear algebra.

Source label: l_pyth

02 / LEAN REPRESENTATION

Formal statement

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

theorem matrix_pythagoras {m n : ℕ} (A B : Matrix (Fin m) (Fin n) ℝ)
    (h : Aᵀ * B = 0) :
    frobeniusNorm (A + B) ^ 2 = frobeniusNorm A ^ 2 + frobeniusNorm B ^ 2 := 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.DM2017.MatrixPythagoras

/-- The Frobenius norm of a real `m × n` matrix: `‖A‖_F = sqrt (∑_i ∑_j A_ij^2)`.
Defined explicitly so that it does not clash with the scoped L2-operator norm
instance opened in the header. -/
noncomputable def frobeniusNorm {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) : ℝ :=
  Real.sqrt (∑ i, ∑ j, A i j ^ 2)

/-- dm2017 Lemma `l_pyth` (matrix Pythagoras): for `A, B ∈ ℝ^{m×n}`, if `Aᵀ B = 0`
then `‖A + B‖_F^2 = ‖A‖_F^2 + ‖B‖_F^2`. -/
theorem matrix_pythagoras {m n : ℕ} (A B : Matrix (Fin m) (Fin n) ℝ)
    (h : Aᵀ * B = 0) :
    frobeniusNorm (A + B) ^ 2 = frobeniusNorm A ^ 2 + frobeniusNorm B ^ 2 := by
  sorry

end RNLAPhaseB.DM2017.MatrixPythagoras

How to read the formalization

The Frobenius norm is defined explicitly; the hypothesis is matrix orthogonality.

← Back to all statements