@[reducible, inline]

abbrev RowVector (n : ℕ) : Type

Definition 6.1 (Row vectors): for a natural number n, an n-dimensional row vector over ℝ is represented as a 1 × n matrix; vector addition, scalar multiplication, the zero vector, and additive inverses are the inherited pointwise operations.

Equations

• RowVector n = Matrix (Fin 1) (Fin n) ℝ

theorem helperForLemma_6_1_additiveGroupIdentities (n : ℕ) (x y z : Fin n → ℝ) : x + y = y + x ∧ x + y + z = x + (y + z) ∧ x + 0 = x ∧ 0 + x = x ∧ x + -x = 0 ∧ -x + x = 0

Helper for Lemma 6.1: additive-group identities for vectors Fin n → ℝ.

theorem helperForLemma_6_1_scalarAssociativityUnit (n : ℕ) (x : Fin n → ℝ) (c d : ℝ) : (c * d) • x = c • d • x ∧ 1 • x = x

Helper for Lemma 6.1: scalar associativity and scalar unit on Fin n → ℝ.

theorem helperForLemma_6_1_scalarDistributivity (n : ℕ) (x y : Fin n → ℝ) (c d : ℝ) : c • (x + y) = c • x + c • y ∧ (c + d) • x = c • x + d • x

Helper for Lemma 6.1: scalar distributivity identities on Fin n → ℝ.

theorem rowVector_real_vector_space_identities (n : ℕ) (x y z : Fin n → ℝ) (c d : ℝ) : x + y = y + x ∧ x + y + z = x + (y + z) ∧ x + 0 = x ∧ 0 + x = x ∧ x + -x = 0 ∧ -x + x = 0 ∧ (c * d) • x = c • d • x ∧ c • (x + y) = c • x + c • y ∧ (c + d) • x = c • x + d • x ∧ 1 • x = x

Lemma 6.1: ℝ^n is a vector space over ℝ; for all x y z : Fin n → ℝ and c d : ℝ, vector addition is commutative and associative, 0 is an additive identity, -x is an additive inverse, scalar multiplication is associative, distributes over vector and scalar addition, and 1 acts as the identity scalar.

@[reducible, inline]

abbrev ColumnVector (n : ℕ) : Type

An n-dimensional column vector over ℝ, represented as an n × 1 matrix.

Equations

• ColumnVector n = Matrix (Fin n) (Fin 1) ℝ

def rowVectorTranspose {n : ℕ} (x : RowVector n) : ColumnVector n

Definition 6.2 (Transpose): for n : ℕ and a row vector x = (x₁, …, xₙ) : RowVector n, its transpose xᵀ is the n × 1 column vector with the same coordinates. Equivalently, an n-dimensional column vector is a vector of the form xᵀ for some row vector x.

Equations

• rowVectorTranspose x = Matrix.transpose x

theorem columnVector_exists_as_transpose (n : ℕ) (y : ColumnVector n) : ∃ (x : RowVector n), rowVectorTranspose x = y

Every n-dimensional column vector is the transpose of a row vector.

def standardBasisRowVector (n : ℕ) (j : Fin n) : RowVector n

Definition 6.3 (Standard basis vectors of ℝ^n): for j : Fin n, the standard basis row vector e_j has entries (e_j)_i = 1 if i = j and (e_j)_i = 0 otherwise.

Equations

• standardBasisRowVector n j x✝ i = if i = j then 1 else 0

theorem rowVector_eq_sum_standardBasisRowVector (n : ℕ) (x : RowVector n) : x = ∑ j : Fin n, x 0 j • standardBasisRowVector n j

Every row vector in ℝ^n is the sum of its coordinates times the standard basis row vectors.

theorem rowVectorTranspose_eq_sum_standardBasisTranspose (n : ℕ) (x : RowVector n) : rowVectorTranspose x = ∑ j : Fin n, x 0 j • rowVectorTranspose (standardBasisRowVector n j)

The transpose of a row vector is the corresponding linear combination of the transposed standard basis vectors.

def IsLinearTransformation {n m : ℕ} (T : (Fin n → ℝ) → Fin m → ℝ) : Prop

Definition 6.4 (Linear transformation): a function T : ℝ^n → ℝ^m is linear iff for all x y : ℝ^n and c : ℝ, (i) T (x + y) = T x + T y and (ii) T (c • x) = c • T x.

Equations

• IsLinearTransformation T = ((∀ (x y : Fin n → ℝ), T (x + y) = T x + T y) ∧ ∀ (c : ℝ) (x : Fin n → ℝ), T (c • x) = c • T x)

@[reducible, inline]

abbrev MatrixOver (S : Type u_1) (m n : ℕ+) : Type u_1

Definition 6.5 (Matrices): for positive natural numbers m, n, an m × n matrix over a set S is a family A = (a i j) of elements of S indexed by i : Fin m and j : Fin n. A 1 × n matrix is an n-dimensional row vector, and an n × 1 matrix is an n-dimensional column vector.

Equations

• MatrixOver S m n = Matrix (Fin ↑m) (Fin ↑n) S

@[reducible, inline]

abbrev matrixProduct {m n p : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (B : Matrix (Fin n) (Fin p) ℝ) : Matrix (Fin m) (Fin p) ℝ

Definition 6.6 (Matrix product): for m n p : ℕ, if A is an m × n matrix and B is an n × p matrix (over ℝ), then matrixProduct A B is the m × p matrix with entries (matrixProduct A B) i k = ∑ j : Fin n, A i j * B j k. In particular, when p = 1, this gives matrix-column-vector multiplication (A xᵀ) i = ∑ j : Fin n, A i j * xᵀ j 0.

Equations

• matrixProduct A B = A * B

def helperForLemma_6_2_linearMapFromIsLinearTransformation {n m : ℕ} (T : (Fin n → ℝ) → Fin m → ℝ) (hT : IsLinearTransformation T) : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ

Helper for Lemma 6.2: convert IsLinearTransformation to a mathlib LinearMap.

Equations

• helperForLemma_6_2_linearMapFromIsLinearTransformation T hT = { toFun := T, map_add' := ⋯, map_smul' := ⋯ }

theorem helperForLemma_6_2_matrixCandidateRepresentsT {n m : ℕ} (T : (Fin n → ℝ) → Fin m → ℝ) (hT : IsLinearTransformation T) (x : Fin n → ℝ) : T x = (LinearMap.toMatrix' (helperForLemma_6_2_linearMapFromIsLinearTransformation T hT)).mulVec x

Helper for Lemma 6.2: the matrix from LinearMap.toMatrix' represents T.

theorem helperForLemma_6_2_toLin_eq_of_representsT {n m : ℕ} (T : (Fin n → ℝ) → Fin m → ℝ) (hT : IsLinearTransformation T) (B : Matrix (Fin m) (Fin n) ℝ) (hB : ∀ (x : Fin n → ℝ), T x = B.mulVec x) : Matrix.toLin' B = helperForLemma_6_2_linearMapFromIsLinearTransformation T hT

Helper for Lemma 6.2: a representing matrix yields the corresponding Matrix.toLin' equality.

theorem helperForLemma_6_2_representation_unique {n m : ℕ} (T : (Fin n → ℝ) → Fin m → ℝ) (hT : IsLinearTransformation T) (B : Matrix (Fin m) (Fin n) ℝ) (hB : ∀ (x : Fin n → ℝ), T x = B.mulVec x) : B = LinearMap.toMatrix' (helperForLemma_6_2_linearMapFromIsLinearTransformation T hT)

Helper for Lemma 6.2: matrix representation of T is unique.

theorem linearTransformation_existsUnique_matrixRepresentation {n m : ℕ} (T : (Fin n → ℝ) → Fin m → ℝ) (hT : IsLinearTransformation T) : ∃! A : Matrix (Fin m) (Fin n) ℝ, ∀ (x : Fin n → ℝ), T x = A.mulVec x

Lemma 6.2: if T : ℝ^n → ℝ^m is a linear transformation, then there exists a unique matrix A : ℝ^{m × n} such that T x = A x for every x : ℝ^n.

theorem leftMultiplication_comp_eq_leftMultiplication_mul {𝔽 : Type u_1} [Field 𝔽] {m n p : ℕ} (A : Matrix (Fin m) (Fin n) 𝔽) (B : Matrix (Fin n) (Fin p) 𝔽) : A.mulVecLin ∘ₗ B.mulVecLin = (A * B).mulVecLin

Lemma 6.3: for matrices A and B over the same field, if L_M denotes left-multiplication by M on compatible column vectors, then L_A ∘ L_B = L_{AB} as linear maps 𝔽^p → 𝔽^m.

theorem helperForProposition_6_1_fixedScalar_add (n : ℕ) (a : ℝ) (x y : Fin n → ℝ) : a • (x + y) = a • x + a • y

Helper for Proposition 6.1: scaling by a fixed scalar preserves addition on Fin n → ℝ.

theorem helperForProposition_6_1_fixedScalar_smul (n : ℕ) (a c : ℝ) (x : Fin n → ℝ) : a • c • x = c • a • x

Helper for Proposition 6.1: scaling by a fixed scalar commutes with an external scalar multiplication on Fin n → ℝ.

theorem helperForProposition_6_1_fixedScalar_isLinear (n : ℕ) (a : ℝ) : IsLinearTransformation fun (x : Fin n → ℝ) => a • x

Helper for Proposition 6.1: for any dimension n and scalar a, the map x ↦ a • x is linear.

theorem t1_isLinearTransformation : IsLinearTransformation fun (x : Fin 3 → ℝ) => 5 • x

Proposition 6.1: the map T₁ : ℝ^3 → ℝ^3 defined by T₁ x = 5x is a linear transformation.

theorem helperForProposition_6_2_rotate_add (x y : Fin 2 → ℝ) : (fun (z : Fin 2 → ℝ) => ![-z 1, z 0]) (x + y) = (fun (z : Fin 2 → ℝ) => ![-z 1, z 0]) x + (fun (z : Fin 2 → ℝ) => ![-z 1, z 0]) y

Helper for Proposition 6.2: the rotation map x ↦ (-x₂, x₁) preserves vector addition on ℝ².

theorem helperForProposition_6_2_rotate_smul (c : ℝ) (x : Fin 2 → ℝ) : (fun (z : Fin 2 → ℝ) => ![-z 1, z 0]) (c • x) = c • (fun (z : Fin 2 → ℝ) => ![-z 1, z 0]) x

Helper for Proposition 6.2: the rotation map x ↦ (-x₂, x₁) commutes with scalar multiplication on ℝ².

theorem t2_rotatePiOverTwo_isLinearTransformation : IsLinearTransformation fun (x : Fin 2 → ℝ) => ![-x 1, x 0]

Proposition 6.2: let T₂ : ℝ² → ℝ² be the map that rotates each vector about the origin by angle π/2 counterclockwise, i.e. T₂(x₁, x₂) = (-x₂, x₁). Then T₂ is a linear transformation.

theorem helperForProposition_6_3_dropThird_add (x y : Fin 3 → ℝ) : (fun (z : Fin 3 → ℝ) => ![z 0, z 1]) (x + y) = (fun (z : Fin 3 → ℝ) => ![z 0, z 1]) x + (fun (z : Fin 3 → ℝ) => ![z 0, z 1]) y

Helper for Proposition 6.3: dropping the third coordinate preserves vector addition on ℝ³.

theorem helperForProposition_6_3_dropThird_smul (c : ℝ) (x : Fin 3 → ℝ) : (fun (z : Fin 3 → ℝ) => ![z 0, z 1]) (c • x) = c • (fun (z : Fin 3 → ℝ) => ![z 0, z 1]) x

Helper for Proposition 6.3: dropping the third coordinate commutes with scalar multiplication on ℝ³.

theorem t3_dropThirdCoordinate_isLinearTransformation : IsLinearTransformation fun (x : Fin 3 → ℝ) => ![x 0, x 1]

Proposition 6.3: define T₃ : ℝ³ → ℝ² by T₃(x, y, z) = (x, y). Then T₃ is a linear transformation, i.e. for all u v : ℝ³ and c : ℝ, T₃ (u + v) = T₃ u + T₃ v and T₃ (c • u) = c • T₃ u.

theorem helperForProposition_6_4_embed_add (x y : Fin 2 → ℝ) : (fun (z : Fin 2 → ℝ) => ![z 0, z 1, 0]) (x + y) = (fun (z : Fin 2 → ℝ) => ![z 0, z 1, 0]) x + (fun (z : Fin 2 → ℝ) => ![z 0, z 1, 0]) y

Helper for Proposition 6.4: the embedding map x ↦ (x₁, x₂, 0) preserves vector addition on ℝ².

theorem helperForProposition_6_4_embed_smul (c : ℝ) (x : Fin 2 → ℝ) : (fun (z : Fin 2 → ℝ) => ![z 0, z 1, 0]) (c • x) = c • (fun (z : Fin 2 → ℝ) => ![z 0, z 1, 0]) x

Helper for Proposition 6.4: the embedding map x ↦ (x₁, x₂, 0) commutes with scalar multiplication on ℝ².

theorem helperForProposition_6_4_embed_isLinear : IsLinearTransformation fun (x : Fin 2 → ℝ) => ![x 0, x 1, 0]

Helper for Proposition 6.4: the embedding map x ↦ (x₁, x₂, 0) is linear.

theorem t4_embedInThreeSpace_isLinearTransformation : IsLinearTransformation fun (x : Fin 2 → ℝ) => ![x 0, x 1, 0]

Proposition 6.4: define T₄ : ℝ² → ℝ³ by T₄(x, y) = (x, y, 0). Then T₄ is a linear transformation, i.e. for all u v : ℝ² and c : ℝ, T₄ (u + v) = T₄ u + T₄ v and T₄ (c • u) = c • T₄ u.

theorem helperForProposition_6_5_identity_add (n : ℕ) (x y : Fin n → ℝ) : (fun (z : Fin n → ℝ) => z) (x + y) = (fun (z : Fin n → ℝ) => z) x + (fun (z : Fin n → ℝ) => z) y

Helper for Proposition 6.5: the identity map on Fin n → ℝ preserves addition.

theorem helperForProposition_6_5_identity_smul (n : ℕ) (c : ℝ) (x : Fin n → ℝ) : (fun (z : Fin n → ℝ) => z) (c • x) = c • (fun (z : Fin n → ℝ) => z) x

Helper for Proposition 6.5: the identity map on Fin n → ℝ commutes with scalar multiplication.

theorem helperForProposition_6_5_identity_isLinear (n : ℕ) : IsLinearTransformation fun (x : Fin n → ℝ) => x

Helper for Proposition 6.5: for each n, the identity map on Fin n → ℝ is linear.

theorem identityMap_isLinearTransformation (n : ℕ) : IsLinearTransformation fun (x : Fin n → ℝ) => x

Proposition 6.5: for each n : ℕ, the map I_n : ℝ^n → ℝ^n defined by I_n x = x for all x is a linear transformation.

theorem composition_isLinearTransformation {p n m : ℕ} (T : (Fin n → ℝ) → Fin m → ℝ) (S : (Fin p → ℝ) → Fin n → ℝ) (hT : IsLinearTransformation T) (hS : IsLinearTransformation S) : IsLinearTransformation fun (x : Fin p → ℝ) => T (S x)

Proposition 6.6: if T : ℝ^n → ℝ^m and S : ℝ^p → ℝ^n are linear transformations, then their composition TS, defined by (TS) x = T (S x) for all x : ℝ^p, is also a linear transformation.

theorem helperForProposition_6_7_bound_by_opNorm {n m : ℕ} (T : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (x : EuclideanSpace ℝ (Fin n)) : ‖T x‖ ≤ ‖LinearMap.toContinuousLinearMap T‖ * ‖x‖

Helper for Proposition 6.7: the operator norm of T bounds ‖T x‖ by ‖LinearMap.toContinuousLinearMap T‖ * ‖x‖.

theorem helperForProposition_6_7_bound_by_opNormPlusOne {n m : ℕ} (T : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (x : EuclideanSpace ℝ (Fin n)) : ‖T x‖ ≤ (‖LinearMap.toContinuousLinearMap T‖ + 1) * ‖x‖

Helper for Proposition 6.7: replacing the operator norm by ‖LinearMap.toContinuousLinearMap T‖ + 1 preserves the bound.

theorem helperForProposition_6_7_positive_constant {n m : ℕ} (T : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) : 0 < ‖LinearMap.toContinuousLinearMap T‖ + 1

Helper for Proposition 6.7: the constant ‖LinearMap.toContinuousLinearMap T‖ + 1 is strictly positive.

theorem helperForProposition_6_7_continuous_apply {n m : ℕ} (T : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) : Continuous fun (x : EuclideanSpace ℝ (Fin n)) => T x

Helper for Proposition 6.7: every linear map between these finite-dimensional Euclidean spaces is continuous.

theorem linearTransformation_exists_pos_bound_and_continuous {n m : ℕ} (T : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) : ∃ M > 0, (∀ (x : EuclideanSpace ℝ (Fin n)), ‖T x‖ ≤ M * ‖x‖) ∧ Continuous fun (x : EuclideanSpace ℝ (Fin n)) => T x

Proposition 6.7: if T : ℝ^n → ℝ^m is a linear transformation, then there exists a constant M > 0 such that ‖T x‖ ≤ M * ‖x‖ for all x : ℝ^n. Consequently, T is continuous on ℝ^n.