FARMSAcceptedDefinition
Axioms of a matrix norm
A matrix norm is characterized by definiteness, the triangle inequality and absolute homogeneity.
Drineas & Mahoney ↗
Source label: def:norm
Definition. The displayed code defines the mathematical object or predicate.
01 / MATHEMATICAL STATEMENT
Meaning & conditions
Mathematical summary
A matrix norm is characterized by definiteness, the triangle inequality and absolute homogeneity.
Assumptions & context
- The function maps real m × n matrices to real numbers and uses ordinary matrix addition and scalar multiplication.
Source
Drineas & Mahoney. Lectures on randomized numerical linear algebra.
Source label: def:norm
02 / LEAN REPRESENTATION
Definition
Definition. Expand the complete file below to read imports, local definitions and surrounding context.
def IsNorm {m n : ℕ} (nrm : Matrix (Fin m) (Fin n) ℝ → ℝ) : Prop :=
-- 1. Non-negativity: `‖A‖ ≥ 0`.
(∀ A : Matrix (Fin m) (Fin n) ℝ, 0 ≤ nrm A) ∧
-- 1. (cont.) `‖A‖ = 0` if and only if `A = 0`.
(∀ A : Matrix (Fin m) (Fin n) ℝ, nrm A = 0 ↔ A = 0) ∧
-- 2. Triangle inequality: `‖A + B‖ ≤ ‖A‖ + ‖B‖`.
(∀ A B : Matrix (Fin m) (Fin n) ℝ, nrm (A + B) ≤ nrm A + nrm B) ∧
-- 3. Scalar multiplication: `‖α A‖ = |α| ‖A‖` for all `α ∈ ℝ`.
(∀ (α : ℝ) (A : Matrix (Fin m) (Fin n) ℝ), nrm (α • A) = |α| * nrm A)
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.DefNorm
/-- dm2017::def:norm. A function `‖·‖ : ℝ^{m×n} → ℝ` (here `nrm`) is called a **norm**
if it satisfies:
1. Non-negativity: `‖A‖ ≥ 0`, and `‖A‖ = 0` if and only if `A = 0`;
2. Triangle inequality: `‖A + B‖ ≤ ‖A‖ + ‖B‖`;
3. Scalar multiplication: `‖α A‖ = |α| ‖A‖` for all `α ∈ ℝ`.
Matrix addition and scalar multiplication are the standard entrywise operations
(the section's stated convention of basic matrix operations). The predicate is the
explicit conjunction of these axioms; no scoped Mathlib matrix norm is used. -/
def IsNorm {m n : ℕ} (nrm : Matrix (Fin m) (Fin n) ℝ → ℝ) : Prop :=
-- 1. Non-negativity: `‖A‖ ≥ 0`.
(∀ A : Matrix (Fin m) (Fin n) ℝ, 0 ≤ nrm A) ∧
-- 1. (cont.) `‖A‖ = 0` if and only if `A = 0`.
(∀ A : Matrix (Fin m) (Fin n) ℝ, nrm A = 0 ↔ A = 0) ∧
-- 2. Triangle inequality: `‖A + B‖ ≤ ‖A‖ + ‖B‖`.
(∀ A B : Matrix (Fin m) (Fin n) ℝ, nrm (A + B) ≤ nrm A + nrm B) ∧
-- 3. Scalar multiplication: `‖α A‖ = |α| ‖A‖` for all `α ∈ ℝ`.
(∀ (α : ℝ) (A : Matrix (Fin m) (Fin n) ℝ), nrm (α • A) = |α| * nrm A)
end RNLAPhaseB.DM2017.DefNorm
How to read the formalization
- IsNorm is a conjunction of axioms for an arbitrary function; it does not select a particular matrix norm.