AcceptedDefinition with auxiliary statements (proofs omitted)

Frobenius norm and the trace identity

The Frobenius norm is the square root of the sum of squared matrix entries.

Drineas & Mahoney ↗
Source label: def:frobenius-norm

Definition. The displayed code defines the mathematical object or predicate. Auxiliary statements shown alongside the definition have omitted proofs (sorry).

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

The Frobenius norm is the square root of the sum of squared matrix entries.

\|A\|_F=\left(\sum_{j=1}^n\sum_{i=1}^m A_{ij}^2\right)^{1/2}=\sqrt{\operatorname{tr}(A^\top A)}

Assumptions & context

A is a real m × n matrix; the trace identity uses the n × n Gram matrix AᵀA.

Source

Drineas & Mahoney. Lectures on randomized numerical linear algebra.

Source label: def:frobenius-norm

02 / LEAN REPRESENTATION

Definition

Definition with auxiliary statements (proofs omitted). Expand the complete file below to read imports, local definitions and surrounding context.

noncomputable def frobeniusNorm {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) : ℝ :=
  Real.sqrt (∑ j : Fin n, ∑ i : Fin m, A i j ^ 2)

theorem frobeniusNorm_eq_sqrt_trace {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) :
    frobeniusNorm A = Real.sqrt (Matrix.trace (Aᵀ * A)) := 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.FrobeniusNormDef

/-- dm2017 `def:frobenius-norm`: for `A ∈ ℝ^{m×n}`, the Frobenius norm is defined as
`‖A‖_F = sqrt (∑_{j=1}^n ∑_{i=1}^m A_{ij}^2)`.
The sum runs over columns `j` on the outside and rows `i` on the inside, as the source writes it. -/
noncomputable def frobeniusNorm {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) : ℝ :=
  Real.sqrt (∑ j : Fin n, ∑ i : Fin m, A i j ^ 2)

/-- dm2017 `def:frobenius-norm`, second displayed equality:
`‖A‖_F = sqrt (Tr (Aᵀ A))`.
Here `Tr` is the matrix trace, the sum of the main-diagonal entries of a square matrix.
In Lean this is `Matrix.trace`. -/
theorem frobeniusNorm_eq_sqrt_trace {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) :
    frobeniusNorm A = Real.sqrt (Matrix.trace (Aᵀ * A)) := by
  sorry

end RNLAPhaseB.DM2017.FrobeniusNormDef

How to read the formalization

The file defines the norm explicitly and states a separate trace identity with an omitted proof.

← Back to all statements