Tensor rank and border rank: proof internals #
Proofs behind Complexitylib.Algebraic.LinearAlgebra.Tensor.BorderRank: the algebra of
RankLE (sums, scalar multiples, monotonicity, existence of a decomposition), its transport
along map and subtensor, the composition of maps (map_map, proved on outer products), and
the corresponding closure arguments for BorderRankLE.
theorem
Algebraic.Tensor3.Internal.rankLE_card_mul_card
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Fintype α]
[Fintype β]
(T : Tensor3 α β γ)
:
T.RankLE (Fintype.card α * Fintype.card β)
theorem
Algebraic.Tensor3.Internal.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
theorem
Algebraic.Tensor3.Internal.map_one
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Fintype α]
[Fintype β]
[Fintype γ]
[DecidableEq α]
[DecidableEq β]
[DecidableEq γ]
(T : Tensor3 α β γ)
:
theorem
Algebraic.Tensor3.Internal.map_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{α' : Type u_4}
{β' : Type u_5}
{γ' : Type u_6}
[Fintype α]
[Fintype β]
[Fintype γ]
[Fintype α']
[Fintype β']
[Fintype γ']
{α'' : Type u_7}
{β'' : Type u_8}
{γ'' : Type u_9}
(X : Matrix α' α ℂ)
(Y : Matrix β' β ℂ)
(Z : Matrix γ' γ ℂ)
(X' : Matrix α'' α' ℂ)
(Y' : Matrix β'' β' ℂ)
(Z' : Matrix γ'' γ' ℂ)
(T : Tensor3 α β γ)
:
theorem
Algebraic.Tensor3.Internal.borderRankLE_of_rankLE
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{T : Tensor3 α β γ}
{r : ℕ}
(h : T.RankLE r)
:
T.BorderRankLE r
theorem
Algebraic.Tensor3.Internal.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'
theorem
Algebraic.Tensor3.Internal.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')
theorem
Algebraic.Tensor3.Internal.borderRankLE_smul
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{T : Tensor3 α β γ}
{r : ℕ}
(c : ℂ)
(h : T.BorderRankLE r)
:
(c • T).BorderRankLE r
theorem
Algebraic.Tensor3.Internal.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)
:
(map X Y Z T).BorderRankLE r
theorem
Algebraic.Tensor3.Internal.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
theorem
Algebraic.Tensor3.Internal.borderRankLE_zero_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{T : Tensor3 α β γ}
:
theorem
Algebraic.Tensor3.Internal.rankLE_tensorRank
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Fintype α]
[Fintype β]
(T : Tensor3 α β γ)
:
T.RankLE T.tensorRank