class IsVectorNorm {n : ℕ} (f : (Fin n → ℝ) → ℝ) : Prop

Source notion for Chapter01 Definition 1.2.1: a map f : (Fin n → ℝ) → ℝ is a vector norm on ℝ^n when it is nonnegative, vanishes exactly at 0, is absolutely homogeneous, and satisfies the triangle inequality.

• nonneg (x : Fin n → ℝ) : 0 ≤ f x
• eq_zero_iff (x : Fin n → ℝ) : f x = 0 ↔ x = 0
• smul_eq (a : ℝ) (x : Fin n → ℝ) : f (a • x) = |a| * f x
• add_le (x y : Fin n → ℝ) : f (x + y) ≤ f x + f y

theorem isVectorNorm_iff {n : ℕ} (f : (Fin n → ℝ) → ℝ) : IsVectorNorm f ↔ (∀ (x : Fin n → ℝ), 0 ≤ f x) ∧ (∀ (x : Fin n → ℝ), f x = 0 ↔ x = 0) ∧ (∀ (a : ℝ) (x : Fin n → ℝ), f (a • x) = |a| * f x) ∧ ∀ (x y : Fin n → ℝ), f (x + y) ≤ f x + f y

Unfolding formula for IsVectorNorm.

theorem IsVectorNorm.map_zero {n : ℕ} {f : (Fin n → ℝ) → ℝ} (hf : IsVectorNorm f) : f 0 = 0

Any vector norm vanishes at the zero vector.

theorem IsVectorNorm.map_neg {n : ℕ} {f : (Fin n → ℝ) → ℝ} (hf : IsVectorNorm f) (x : Fin n → ℝ) : f (-x) = f x

Any vector norm is invariant under negation.

noncomputable def IsVectorNorm.toSeminorm {n : ℕ} {f : (Fin n → ℝ) → ℝ} (hf : IsVectorNorm f) : Seminorm ℝ (Fin n → ℝ)

A vector norm on ℝ^n defines a real seminorm.

@[simp]

theorem IsVectorNorm.toSeminorm_apply {n : ℕ} {f : (Fin n → ℝ) → ℝ} (hf : IsVectorNorm f) (x : Fin n → ℝ) : hf.toSeminorm x = f x

theorem IsVectorNorm.toSeminorm_eq_zero_iff {n : ℕ} {f : (Fin n → ℝ) → ℝ} (hf : IsVectorNorm f) (x : Fin n → ℝ) : hf.toSeminorm x = 0 ↔ x = 0

The induced seminorm vanishes exactly at the zero vector.

noncomputable def IsVectorNorm.toAddGroupNorm {n : ℕ} {f : (Fin n → ℝ) → ℝ} (hf : IsVectorNorm f) : AddGroupNorm (Fin n → ℝ)

A vector norm on ℝ^n defines an additive group norm.

@[simp]

theorem IsVectorNorm.toAddGroupNorm_apply {n : ℕ} {f : (Fin n → ℝ) → ℝ} (hf : IsVectorNorm f) (x : Fin n → ℝ) : hf.toAddGroupNorm x = f x

noncomputable def lpNorm {n : ℕ} (p : ENNReal) [Fact (1 ≤ p)] : (Fin n → ℝ) → ℝ

The ℓ^p norm on ℝ^n for 1 ≤ p, implemented via the canonical PiLp norm on functions Fin n → ℝ.

theorem lpNorm_eq_sum {n : ℕ} (p : ENNReal) [Fact (1 ≤ p)] (hp : 0 < p.toReal) (x : Fin n → ℝ) : lpNorm p x = (∑ i : Fin n, |x i| ^ p.toReal) ^ (1 / p.toReal)

For 0 < p.toReal, the ℓ^p norm is given by the usual finite-sum formula.

instance lpNorm_isVectorNorm {n : ℕ} (p : ENNReal) [Fact (1 ≤ p)] : IsVectorNorm fun (x : Fin n → ℝ) => lpNorm p x

Chapter01 Definition 1.2.1: for 1 ≤ p, the ℓ^p norm is a vector norm on ℝ^n.

noncomputable def linftyNorm {n : ℕ} : (Fin n → ℝ) → ℝ

The ℓ^∞ norm on ℝ^n.

noncomputable def l1Norm {n : ℕ} : (Fin n → ℝ) → ℝ

The ℓ^1 norm on ℝ^n.

noncomputable def l2Norm {n : ℕ} : (Fin n → ℝ) → ℝ

The ℓ^2 norm on ℝ^n.

def «term‖_‖∞» : Lean.ParserDescr

def «term‖_‖₁» : Lean.ParserDescr

def «term‖_‖₂» : Lean.ParserDescr

theorem linftyNorm_eq_finset_sup'_abs {n : ℕ} [Nonempty (Fin n)] (x : Fin n → ℝ) : ‖x‖∞ = Finset.univ.sup' ⋯ fun (i : Fin n) => |x i|

For n ≥ 1, the ℓ^∞ norm is the maximum of the coordinatewise absolute values.

theorem linftyNorm_eq_iSup_abs {n : ℕ} (x : Fin n → ℝ) : ‖x‖∞ = ⨆ (i : Fin n), |x i|

The ℓ^∞ norm is the supremum of the coordinatewise absolute values.

instance linftyNorm_isVectorNorm {n : ℕ} : IsVectorNorm fun (x : Fin n → ℝ) => ‖x‖∞

The ℓ^∞ norm is a vector norm on ℝ^n.

theorem l1Norm_eq_sum_abs {n : ℕ} (x : Fin n → ℝ) : ‖x‖₁ = ∑ i : Fin n, |x i|

The ℓ^1 norm is the sum of the coordinatewise absolute values.

instance l1Norm_isVectorNorm {n : ℕ} : IsVectorNorm fun (x : Fin n → ℝ) => ‖x‖₁

The ℓ^1 norm is a vector norm on ℝ^n.

theorem l2Norm_eq_sqrt_sum_sq {n : ℕ} (x : Fin n → ℝ) : ‖x‖₂ = √(∑ i : Fin n, |x i| ^ 2)

The ℓ^2 norm is the square root of the sum of the squared absolute values.

instance l2Norm_isVectorNorm {n : ℕ} : IsVectorNorm fun (x : Fin n → ℝ) => ‖x‖₂

The ℓ^2 norm is a vector norm on ℝ^n.

noncomputable def ellipsoidNorm {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : (Fin n → ℝ) → ℝ

The ellipsoid norm attached to a real square matrix A. For positive-definite A, the corresponding theorem below upgrades it to a vector norm.

theorem ellipsoidNorm_eq_sqrt_dotProduct_mulVec {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (x : Fin n → ℝ) : ellipsoidNorm A x = √(x ⬝ᵥ A.mulVec x)

The ellipsoid norm is given by sqrt (xᵀ A x).

theorem ellipsoidNorm_isVectorNorm {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.PosDef) : IsVectorNorm (ellipsoidNorm A)

With hA : A.PosDef, the ellipsoid norm is a vector norm on ℝ^n.