The deletion game: definitions

Definitions for the deletion game of Complexitylib.Algebraic.LinearAlgebra.Tensor.DeletionGame, the global step of a border-rank lower bound for tensors with m = 2k + 1 slices Fin (2 * k + 1), by border substitution (Complexitylib.Algebraic.LinearAlgebra.Tensor.Substitution).

• DeletionGame.offset k a = a - k ∈ [-k, k] is the offset of the slice a.
• DeletionGame.sideBlock f L i is the set of slices a with i L + 1 ≤ f a ≤ (i + 1) L. The positive blocks DeletionGame.posBlock k L i (offsets in [i L + 1, (i + 1) L]) and the negative blocks DeletionGame.negBlock k L i (offsets in [-(i + 1) L, -(i L + 1)]) split the offsets 1, …, k and -1, …, -k into consecutive runs of length L, the last one possibly shorter. A block B is good for a set S of surviving slices if R ≤ card (S ∩ B).
• DeletionGame.phi n r s = max (max (n - r) (n - s)) (max (r + s) (2 * min (r + s) (n - r - s))) is the width function Φ_n(r, s) of a positive cluster at offset r paired with a negative cluster at offset -s.
• DeletionGame.PairedClusterBound k L R D E LB is the paired-cluster hypothesis on a function LB on sets of slices: whenever a positive block B⁺ and a negative block B⁻ are both good for S, some offsets r in B⁺ and -s in B⁻ satisfy D * (Φ_{2k+1}(r, s) - E) ≤ LB S. For the Koszul certificate of paired clusters of 2p + 1 slices, D = (2p + 1) / (p + 1) and E = O(p L).

def Algebraic.Tensor3.DeletionGame.offset (k : ℕ) (a : Fin (2 * k + 1)) : ℤ

The offset a - k ∈ [-k, k] of the slice a among the 2k + 1 slices Fin (2 * k + 1).

Equations

• Algebraic.Tensor3.DeletionGame.offset k a = ↑↑a - ↑k

def Algebraic.Tensor3.DeletionGame.sideBlock {α : Type u_1} [Fintype α] (f : α → ℤ) (L i : ℕ) : Finset α

The block of index i and length L on the side described by f: the elements a with i L + 1 ≤ f a ≤ (i + 1) L.

Equations

• Algebraic.Tensor3.DeletionGame.sideBlock f L i = {a : α | ↑i * ↑L + 1 ≤ f a ∧ f a ≤ (↑i + 1) * ↑L}

def Algebraic.Tensor3.DeletionGame.posBlock (k L i : ℕ) : Finset (Fin (2 * k + 1))

The positive block of index i: the slices with offset in [i L + 1, (i + 1) L].

Equations

• Algebraic.Tensor3.DeletionGame.posBlock k L i = Algebraic.Tensor3.DeletionGame.sideBlock (Algebraic.Tensor3.DeletionGame.offset k) L i

def Algebraic.Tensor3.DeletionGame.negBlock (k L i : ℕ) : Finset (Fin (2 * k + 1))

The negative block of index i: the slices with offset in [-(i + 1) L, -(i L + 1)].

Equations

• Algebraic.Tensor3.DeletionGame.negBlock k L i = Algebraic.Tensor3.DeletionGame.sideBlock (fun (a : Fin (2 * k + 1)) => -Algebraic.Tensor3.DeletionGame.offset k a) L i

def Algebraic.Tensor3.DeletionGame.phi (n r s : ℤ) : ℤ

The width function Φ_n(r, s) = max {n - r, n - s, r + s, 2 min (r + s, n - r - s)} of a positive cluster at offset r paired with a negative cluster at offset -s, in an n × n square.

Equations

• Algebraic.Tensor3.DeletionGame.phi n r s = max (max (n - r) (n - s)) (max (r + s) (2 * min (r + s) (n - r - s)))

def Algebraic.Tensor3.DeletionGame.PairedClusterBound (k L R : ℕ) (D E : ℝ) (LB : Finset (Fin (2 * k + 1)) → ℕ) : Prop

The paired-cluster hypothesis. For every set S of slices and every positive block posBlock k L i and negative block negBlock k L j that are both good for S (at least R of their slices lie in S), some slice a of the positive block and some slice b of the negative block satisfy D * (Φ_{2k+1}(offset a, -offset b) - E) ≤ LB S.

Equations

• One or more equations did not get rendered due to their size.