Koszul flattenings of cluster tensors: proof internals

Proofs behind Complexitylib.Algebraic.LinearAlgebra.Tensor.Diagonal.

• Matching. exists_equiv_subset: for card α = 2p + 1 a bijection σ from the p-subsets to the (p + 1)-subsets with I ⊆ σ I, by Hall's theorem; the inclusion graph is (p + 1)-regular on both sides, so Hall's condition follows by double counting.
• Entries. The ((J, ℓ), (I, j)) entry of the Koszul flattening of weightedShifts o g is wedgeCoeff J I t * g t j when J = insert t I with t ∉ I and ℓ = j + o t, and 0 otherwise (koszulFlattening_weightedShifts_eq_zero).
• One block. det_submatrix_shift_ne_zero: for a shift w, the minor with columns (I, w + ∑_I o) and rows (σ I, w + ∑_{σ I} o) is nonsingular by Matrix.det_ne_zero_of_two_pow_two_pow with the identity permutation as the perfect matching: the entry in row σ I, column I' has the label e t (w + ∑_{I'} o), where t is the element with σ I = insert t I' (insertedElt).
• A window of blocks. choose_mul_card_le_rank_of_shifts: for pairwise distinct shifts w q whose positions lie in [0, m), entries between different blocks vanish because w is preserved, so the blocks form a block-diagonal minor. choose_mul_le_rank_of_bounds is the case where all sums over subsets of size p or p + 1 lie in [lo, lo + D] and the shifts are w = i - lo for i : Fin (m - D).
• Spread. exists_bounds produces lo with D = sumSpread p o; sumSpread_le compares each sum with the median: the elements above the median add at most p (o (2p) - r), those below subtract at most p (r - o 0), and the sizes differ by at most one.

theorem Algebraic.Tensor3.Internal.Diagonal.map_selectSlices {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_4} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [Fintype γ] [DecidableEq γ] (c : α' → α) (T : Tensor3 α β γ) : map (selectSlices c) 1 1 T = T.subtensor c id id

theorem Algebraic.Tensor3.Internal.Diagonal.map_diagonal_apply {α : Type u_1} {β : Type u_3} {γ : Type u_4} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [Fintype γ] [DecidableEq γ] (d : α → ℂ) (T : Tensor3 α β γ) (a : α) (j : β) (l : γ) : map (Matrix.diagonal d) 1 1 T a j l = d a * T a j l

theorem Algebraic.Tensor3.Internal.Diagonal.map_selectSlices_map_diagonal {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_4} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] [Fintype γ] [DecidableEq γ] (c : α' → α) (d : α → ℂ) (hd : ∀ (t : α'), d (c t) = 1) (T : Tensor3 α β γ) : map (selectSlices c) 1 1 (map (Matrix.diagonal d) 1 1 T) = map (selectSlices c) 1 1 T

theorem Algebraic.Tensor3.Internal.Diagonal.subtensor_lmTensor (k : ℕ) (γ : Fin (2 * k + 1) → Fin (2 * k + 1) → ℂ) {n : ℕ} (c : Fin n → Fin (2 * k + 1)) : (lmTensor k γ).subtensor c id id = weightedShifts (clusterOffsets k c) fun (t : Fin n) (j : Fin (2 * k + 1)) => γ (c t) j

theorem Algebraic.Tensor3.Internal.Diagonal.wedgeCoeff_eq_zero_of_ne {α : Type u_1} [LinearOrder α] {J I : Finset α} {t t' : α} (hJ : insert t I = J) (hne : t' ≠ t) : wedgeCoeff J I t' = 0

theorem Algebraic.Tensor3.Internal.Diagonal.wedgeCoeff_eq_zero_of_not_exists {α : Type u_1} [LinearOrder α] {J I : Finset α} (h : ¬∃ t ∉ I, insert t I = J) (t : α) : wedgeCoeff J I t = 0

theorem Algebraic.Tensor3.Internal.Diagonal.wedgeCoeff_of_insert {α : Type u_1} [LinearOrder α] {J I : Finset α} {t : α} (ht : t ∉ I) (hJ : insert t I = J) : wedgeCoeff J I t = (-1) ^ {x ∈ I | x < t}.card

theorem Algebraic.Tensor3.Internal.Diagonal.sum_wedgeCoeff_mul_of_insert {α : Type u_1} [LinearOrder α] [Fintype α] {J I : Finset α} {t : α} (hJ : insert t I = J) (F : α → ℂ) : ∑ t' : α, wedgeCoeff J I t' * F t' = wedgeCoeff J I t * F t

theorem Algebraic.Tensor3.Internal.Diagonal.sum_wedgeCoeff_mul_of_not_exists {α : Type u_1} [LinearOrder α] [Fintype α] {J I : Finset α} (h : ¬∃ t ∉ I, insert t I = J) (F : α → ℂ) : ∑ t' : α, wedgeCoeff J I t' * F t' = 0

theorem Algebraic.Tensor3.Internal.Diagonal.koszulFlattening_weightedShifts_apply {α : Type u_1} [LinearOrder α] [Fintype α] {m p : ℕ} (o : α → ℤ) (g : α → Fin m → ℂ) (J : { J : Finset α // J.card = p + 1 }) (ℓ : Fin m) (I : { I : Finset α // I.card = p }) (j : Fin m) : koszulFlattening p (weightedShifts o g) (J, ℓ) (I, j) = ∑ t : α, wedgeCoeff (↑J) (↑I) t * if ↑↑ℓ = ↑↑j + o t then g t j else 0

theorem Algebraic.Tensor3.Internal.Diagonal.koszulFlattening_weightedShifts_eq_zero {α : Type u_1} [LinearOrder α] [Fintype α] {m p : ℕ} (o : α → ℤ) (g : α → Fin m → ℂ) (J : { J : Finset α // J.card = p + 1 }) (ℓ : Fin m) (I : { I : Finset α // I.card = p }) (j : Fin m) (h : ∀ t ∉ ↑I, insert t ↑I = ↑J → ↑↑ℓ ≠ ↑↑j + o t) : koszulFlattening p (weightedShifts o g) (J, ℓ) (I, j) = 0

An entry of the Koszul flattening of weighted shifts in row (J, ℓ) and column (I, j) vanishes unless ℓ = j + o t for the element t ∉ I with insert t I = J.

theorem Algebraic.Tensor3.Internal.Diagonal.card_sub_le_card_filter_superset {α : Type u_1} [Fintype α] [DecidableEq α] {p : ℕ} (I : { I : Finset α // I.card = p }) (s : Finset { J : Finset α // J.card = p + 1 }) (hs : ∀ (J : { J : Finset α // J.card = p + 1 }), ↑I ⊆ ↑J → J ∈ s) : Fintype.card α - p ≤ {J ∈ s | ↑I ⊆ ↑J}.card

Every p-subset of an n-set with p < n has at least n - p supersets of size p + 1 in any family containing all of them.

theorem Algebraic.Tensor3.Internal.Diagonal.card_filter_subset_le {α : Type u_1} [DecidableEq α] {p : ℕ} (J : { J : Finset α // J.card = p + 1 }) (s : Finset { I : Finset α // I.card = p }) : {I ∈ s | ↑I ⊆ ↑J}.card ≤ p + 1

A (p + 1)-set has p + 1 subsets of size p.

theorem Algebraic.Tensor3.Internal.Diagonal.exists_equiv_subset {α : Type u_1} [Fintype α] [DecidableEq α] {p : ℕ} (hα : Fintype.card α = 2 * p + 1) : ∃ (e : { I : Finset α // I.card = p } ≃ { J : Finset α // J.card = p + 1 }), ∀ (I : { I : Finset α // I.card = p }), ↑I ⊆ ↑(e I)

A perfect matching in the inclusion graph. For card α = 2p + 1 there is a bijection from the p-subsets to the (p + 1)-subsets of α sending each I to a superset of I. The inclusion graph is (p + 1)-regular on both sides, so Hall's condition holds by double counting.

noncomputable def Algebraic.Tensor3.Internal.Diagonal.insertedElt {α : Type u_1} [Nonempty α] [DecidableEq α] (J I : Finset α) : α

The element t with t ∉ I and insert t I = J, if there is one.

Equations

• Algebraic.Tensor3.Internal.Diagonal.insertedElt J I = Classical.epsilon fun (t : α) => t ∉ I ∧ insert t I = J

theorem Algebraic.Tensor3.Internal.Diagonal.insertedElt_eq {α : Type u_1} [Nonempty α] [DecidableEq α] {J I : Finset α} {t : α} (ht : t ∉ I) (hJ : insert t I = J) : insertedElt J I = t

theorem Algebraic.Tensor3.Internal.Diagonal.det_submatrix_shift_ne_zero {p m : ℕ} (o : Fin (2 * p + 1) → ℤ) (g : Fin (2 * p + 1) → Fin m → ℂ) (e : Fin (2 * p + 1) → Fin m → ℕ) (ho : Set.InjOn (fun (I : Finset (Fin (2 * p + 1))) => ∑ t ∈ I, o t) {I : Finset (Fin (2 * p + 1)) | I.card = p}) (hg : ∀ (t : Fin (2 * p + 1)) (j : Fin m), g t j = 2 ^ 2 ^ e t j) (D : ℕ) (hD : ∀ (I I' : Finset (Fin (2 * p + 1))), I.card = p → I'.card = p → ∑ t ∈ I, o t - ∑ t ∈ I', o t ≤ ↑D) (he : ∀ (t t' : Fin (2 * p + 1)) (j j' : Fin m), |↑↑j - ↑↑j'| ≤ ↑D → e t j = e t' j' → t = t' ∧ j = j') (σ : { I : Finset (Fin (2 * p + 1)) // I.card = p } ≃ { J : Finset (Fin (2 * p + 1)) // J.card = p + 1 }) (hσ : ∀ (I : { I : Finset (Fin (2 * p + 1)) // I.card = p }), ↑I ⊆ ↑(σ I)) (w : ℤ) (ℓ j : { I : Finset (Fin (2 * p + 1)) // I.card = p } → Fin m) (hℓ : ∀ (I : { I : Finset (Fin (2 * p + 1)) // I.card = p }), ↑↑(ℓ I) = w + ∑ t ∈ ↑(σ I), o t) (hj : ∀ (I : { I : Finset (Fin (2 * p + 1)) // I.card = p }), ↑↑(j I) = w + ∑ t ∈ ↑I, o t) : ((koszulFlattening p (weightedShifts o g)).submatrix (fun (I : { I : Finset (Fin (2 * p + 1)) // I.card = p }) => (σ I, ℓ I)) fun (I : { I : Finset (Fin (2 * p + 1)) // I.card = p }) => (I, j I)).det ≠ 0

A block of the single-cluster minor is nonsingular. Let the p-subset sums of o be pairwise distinct and differ by at most D, and let the weights be 2^{2^{e t j}} with labels e injective on positions at distance at most D. For a bijection σ from the p-subsets to the (p + 1)-subsets with I ⊆ σ I and a shift w, the minor with rows (σ I, w + ∑_{σ I} o) and columns (I, w + ∑_I o) has nonzero determinant.

theorem Algebraic.Tensor3.Internal.Diagonal.choose_mul_card_le_rank_of_shifts {p m : ℕ} (o : Fin (2 * p + 1) → ℤ) (g : Fin (2 * p + 1) → Fin m → ℂ) (e : Fin (2 * p + 1) → Fin m → ℕ) (ho : Set.InjOn (fun (I : Finset (Fin (2 * p + 1))) => ∑ t ∈ I, o t) {I : Finset (Fin (2 * p + 1)) | I.card = p}) (hg : ∀ (t : Fin (2 * p + 1)) (j : Fin m), g t j = 2 ^ 2 ^ e t j) (D : ℕ) (hD : ∀ (I I' : Finset (Fin (2 * p + 1))), I.card = p → I'.card = p → ∑ t ∈ I, o t - ∑ t ∈ I', o t ≤ ↑D) (he : ∀ (t t' : Fin (2 * p + 1)) (j j' : Fin m), |↑↑j - ↑↑j'| ≤ ↑D → e t j = e t' j' → t = t' ∧ j = j') {Q : Type u_3} [Fintype Q] [DecidableEq Q] (w : Q → ℤ) (hw : Function.Injective w) (hrange : ∀ (q : Q) (K : Finset (Fin (2 * p + 1))), K.card = p ∨ K.card = p + 1 → 0 ≤ w q + ∑ t ∈ K, o t ∧ w q + ∑ t ∈ K, o t < ↑m) : (2 * p + 1).choose p * Fintype.card Q ≤ (koszulFlattening p (weightedShifts o g)).rank

The single-cluster certificate on a window of shifts. Under the hypotheses of det_submatrix_shift_ne_zero, let w : Q → ℤ be pairwise distinct shifts whose positions w q + ∑_K o lie in [0, m) for all subsets K of size p or p + 1. The blocks of the shifts w q form a block-diagonal minor, so the Koszul flattening has rank at least (2p+1).choose p * card Q.

theorem Algebraic.Tensor3.Internal.Diagonal.le_subsetSumSpread {α : Type u_1} {p : ℕ} [Fintype α] (o : α → ℤ) {I I' : Finset α} (hI : I.card = p) (hI' : I'.card = p) : ∑ t ∈ I, o t - ∑ t ∈ I', o t ≤ ↑(subsetSumSpread p o)

The difference of two p-subset sums is at most subsetSumSpread p o.

theorem Algebraic.Tensor3.Internal.Diagonal.choose_mul_le_rank_of_bounds {p m : ℕ} (o : Fin (2 * p + 1) → ℤ) (g : Fin (2 * p + 1) → Fin m → ℂ) (e : Fin (2 * p + 1) → Fin m → ℕ) (ho : Set.InjOn (fun (I : Finset (Fin (2 * p + 1))) => ∑ t ∈ I, o t) {I : Finset (Fin (2 * p + 1)) | I.card = p}) (hg : ∀ (t : Fin (2 * p + 1)) (j : Fin m), g t j = 2 ^ 2 ^ e t j) (lo : ℤ) (D : ℕ) (hlo : ∀ (K : Finset (Fin (2 * p + 1))), K.card = p ∨ K.card = p + 1 → lo ≤ ∑ t ∈ K, o t ∧ ∑ t ∈ K, o t ≤ lo + ↑D) (he : ∀ (t t' : Fin (2 * p + 1)) (j j' : Fin m), |↑↑j - ↑↑j'| ≤ ↑(subsetSumSpread p o) → e t j = e t' j' → t = t' ∧ j = j') : (2 * p + 1).choose p * (m - D) ≤ (koszulFlattening p (weightedShifts o g)).rank

The single-cluster certificate, with explicit bounds on the subset sums. If every sum ∑_{t ∈ K} o t over a subset K of size p or p + 1 lies in [lo, lo + D], the p-subset sums are pairwise distinct, and the weights are 2^{2^{e t j}} with labels e that are injective on positions at distance at most subsetSumSpread p o, then the Koszul flattening has rank at least (2p+1).choose p * (m - D).

theorem Algebraic.Tensor3.Internal.Diagonal.le_sumSpread {α : Type u_1} {p : ℕ} [Fintype α] (o : α → ℤ) {K K' : Finset α} (hK : K.card = p ∨ K.card = p + 1) (hK' : K'.card = p ∨ K'.card = p + 1) : ∑ t ∈ K, o t - ∑ t ∈ K', o t ≤ ↑(sumSpread p o)

theorem Algebraic.Tensor3.Internal.Diagonal.exists_bounds {p : ℕ} (o : Fin (2 * p + 1) → ℤ) : ∃ (lo : ℤ), ∀ (K : Finset (Fin (2 * p + 1))), K.card = p ∨ K.card = p + 1 → lo ≤ ∑ t ∈ K, o t ∧ ∑ t ∈ K, o t ≤ lo + ↑(sumSpread p o)

The sums over subsets of size p or p + 1 lie in an interval of length sumSpread p o.

theorem Algebraic.Tensor3.Internal.Diagonal.subsetSumSpread_le_sumSpread {α : Type u_1} {p : ℕ} [Fintype α] (o : α → ℤ) : subsetSumSpread p o ≤ sumSpread p o

The spread of the p-subset sums is at most the spread over subsets of size p or p + 1.

theorem Algebraic.Tensor3.Internal.Diagonal.choose_mul_le_rank {p m : ℕ} (o : Fin (2 * p + 1) → ℤ) (g : Fin (2 * p + 1) → Fin m → ℂ) (e : Fin (2 * p + 1) → Fin m → ℕ) (ho : Set.InjOn (fun (I : Finset (Fin (2 * p + 1))) => ∑ t ∈ I, o t) {I : Finset (Fin (2 * p + 1)) | I.card = p}) (hg : ∀ (t : Fin (2 * p + 1)) (j : Fin m), g t j = 2 ^ 2 ^ e t j) (he : ∀ (t t' : Fin (2 * p + 1)) (j j' : Fin m), |↑↑j - ↑↑j'| ≤ ↑(subsetSumSpread p o) → e t j = e t' j' → t = t' ∧ j = j') : (2 * p + 1).choose p * (m - sumSpread p o) ≤ (koszulFlattening p (weightedShifts o g)).rank

The single-cluster certificate.

theorem Algebraic.Tensor3.Internal.Diagonal.sum_sub_median_le {p : ℕ} (o : Fin (2 * p + 1) → ℤ) (ho : Monotone o) (K : Finset (Fin (2 * p + 1))) : ∑ t ∈ K, (o t - o ⟨p, ⋯⟩) ≤ ↑p * (o (Fin.last (2 * p)) - o ⟨p, ⋯⟩)

theorem Algebraic.Tensor3.Internal.Diagonal.sum_median_sub_le {p : ℕ} (o : Fin (2 * p + 1) → ℤ) (ho : Monotone o) (K : Finset (Fin (2 * p + 1))) : ∑ t ∈ K, (o ⟨p, ⋯⟩ - o t) ≤ ↑p * (o ⟨p, ⋯⟩ - o 0)

theorem Algebraic.Tensor3.Internal.Diagonal.sum_sub_sum_le {p : ℕ} (o : Fin (2 * p + 1) → ℤ) (ho : Monotone o) {L : ℤ} (hL : o (Fin.last (2 * p)) - o 0 ≤ L) {K K' : Finset (Fin (2 * p + 1))} (hK : K.card = p ∨ K.card = p + 1) (hK' : K'.card = p ∨ K'.card = p + 1) : ∑ t ∈ K, o t - ∑ t ∈ K', o t ≤ |o ⟨p, ⋯⟩| + ↑p * L

For monotone offsets with median r and diameter at most L, the difference of two sums over subsets of size p or p + 1 is at most |r| + p L.

theorem Algebraic.Tensor3.Internal.Diagonal.sumSpread_le {p : ℕ} (o : Fin (2 * p + 1) → ℤ) (ho : Monotone o) {L : ℤ} (hL : o (Fin.last (2 * p)) - o 0 ≤ L) : ↑(sumSpread p o) ≤ |o ⟨p, ⋯⟩| + ↑p * L

Spread of a cluster. For monotone offsets o with median r = o p and diameter o (2p) - o 0 ≤ L, the spread is at most |r| + p L.

theorem Algebraic.Tensor3.Internal.Diagonal.monotone_clusterOffsets {p k : ℕ} {c : Fin (2 * p + 1) → Fin (2 * k + 1)} (hc : Monotone c) : Monotone (clusterOffsets k c)

theorem Algebraic.Tensor3.Internal.Diagonal.sumSpread_clusterOffsets_le {p k : ℕ} (c : Fin (2 * p + 1) → Fin (2 * k + 1)) (hc : Monotone c) {L : ℤ} (hL : ↑↑(c (Fin.last (2 * p))) - ↑↑(c 0) ≤ L) : ↑(sumSpread p (clusterOffsets k c)) ≤ |↑↑(c ⟨p, ⋯⟩) - ↑k| + ↑p * L

theorem Algebraic.Tensor3.Internal.Diagonal.sum_sub_sum_le_mul {p : ℕ} (o : Fin (2 * p + 1) → ℤ) (ho : Monotone o) {L : ℤ} (hL : o (Fin.last (2 * p)) - o 0 ≤ L) {I I' : Finset (Fin (2 * p + 1))} (hI : I.card = p) (hI' : I'.card = p) : ∑ t ∈ I, o t - ∑ t ∈ I', o t ≤ ↑p * L

For monotone offsets with diameter at most L, two p-subset sums differ by at most p L: one is at most p o (2p), the other at least p o 0.

theorem Algebraic.Tensor3.Internal.Diagonal.subsetSumSpread_le {p : ℕ} (o : Fin (2 * p + 1) → ℤ) (ho : Monotone o) {L : ℤ} (hL : o (Fin.last (2 * p)) - o 0 ≤ L) : ↑(subsetSumSpread p o) ≤ ↑p * L

The p-subset spread of a cluster. For monotone offsets with diameter o (2p) - o 0 ≤ L, the p-subset sums spread over at most p L, whatever the median.

theorem Algebraic.Tensor3.Internal.Diagonal.subsetSumSpread_clusterOffsets_le {p k : ℕ} (c : Fin (2 * p + 1) → Fin (2 * k + 1)) (hc : Monotone c) {L : ℤ} (hL : ↑↑(c (Fin.last (2 * p))) - ↑↑(c 0) ≤ L) : ↑(subsetSumSpread p (clusterOffsets k c)) ≤ ↑p * L

theorem Algebraic.Tensor3.Internal.Diagonal.le_rank_lmTensor_cluster {k p : ℕ} (γ : Fin (2 * k + 1) → Fin (2 * k + 1) → ℂ) (e : Fin (2 * k + 1) → Fin (2 * k + 1) → ℕ) (hγ : ∀ (a j : Fin (2 * k + 1)), γ a j = 2 ^ 2 ^ e a j) (c : Fin (2 * p + 1) → Fin (2 * k + 1)) (ho : Set.InjOn (fun (I : Finset (Fin (2 * p + 1))) => ∑ t ∈ I, clusterOffsets k c t) {I : Finset (Fin (2 * p + 1)) | I.card = p}) (he : ∀ (t t' : Fin (2 * p + 1)) (j j' : Fin (2 * k + 1)), |↑↑j - ↑↑j'| ≤ ↑(subsetSumSpread p (clusterOffsets k c)) → e (c t) j = e (c t') j' → t = t' ∧ j = j') : (2 * p + 1).choose p * (2 * k + 1 - sumSpread p (clusterOffsets k c)) ≤ (koszulFlattening p (map (selectSlices c) 1 1 (lmTensor k γ))).rank

theorem Algebraic.Tensor3.Internal.Diagonal.code_injective {m a a' j j' : ℕ} (hj : j < m) (hj' : j' < m) (h : a * m + j = a' * m + j') : a = a' ∧ j = j'

theorem Algebraic.Tensor3.Internal.Diagonal.cluster_labels_of_window {k p : ℕ} (e : Fin (2 * k + 1) → Fin (2 * k + 1) → ℕ) {L : ℕ} (he : ∀ (a a' j j' : Fin (2 * k + 1)), |↑↑a - ↑↑a'| ≤ ↑L → |↑↑j - ↑↑j'| ≤ ↑p * ↑L → e a j = e a' j' → a = a' ∧ j = j') {c : Fin (2 * p + 1) → Fin (2 * k + 1)} (hc : StrictMono c) (hL : ↑↑(c (Fin.last (2 * p))) - ↑↑(c 0) ≤ ↑L) (t t' : Fin (2 * p + 1)) (j j' : Fin (2 * k + 1)) (hj : |↑↑j - ↑↑j'| ≤ ↑p * ↑L) (h : e (c t) j = e (c t') j') : t = t' ∧ j = j'

Window labels on a cluster. If the labels e separate positions whose slices differ by at most L and whose columns differ by at most p L, they separate the positions of a strictly monotone cluster of diameter at most L whose columns differ by at most p L.

theorem Algebraic.Tensor3.Internal.Diagonal.cluster_labels_of_window_subsetSumSpread {k p : ℕ} (e : Fin (2 * k + 1) → Fin (2 * k + 1) → ℕ) {L : ℕ} (he : ∀ (a a' j j' : Fin (2 * k + 1)), |↑↑a - ↑↑a'| ≤ ↑L → |↑↑j - ↑↑j'| ≤ ↑p * ↑L → e a j = e a' j' → a = a' ∧ j = j') {c : Fin (2 * p + 1) → Fin (2 * k + 1)} (hc : StrictMono c) (hL : ↑↑(c (Fin.last (2 * p))) - ↑↑(c 0) ≤ ↑L) (t t' : Fin (2 * p + 1)) (j j' : Fin (2 * k + 1)) (hj : |↑↑j - ↑↑j'| ≤ ↑(subsetSumSpread p (clusterOffsets k c))) (h : e (c t) j = e (c t') j') : t = t' ∧ j = j'

Window labels satisfy the label condition of the single-cluster certificate for every strictly monotone cluster of diameter at most L, whose p-subset spread is at most p L.

theorem Algebraic.Tensor3.Internal.Diagonal.lmWeight_eq {k : ℕ} (a j : Fin (2 * k + 1)) : lmWeight k a j = 2 ^ 2 ^ (↑a * (2 * k + 1) + ↑j)

theorem Algebraic.Tensor3.Internal.Diagonal.le_rank_weightedLMTensor_cluster {k p : ℕ} (c : Fin (2 * p + 1) → Fin (2 * k + 1)) (hc : Function.Injective c) (ho : Set.InjOn (fun (I : Finset (Fin (2 * p + 1))) => ∑ t ∈ I, clusterOffsets k c t) {I : Finset (Fin (2 * p + 1)) | I.card = p}) : (2 * p + 1).choose p * (2 * k + 1 - sumSpread p (clusterOffsets k c)) ≤ (koszulFlattening p (map (selectSlices c) 1 1 (weightedLMTensor k))).rank

theorem Algebraic.Tensor3.Internal.Diagonal.rank_le_borderRank_mul {k p : ℕ} (c : Fin (2 * p + 1) → Fin (2 * k + 1)) (T : Tensor3 (Fin (2 * k + 1)) (Fin (2 * k + 1)) (Fin (2 * k + 1))) : (koszulFlattening p (map (selectSlices c) 1 1 T)).rank ≤ T.borderRank * (2 * p).choose p

The Koszul bound for a tensor T whose cluster tensor is map (selectSlices c) 1 1 T'.

theorem Algebraic.Tensor3.Internal.Diagonal.rank_le_mul_of_borderRankLE {k p : ℕ} (c : Fin (2 * p + 1) → Fin (2 * k + 1)) {T : Tensor3 (Fin (2 * k + 1)) (Fin (2 * k + 1)) (Fin (2 * k + 1))} {r : ℕ} (h : T.BorderRankLE r) : (koszulFlattening p (map (selectSlices c) 1 1 T)).rank ≤ r * (2 * p).choose p

theorem Algebraic.Tensor3.Internal.Diagonal.choose_mul_le_borderRank_mul_lmTensor {k p : ℕ} (γ : Fin (2 * k + 1) → Fin (2 * k + 1) → ℂ) (e : Fin (2 * k + 1) → Fin (2 * k + 1) → ℕ) (hγ : ∀ (a j : Fin (2 * k + 1)), γ a j = 2 ^ 2 ^ e a j) (c : Fin (2 * p + 1) → Fin (2 * k + 1)) (ho : Set.InjOn (fun (I : Finset (Fin (2 * p + 1))) => ∑ t ∈ I, clusterOffsets k c t) {I : Finset (Fin (2 * p + 1)) | I.card = p}) (he : ∀ (t t' : Fin (2 * p + 1)) (j j' : Fin (2 * k + 1)), |↑↑j - ↑↑j'| ≤ ↑(subsetSumSpread p (clusterOffsets k c)) → e (c t) j = e (c t') j' → t = t' ∧ j = j') (d : Fin (2 * k + 1) → ℂ) (hd : ∀ (t : Fin (2 * p + 1)), d (c t) = 1) : (2 * p + 1).choose p * (2 * k + 1 - sumSpread p (clusterOffsets k c)) ≤ (map (Matrix.diagonal d) 1 1 (lmTensor k γ)).borderRank * (2 * p).choose p

theorem Algebraic.Tensor3.Internal.Diagonal.choose_mul_le_borderRank_mul_weightedLMTensor {k p : ℕ} (c : Fin (2 * p + 1) → Fin (2 * k + 1)) (hc : Function.Injective c) (ho : Set.InjOn (fun (I : Finset (Fin (2 * p + 1))) => ∑ t ∈ I, clusterOffsets k c t) {I : Finset (Fin (2 * p + 1)) | I.card = p}) (d : Fin (2 * k + 1) → ℂ) (hd : ∀ (t : Fin (2 * p + 1)), d (c t) = 1) : (2 * p + 1).choose p * (2 * k + 1 - sumSpread p (clusterOffsets k c)) ≤ (map (Matrix.diagonal d) 1 1 (weightedLMTensor k)).borderRank * (2 * p).choose p

theorem Algebraic.Tensor3.Internal.Diagonal.not_borderRankLE_weightedLMTensor {k p : ℕ} (c : Fin (2 * p + 1) → Fin (2 * k + 1)) (hc : Function.Injective c) (ho : Set.InjOn (fun (I : Finset (Fin (2 * p + 1))) => ∑ t ∈ I, clusterOffsets k c t) {I : Finset (Fin (2 * p + 1)) | I.card = p}) (d : Fin (2 * k + 1) → ℂ) (hd : ∀ (t : Fin (2 * p + 1)), d (c t) = 1) {r : ℕ} (hr : r * (2 * p).choose p < (2 * p + 1).choose p * (2 * k + 1 - sumSpread p (clusterOffsets k c))) : ¬(map (Matrix.diagonal d) 1 1 (weightedLMTensor k)).BorderRankLE r