Basic properties of tensor rank and border rank

For 3-tensors T : Tensor3 α β γ (see Complexitylib.Algebraic.LinearAlgebra.Tensor.Defs):

• Rank. RankLE is closed under sums (RankLE.add, RankLE.sum) and scalar multiples, is monotone in the bound (RankLE.mono), and every tensor over finite α, β has rank at most card α * card β (rankLE_card_mul_card), so tensorRank is attained (rankLE_tensorRank, tensorRank_le_iff).
• Border rank. Rank at most r implies border rank at most r (RankLE.borderRankLE); BorderRankLE is monotone, closed under sums and scalar multiples, and defines a closed set of tensors (isClosed_setOf_borderRankLE). borderRank is attained, and borderRank T ≤ tensorRank T.
• Linear maps on the factors. map X Y Z sends outer products to outer products (map_outer), is additive and continuous, and composes as matrices multiply (map_map), so it preserves RankLE and BorderRankLE: rank and border rank do not increase under X ⊗ Y ⊗ Z (tensorRank_map_le, borderRank_map_le). Taking Y = Z = 1 gives restriction or projection along the first factor by any linear map ℂ^α → ℂ^α'.
• Reindexing. subtensor (deleting, permuting, or repeating slices in any factor) also preserves RankLE and BorderRankLE.

theorem Algebraic.Tensor3.rankLE_zero_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {T : Tensor3 α β γ} : T.RankLE 0 ↔ T = 0

A tensor has rank at most 0 exactly when it is zero.

theorem Algebraic.Tensor3.rankLE_one_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {T : Tensor3 α β γ} : T.RankLE 1 ↔ ∃ (u : α → ℂ) (v : β → ℂ) (w : γ → ℂ), T = outer u v w

A tensor has rank at most 1 exactly when it is an outer product u ⊗ v ⊗ w.

theorem Algebraic.Tensor3.rankLE_outer {α : Type u_1} {β : Type u_2} {γ : Type u_3} (u : α → ℂ) (v : β → ℂ) (w : γ → ℂ) : (outer u v w).RankLE 1

An outer product has rank at most one.

theorem Algebraic.Tensor3.zero_rankLE {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : ℕ) : RankLE 0 r

The zero tensor has rank at most r for every r.

theorem Algebraic.Tensor3.RankLE.add {α : Type u_1} {β : Type u_2} {γ : Type u_3} {S T : Tensor3 α β γ} {r r' : ℕ} (hS : S.RankLE r) (hT : T.RankLE r') : (S + T).RankLE (r + r')

Rank is subadditive.

theorem Algebraic.Tensor3.RankLE.mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {T : Tensor3 α β γ} {r r' : ℕ} (h : T.RankLE r) (hr : r ≤ r') : T.RankLE r'

RankLE is monotone in the bound.

theorem Algebraic.Tensor3.RankLE.sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_7} {s : Finset ι} {T : ι → Tensor3 α β γ} {r : ι → ℕ} (h : ∀ x ∈ s, (T x).RankLE (r x)) : (∑ x ∈ s, T x).RankLE (∑ x ∈ s, r x)

Rank is subadditive over finite sums.

theorem Algebraic.Tensor3.RankLE.smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} {T : Tensor3 α β γ} {r : ℕ} (c : ℂ) (h : T.RankLE r) : (c • T).RankLE r

Scalar multiples do not increase rank.

theorem Algebraic.Tensor3.rankLE_card_mul_card {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] (T : Tensor3 α β γ) : T.RankLE (Fintype.card α * Fintype.card β)

Every tensor over finite α and β is a sum of card α * card β outer products.

theorem Algebraic.Tensor3.rankLE_tensorRank {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] (T : Tensor3 α β γ) : T.RankLE T.tensorRank

The tensor rank is attained.

theorem Algebraic.Tensor3.tensorRank_le_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] {T : Tensor3 α β γ} {r : ℕ} : T.tensorRank ≤ r ↔ T.RankLE r

tensorRank T ≤ r exactly when T is a sum of r outer products.

theorem Algebraic.Tensor3.tensorRank_add_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] (S T : Tensor3 α β γ) : (S + T).tensorRank ≤ S.tensorRank + T.tensorRank

Tensor rank is subadditive.

theorem Algebraic.Tensor3.RankLE.borderRankLE {α : Type u_1} {β : Type u_2} {γ : Type u_3} {T : Tensor3 α β γ} {r : ℕ} (h : T.RankLE r) : T.BorderRankLE r

Rank at most r implies border rank at most r.

theorem Algebraic.Tensor3.BorderRankLE.mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {T : Tensor3 α β γ} {r r' : ℕ} (h : T.BorderRankLE r) (hr : r ≤ r') : T.BorderRankLE r'

BorderRankLE is monotone in the bound.

theorem Algebraic.Tensor3.isClosed_setOf_borderRankLE {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : ℕ) : IsClosed {T : Tensor3 α β γ | T.BorderRankLE r}

The tensors of border rank at most r form a closed set.

theorem Algebraic.Tensor3.BorderRankLE.add {α : Type u_1} {β : Type u_2} {γ : Type u_3} {S T : Tensor3 α β γ} {r r' : ℕ} (hS : S.BorderRankLE r) (hT : T.BorderRankLE r') : (S + T).BorderRankLE (r + r')

Border rank is subadditive.

theorem Algebraic.Tensor3.BorderRankLE.smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} {T : Tensor3 α β γ} {r : ℕ} (c : ℂ) (h : T.BorderRankLE r) : (c • T).BorderRankLE r

Scalar multiples do not increase border rank.

theorem Algebraic.Tensor3.borderRankLE_zero_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {T : Tensor3 α β γ} : T.BorderRankLE 0 ↔ T = 0

A tensor has border rank at most 0 exactly when it is zero.

theorem Algebraic.Tensor3.borderRankLE_borderRank {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] (T : Tensor3 α β γ) : T.BorderRankLE T.borderRank

The border rank is attained.

theorem Algebraic.Tensor3.borderRank_le_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] {T : Tensor3 α β γ} {r : ℕ} : T.borderRank ≤ r ↔ T.BorderRankLE r

borderRank T ≤ r exactly when T is a limit of tensors of rank at most r.

theorem Algebraic.Tensor3.borderRank_le_tensorRank {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] (T : Tensor3 α β γ) : T.borderRank ≤ T.tensorRank

Border rank is at most rank.

theorem Algebraic.Tensor3.borderRank_add_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] (S T : Tensor3 α β γ) : (S + T).borderRank ≤ S.borderRank + T.borderRank

Border rank is subadditive.

theorem Algebraic.Tensor3.map_outer {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} [Fintype α] [Fintype β] [Fintype γ] (X : Matrix α' α ℂ) (Y : Matrix β' β ℂ) (Z : Matrix γ' γ ℂ) (u : α → ℂ) (v : β → ℂ) (w : γ → ℂ) : map X Y Z (outer u v w) = outer (X.mulVec u) (Y.mulVec v) (Z.mulVec w)

X ⊗ Y ⊗ Z sends u ⊗ v ⊗ w to Xu ⊗ Yv ⊗ Zw.

theorem Algebraic.Tensor3.map_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} [Fintype α] [Fintype β] [Fintype γ] (X : Matrix α' α ℂ) (Y : Matrix β' β ℂ) (Z : Matrix γ' γ ℂ) (S T : Tensor3 α β γ) : map X Y Z (S + T) = map X Y Z S + map X Y Z T

theorem Algebraic.Tensor3.map_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} [Fintype α] [Fintype β] [Fintype γ] (X : Matrix α' α ℂ) (Y : Matrix β' β ℂ) (Z : Matrix γ' γ ℂ) : map X Y Z 0 = 0

theorem Algebraic.Tensor3.map_smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} [Fintype α] [Fintype β] [Fintype γ] (X : Matrix α' α ℂ) (Y : Matrix β' β ℂ) (Z : Matrix γ' γ ℂ) (c : ℂ) (T : Tensor3 α β γ) : map X Y Z (c • T) = c • map X Y Z T

theorem Algebraic.Tensor3.map_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} [Fintype α] [Fintype β] [Fintype γ] (X : Matrix α' α ℂ) (Y : Matrix β' β ℂ) (Z : Matrix γ' γ ℂ) {ι : Type u_7} (s : Finset ι) (T : ι → Tensor3 α β γ) : map X Y Z (∑ x ∈ s, T x) = ∑ x ∈ s, map X Y Z (T x)

theorem Algebraic.Tensor3.continuous_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} [Fintype α] [Fintype β] [Fintype γ] (X : Matrix α' α ℂ) (Y : Matrix β' β ℂ) (Z : Matrix γ' γ ℂ) : Continuous (map X Y Z)

theorem Algebraic.Tensor3.map_diagonal {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq α] [DecidableEq β] [DecidableEq γ] (a : α → ℂ) (b : β → ℂ) (c : γ → ℂ) (T : Tensor3 α β γ) : map (Matrix.diagonal a) (Matrix.diagonal b) (Matrix.diagonal c) T = fun (i : α) (j : β) (k : γ) => a i * b j * c k * T i j k

Diagonal matrices scale the coordinates.

theorem Algebraic.Tensor3.map_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq α] [DecidableEq β] [DecidableEq γ] (T : Tensor3 α β γ) : map 1 1 1 T = T

The identity maps fix every tensor.

theorem Algebraic.Tensor3.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} [Fintype α] [Fintype β] [Fintype γ] (X : Matrix α' α ℂ) (Y : Matrix β' β ℂ) (Z : Matrix γ' γ ℂ) [Fintype α'] [Fintype β'] [Fintype γ'] {α'' : Type u_7} {β'' : Type u_8} {γ'' : Type u_9} (X' : Matrix α'' α' ℂ) (Y' : Matrix β'' β' ℂ) (Z' : Matrix γ'' γ' ℂ) (T : Tensor3 α β γ) : map X' Y' Z' (map X Y Z T) = map (X' * X) (Y' * Y) (Z' * Z) T

Applying X ⊗ Y ⊗ Z and then X' ⊗ Y' ⊗ Z' is applying X'X ⊗ Y'Y ⊗ Z'Z.

theorem Algebraic.Tensor3.RankLE.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} [Fintype α] [Fintype β] [Fintype γ] (X : Matrix α' α ℂ) (Y : Matrix β' β ℂ) (Z : Matrix γ' γ ℂ) {T : Tensor3 α β γ} {r : ℕ} (h : T.RankLE r) : (Tensor3.map X Y Z T).RankLE r

Linear maps on the factors do not increase rank.

theorem Algebraic.Tensor3.BorderRankLE.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} [Fintype α] [Fintype β] [Fintype γ] (X : Matrix α' α ℂ) (Y : Matrix β' β ℂ) (Z : Matrix γ' γ ℂ) {T : Tensor3 α β γ} {r : ℕ} (h : T.BorderRankLE r) : (Tensor3.map X Y Z T).BorderRankLE r

Linear maps on the factors do not increase border rank.

theorem Algebraic.Tensor3.tensorRank_map_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} [Fintype α] [Fintype β] [Fintype γ] (X : Matrix α' α ℂ) (Y : Matrix β' β ℂ) (Z : Matrix γ' γ ℂ) [Fintype α'] [Fintype β'] (T : Tensor3 α β γ) : (map X Y Z T).tensorRank ≤ T.tensorRank

Linear maps on the factors do not increase tensor rank.

theorem Algebraic.Tensor3.borderRank_map_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} [Fintype α] [Fintype β] [Fintype γ] (X : Matrix α' α ℂ) (Y : Matrix β' β ℂ) (Z : Matrix γ' γ ℂ) [Fintype α'] [Fintype β'] (T : Tensor3 α β γ) : (map X Y Z T).borderRank ≤ T.borderRank

Linear maps on the factors do not increase border rank.

theorem Algebraic.Tensor3.subtensor_outer {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} (f : α' → α) (g : β' → β) (h : γ' → γ) (u : α → ℂ) (v : β → ℂ) (w : γ → ℂ) : (outer u v w).subtensor f g h = outer (u ∘ f) (v ∘ g) (w ∘ h)

theorem Algebraic.Tensor3.continuous_subtensor {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} (f : α' → α) (g : β' → β) (h : γ' → γ) : Continuous fun (T : Tensor3 α β γ) => T.subtensor f g h

theorem Algebraic.Tensor3.RankLE.subtensor {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} (f : α' → α) (g : β' → β) (h : γ' → γ) {T : Tensor3 α β γ} {r : ℕ} (hT : T.RankLE r) : (T.subtensor f g h).RankLE r

Reindexing does not increase rank.

theorem Algebraic.Tensor3.BorderRankLE.subtensor {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} (f : α' → α) (g : β' → β) (h : γ' → γ) {T : Tensor3 α β γ} {r : ℕ} (hT : T.BorderRankLE r) : (T.subtensor f g h).BorderRankLE r

Reindexing, in particular deleting or permuting slices, does not increase border rank.

theorem Algebraic.Tensor3.tensorRank_subtensor_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} (f : α' → α) (g : β' → β) (h : γ' → γ) [Fintype α] [Fintype β] [Fintype α'] [Fintype β'] (T : Tensor3 α β γ) : (T.subtensor f g h).tensorRank ≤ T.tensorRank

Reindexing does not increase tensor rank.

theorem Algebraic.Tensor3.borderRank_subtensor_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} (f : α' → α) (g : β' → β) (h : γ' → γ) [Fintype α] [Fintype β] [Fintype α'] [Fintype β'] (T : Tensor3 α β γ) : (T.subtensor f g h).borderRank ≤ T.borderRank

Reindexing, in particular deleting or permuting slices, does not increase border rank.