Border substitution for tight tensors: proof internals

Proofs behind Complexitylib.Algebraic.LinearAlgebra.Tensor.Substitution.

• Only the kernel matters. Over a field, ker P ⊆ ker P' gives P' = G * P (factor P' through ℂ^α ⧸ ker P ≅ range P and extend from range P), so X ↦ map X Y Z T at P' is the image under G ⊗ 1 ⊗ 1 of its value at P.
• One step. Approximate T by T_n = ∑_{s < r + 1} u_{n,s} ⊗ v_{n,s} ⊗ w_{n,s}. A unit vector û_n on the line of u_{n,0} (any unit vector if u_{n,0} = 0) makes orthProj û_n kill the first summand, so (orthProj û_n ⊗ 1 ⊗ 1) T_n has rank at most r. A subsequence of û_n converges on the compact unit sphere of the sup norm, to some u ≠ 0, and (X, S) ↦ (X ⊗ 1 ⊗ 1) S and orthProj (at u ≠ 0) are continuous.
• Torus limit. With weights σ i = τA i - τA i₀ for the i₀ minimizing τA on the support of u (and τC shifted to compensate), λ(t) = diag(t ^ σ i) fixes T together with the matching diagonal maps on B and C. Conjugating gives a border-rank bound for the projection with kernel ℂ λ(t) u. Along t = 2⁻ⁿ, λ(t) u → u i₀ • e_{i₀}, since σ i > 0 for every other i in the support (τA is injective), and the set of v whose projection satisfies the bound is closed at v ≠ 0. The projection along e_{i₀} has the same kernel as the diagonal 0/1 matrix that zeroes slice i₀.
• Deletion. For T restricted to S, the zeroed slice i₀ is in S, or else the bound already holds for the restriction to S and any further deletion keeps it. Iterating gives the deletion order; once the bound reaches 0, the restricted tensor is zero, which forces at most r nonzero slices.

theorem Algebraic.Tensor3.Internal.orthProj_mulVec {α : Type u_1} [Fintype α] [DecidableEq α] (u v : α → ℂ) : (orthProj u).mulVec v = v - ((star u ⬝ᵥ u)⁻¹ * star u ⬝ᵥ v) • u

theorem Algebraic.Tensor3.Internal.star_dotProduct_self_ne_zero {α : Type u_1} [Fintype α] {u : α → ℂ} (hu : u ≠ 0) : star u ⬝ᵥ u ≠ 0

theorem Algebraic.Tensor3.Internal.orthProj_mulVec_self {α : Type u_1} [Fintype α] [DecidableEq α] (u : α → ℂ) : (orthProj u).mulVec u = 0

theorem Algebraic.Tensor3.Internal.orthProj_mulVec_eq_zero_iff {α : Type u_1} [Fintype α] [DecidableEq α] {u v : α → ℂ} : (orthProj u).mulVec v = 0 ↔ ∃ (c : ℂ), v = c • u

theorem Algebraic.Tensor3.Internal.continuousAt_orthProj {α : Type u_1} [Fintype α] [DecidableEq α] {u : α → ℂ} (hu : u ≠ 0) : ContinuousAt orthProj u

theorem Algebraic.Tensor3.Internal.exists_mem_sphere_orthProj_mulVec_eq_zero {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] (x : α → ℂ) : ∃ u ∈ Metric.sphere 0 1, (orthProj u).mulVec x = 0

Some unit vector u (for the sup norm) has orthProj u vanishing at x.

theorem Algebraic.Tensor3.Internal.exists_mul_eq_of_ker {α : Type u_1} {α' : Type u_4} {α'' : Type u_7} [Fintype α] [Fintype α'] {P : Matrix α' α ℂ} {P' : Matrix α'' α ℂ} (h : ∀ (v : α → ℂ), P.mulVec v = 0 → P'.mulVec v = 0) : ∃ (G : Matrix α'' α' ℂ), G * P = P'

Over a field, ker P ⊆ ker P' lets P' factor as G * P.

theorem Algebraic.Tensor3.Internal.borderRankLE_map_of_ker {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} {α'' : Type u_7} [Fintype α] [Fintype β] [Fintype γ] [Fintype α'] [Fintype β'] [Fintype γ'] {P : Matrix α' α ℂ} {P' : Matrix α'' α ℂ} (Y : Matrix β' β ℂ) (Z : Matrix γ' γ ℂ) {T : Tensor3 α β γ} {ρ : ℕ} (h : (map P Y Z T).BorderRankLE ρ) (hker : ∀ (v : α → ℂ), P.mulVec v = 0 → P'.mulVec v = 0) : (map P' Y Z T).BorderRankLE ρ

theorem Algebraic.Tensor3.Internal.continuous_map_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq β] [DecidableEq γ] : Continuous fun (p : Matrix α' α ℂ × Tensor3 α β γ) => map p.1 1 1 p.2

theorem Algebraic.Tensor3.Internal.continuous_map_left_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq β] [DecidableEq γ] (T : Tensor3 α β γ) : Continuous fun (X : Matrix α' α ℂ) => map X 1 1 T

theorem Algebraic.Tensor3.Internal.restrictSlices_restrictSlices {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] (T : Tensor3 α β γ) (S S' : Finset α) : (T.restrictSlices S).restrictSlices S' = T.restrictSlices (S' ∩ S)

theorem Algebraic.Tensor3.Internal.restrictSlices_univ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [Fintype α] (T : Tensor3 α β γ) : T.restrictSlices Finset.univ = T

theorem Algebraic.Tensor3.Internal.restrictSlices_empty {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] (T : Tensor3 α β γ) : T.restrictSlices ∅ = 0

theorem Algebraic.Tensor3.Internal.zero_restrictSlices {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] (S : Finset α) : restrictSlices 0 S = 0

theorem Algebraic.Tensor3.Internal.restrictSlices_eq_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [Fintype α] [Fintype β] [Fintype γ] [DecidableEq β] [DecidableEq γ] (T : Tensor3 α β γ) (S : Finset α) : T.restrictSlices S = map (Matrix.diagonal fun (i : α) => if i ∈ S then 1 else 0) 1 1 T

theorem Algebraic.Tensor3.Internal.tight_restrictSlices {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] {T : Tensor3 α β γ} (hT : T.Tight) (S : Finset α) : (T.restrictSlices S).Tight

theorem Algebraic.Tensor3.Internal.borderRankLE_restrictSlices_of_subset {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [Fintype α] [Fintype β] [Fintype γ] [DecidableEq β] [DecidableEq γ] {T : Tensor3 α β γ} {S S' : Finset α} {ρ : ℕ} (h : (T.restrictSlices S).BorderRankLE ρ) (hS : S' ⊆ S) : (T.restrictSlices S').BorderRankLE ρ

theorem Algebraic.Tensor3.Internal.borderRankLE_restrictSlices {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [Fintype α] [Fintype β] [Fintype γ] [DecidableEq β] [DecidableEq γ] {T : Tensor3 α β γ} {ρ : ℕ} (h : T.BorderRankLE ρ) (S : Finset α) : (T.restrictSlices S).BorderRankLE ρ

theorem Algebraic.Tensor3.Internal.borderRankLE_zero_tensor {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : ℕ) : BorderRankLE 0 r

theorem Algebraic.Tensor3.Internal.exists_mem_sphere_rankLE_map_orthProj {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [Fintype β] [Fintype γ] [DecidableEq β] [DecidableEq γ] [Nonempty α] {S : Tensor3 α β γ} {r : ℕ} (h : S.RankLE (r + 1)) : ∃ u ∈ Metric.sphere 0 1, (map (orthProj u) 1 1 S).RankLE r

A tensor of rank at most r + 1 has rank at most r after projecting the first factor along a suitable unit vector.

theorem Algebraic.Tensor3.Internal.exists_borderRankLE_map_orthProj {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [Fintype β] [Fintype γ] [DecidableEq β] [DecidableEq γ] [Nonempty α] {T : Tensor3 α β γ} {r : ℕ} (h : T.BorderRankLE (r + 1)) : ∃ (u : α → ℂ), u ≠ 0 ∧ (map (orthProj u) 1 1 T).BorderRankLE r

noncomputable def Algebraic.Tensor3.Internal.torus {ι : Type u_8} [DecidableEq ι] (τ : ι → ℤ) (t : ℂ) : Matrix ι ι ℂ

The diagonal matrix diag(t ^ τ i): the one-parameter subgroup with weights τ.

Equations

• Algebraic.Tensor3.Internal.torus τ t = Matrix.diagonal fun (i : ι) => t ^ τ i

theorem Algebraic.Tensor3.Internal.torus_mul_torus_inv {ι : Type u_8} [Fintype ι] [DecidableEq ι] (τ : ι → ℤ) {t : ℂ} (ht : t ≠ 0) : torus τ t * torus τ t⁻¹ = 1

theorem Algebraic.Tensor3.Internal.map_torus {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [Fintype β] [Fintype γ] [DecidableEq β] [DecidableEq γ] {T : Tensor3 α β γ} {τA : α → ℤ} {τB : β → ℤ} {τC : γ → ℤ} (hT : ∀ (i : α) (j : β) (k : γ), T i j k ≠ 0 → τA i + τB j + τC k = 0) {t : ℂ} (ht : t ≠ 0) : map (torus τA t) (torus τB t) (torus τC t) T = T

theorem Algebraic.Tensor3.Internal.borderRankLE_map_orthProj_torus {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [Fintype β] [Fintype γ] [DecidableEq β] [DecidableEq γ] {T : Tensor3 α β γ} {τA : α → ℤ} {τB : β → ℤ} {τC : γ → ℤ} (hT : ∀ (i : α) (j : β) (k : γ), T i j k ≠ 0 → τA i + τB j + τC k = 0) {t : ℂ} (ht : t ≠ 0) {u : α → ℂ} {ρ : ℕ} (h : (map (orthProj u) 1 1 T).BorderRankLE ρ) : (map (orthProj ((torus τA t).mulVec u)) 1 1 T).BorderRankLE ρ

The torus fixing T moves the projection direction u to torus τA t *ᵥ u without changing the border-rank bound.

theorem Algebraic.Tensor3.Internal.exists_borderRankLE_restrictSlices_erase_of_tight {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [Fintype β] [Fintype γ] [DecidableEq β] [DecidableEq γ] {T : Tensor3 α β γ} (hT : T.Tight) {u : α → ℂ} (hu : u ≠ 0) {ρ : ℕ} (h : (map (orthProj u) 1 1 T).BorderRankLE ρ) : ∃ (i : α), u i ≠ 0 ∧ (T.restrictSlices (Finset.univ.erase i)).BorderRankLE ρ

theorem Algebraic.Tensor3.Internal.exists_mem_borderRankLE_restrictSlices_erase {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [Fintype β] [Fintype γ] [DecidableEq β] [DecidableEq γ] {T : Tensor3 α β γ} (hT : T.Tight) {S : Finset α} (hS : S.Nonempty) {r : ℕ} (h : (T.restrictSlices S).BorderRankLE (r + 1)) : ∃ i ∈ S, (T.restrictSlices (S.erase i)).BorderRankLE r

theorem Algebraic.Tensor3.Internal.exists_list_borderRankLE_restrictSlices_sdiff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [Fintype β] [Fintype γ] [DecidableEq β] [DecidableEq γ] {T : Tensor3 α β γ} (hT : T.Tight) (S₀ : Finset α) {r : ℕ} (h : (T.restrictSlices S₀).BorderRankLE r) : ∃ (l : List α), l.Nodup ∧ l.toFinset = S₀ ∧ ∀ (q : ℕ), (T.restrictSlices (S₀ \ (List.take q l).toFinset)).BorderRankLE (r - q)

theorem Algebraic.Tensor3.Internal.card_le_of_borderRankLE_restrictSlices {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [Fintype β] [Fintype γ] [DecidableEq β] [DecidableEq γ] {T : Tensor3 α β γ} (hT : T.Tight) {S : Finset α} (hS : ∀ i ∈ S, T i ≠ 0) {r : ℕ} (h : (T.restrictSlices S).BorderRankLE r) : S.card ≤ r

theorem Algebraic.Tensor3.Internal.exists_list_add_borderRank_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [Fintype β] [Fintype γ] [DecidableEq β] [DecidableEq γ] {T : Tensor3 α β γ} (hT : T.Tight) {S₀ : Finset α} (hS : ∀ i ∈ S₀, T i ≠ 0) : ∃ (l : List α), l.Nodup ∧ l.toFinset = S₀ ∧ ∀ q ≤ S₀.card, q + (T.restrictSlices (S₀ \ (List.take q l).toFinset)).borderRank ≤ (T.restrictSlices S₀).borderRank

theorem Algebraic.Tensor3.Internal.not_borderRankLE_restrictSlices_of_forall_list {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [Fintype β] [Fintype γ] [DecidableEq β] [DecidableEq γ] {T : Tensor3 α β γ} (hT : T.Tight) {S₀ : Finset α} (hS : ∀ i ∈ S₀, T i ≠ 0) {r : ℕ} (LB : Finset α → ℕ) (hLB : ∀ S ⊆ S₀, ∀ (ρ : ℕ), (T.restrictSlices S).BorderRankLE ρ → LB S ≤ ρ) (h : ∀ (l : List α), l.Nodup → l.toFinset = S₀ → ∃ q ≤ S₀.card, r < q + LB (S₀ \ (List.take q l).toFinset)) : ¬(T.restrictSlices S₀).BorderRankLE r