The periodic Landsberg–Michałek tensors: proof internals

Proofs behind Complexitylib.Algebraic.LinearAlgebra.Tensor.Periodic.

• Entries. The coefficient periodicWeight k A M a j is 2^{2^e} with e = (a mod A) M + (j mod M) < A M when A, M > 0, so every entry of periodicLMTensor k A M is 0 or 2^{2^e} with e < A M.
• Window labels. Equal codes (a mod A) M + (j mod M) give a ≡ a' (mod A) and j ≡ j' (mod M). If |a - a'| ≤ L < A and |j - j'| ≤ p L < M, then a = a' and j = j'.
• The paired-cluster Koszul bound. The certificate for T_k(γ) with window labels (Tensor3.div_mul_phi_sub_le_borderRank_restrictSlices_lmTensor) gives PairedKoszulBoundOn (periodicLMTensor k A M) p L (8 (p + 1) L) for L < A, p L < M.
• The bounds. The assembly of Complexitylib.Algebraic.LinearAlgebra.Tensor.Explicit applies to every tight tensor with nonzero slices satisfying PairedKoszulBoundOn. For the asymptotic forms fix p, then L ≥ max (3^{2p} + 1) (2 (3^{2p} + 1) / δ), then A = L + 1 and M = p L + 1.

Entries

theorem Algebraic.Tensor3.Internal.Periodic.periodicWeight_eq (k A M : ℕ) (a j : Fin (2 * k + 1)) : periodicWeight k A M a j = 2 ^ 2 ^ (↑a % A * M + ↑j % M)

theorem Algebraic.Tensor3.Internal.Periodic.periodicWeight_ne_zero (k A M : ℕ) (a j : Fin (2 * k + 1)) : periodicWeight k A M a j ≠ 0

theorem Algebraic.Tensor3.Internal.Periodic.code_lt {A M : ℕ} (hA : 0 < A) (hM : 0 < M) (a j : ℕ) : a % A * M + j % M < A * M

theorem Algebraic.Tensor3.Internal.Periodic.periodicLMTensor_apply (k A M : ℕ) (a j l : Fin (2 * k + 1)) : periodicLMTensor k A M a j l = if ↑↑l = ↑↑j + (↑↑a - ↑k) then periodicWeight k A M a j else 0

theorem Algebraic.Tensor3.Internal.Periodic.periodicLMTensor_apply_mem {k A M : ℕ} (hA : 0 < A) (hM : 0 < M) (a j l : Fin (2 * k + 1)) : periodicLMTensor k A M a j l ∈ insert 0 (Finset.image (fun (e : ℕ) => ↑(2 ^ 2 ^ e)) (Finset.range (A * M)))

Window labels

theorem Algebraic.Tensor3.Internal.Periodic.periodic_label_window {k p A M L : ℕ} (hA : L < A) (hM : p * L < M) (a a' j j' : Fin (2 * k + 1)) (ha : |↑↑a - ↑↑a'| ≤ ↑L) (hj : |↑↑j - ↑↑j'| ≤ ↑p * ↑L) (h : ↑a % A * M + ↑j % M = ↑a' % A * M + ↑j' % M) : a = a' ∧ j = j'

The periodic codes (a mod A) M + (j mod M) separate positions whose slices differ by at most L < A and whose columns differ by at most p L < M.

The paired-cluster Koszul bound

theorem Algebraic.Tensor3.Internal.Periodic.pairedKoszulBoundOn_periodicLMTensor {k p A M L : ℕ} (hA : L < A) (hM : p * L < M) : (periodicLMTensor k A M).PairedKoszulBoundOn p L (8 * (↑p + 1) * ↑L)

The bounds

theorem Algebraic.Tensor3.Internal.Periodic.tight_periodicLMTensor (k A M : ℕ) : (periodicLMTensor k A M).Tight

theorem Algebraic.Tensor3.Internal.Periodic.periodicLMTensor_ne_zero (k A M : ℕ) (a : Fin (2 * k + 1)) : periodicLMTensor k A M a ≠ 0

theorem Algebraic.Tensor3.Internal.Periodic.le_borderRank {k p A M L : ℕ} (hp : 1 ≤ p) (hL : 3 ^ (2 * p) + 1 ≤ L) (hLk : L ≤ k) (hA : L < A) (hM : p * L < M) : (7 / 3 - 2 / (3 * (↑p + 1))) * (2 * ↑k + 1) - (16 * (↑p + 1) * ↑L + (3 ^ (2 * p) + 1) * (2 * ↑k + 1) / ↑L + 2) ≤ ↑(periodicLMTensor k A M).borderRank

theorem Algebraic.Tensor3.Internal.Periodic.eventually_le_borderRank {p A M : ℕ} (hp : 1 ≤ p) {δ : ℝ} (hδ : 0 < δ) {L : ℕ} (hL : 3 ^ (2 * p) + 1 ≤ L) (hLδ : 2 * (3 ^ (2 * p) + 1) / δ ≤ ↑L) (hA : L < A) (hM : p * L < M) : ∀ᶠ (k : ℕ) in Filter.atTop, (7 / 3 - 2 / (3 * (↑p + 1)) - δ) * (2 * ↑k + 1) ≤ ↑(periodicLMTensor k A M).borderRank

theorem Algebraic.Tensor3.Internal.Periodic.exists_eventually_le_borderRank {p : ℕ} (hp : 1 ≤ p) {δ : ℝ} (hδ : 0 < δ) : ∃ (A : ℕ) (M : ℕ), ∀ᶠ (k : ℕ) in Filter.atTop, (7 / 3 - 2 / (3 * (↑p + 1)) - δ) * (2 * ↑k + 1) ≤ ↑(periodicLMTensor k A M).borderRank

theorem Algebraic.Tensor3.Internal.Periodic.eventually_twentyOne_div_ten : ∀ᶠ (k : ℕ) in Filter.atTop, 21 / 10 * (2 * ↑k + 1) ≤ ↑(periodicLMTensor k 14761 29521).borderRank

theorem Algebraic.Tensor3.Internal.Periodic.exists_eventually_seven_div_three {ε : ℝ} (hε : 0 < ε) : ∃ (A : ℕ) (M : ℕ), ∀ᶠ (k : ℕ) in Filter.atTop, (7 / 3 - ε) * (2 * ↑k + 1) ≤ ↑(periodicLMTensor k A M).borderRank