Proofs for Vandermonde and Fourier transform matrices

Let M = (x c ^ r) be the transposed Vandermonde matrix of distinct nodes x c, with rows r and columns c in 0, …, N - 1; the Fourier matrix dft ω N is the case x c = ω ^ c for a primitive N-th root of unity ω.

• Prefix rows are independent (card_filter_lt_le_blockRank): on a set C of columns, the rows r < |C| are linearly independent, since a combination ∑ g r x ^ r of them vanishing at the |C| distinct nodes x c is a polynomial of degree below |C| with |C| roots. So every block M[Y, C] has rank at least the number of rows r ∈ Y with r < |C|.
• Half cuts (le_blockRank_add_blockRank): for a set X of h ≤ N/2 columns and any set Y of rows, rank M[Yᶜ, X] + rank M[Y, Xᶜ] ≥ h. The first block has rank at least the number of rows r < h outside Y, and the second, as |Xᶜ| = N - h ≥ h, at least the number of rows r < h in Y.
• The layout bound (half_le_of_rank_cuts): if some row of M has no zero entry and every split with h inputs on one side satisfies the half-cut bound, a fan-in-two program carrying M and obeying the rank-cut inequality has h ≤ (A + η) (s - N)⁺ + 3 log₂ (N + 3 s) + C. The component of the output wire of the nonzero row is closed, so the rank-cut inequality puts every input into it. Along the ranking of MultiOutput.exists_rank, the number of inputs in a prefix grows by at most one per wire, so the prefix ending at some input holds exactly h inputs; it is crossed by at least h signals and charged to the component holding all inputs.

Vandermonde matrices

theorem Algebraic.Cutwidth.MultiOutput.Internal.card_filter_lt_le_blockRank {F : Type u_1} [Field F] {N : ℕ} {x : Fin N → F} (hx : Function.Injective x) (Y C : Finset (Fin N)) : {r ∈ Y | ↑r < C.card}.card ≤ blockRank (Matrix.vandermonde x).transpose Y C

Prefix rows of a Vandermonde matrix are independent. For distinct nodes x c, every block of (x c ^ r) with rows Y and columns C has rank at least the number of rows r ∈ Y with r < |C|.

theorem Algebraic.Cutwidth.MultiOutput.Internal.card_filter_val_lt_eq {N h : ℕ} (hh : h ≤ N) : {r : Fin N | ↑r < h}.card = h

The first h ≤ N indices number h.

theorem Algebraic.Cutwidth.MultiOutput.Internal.le_blockRank_add_blockRank {F : Type u_1} [Field F] {N : ℕ} {x : Fin N → F} (hx : Function.Injective x) {h : ℕ} (hh : 2 * h ≤ N) (Y X : Finset (Fin N)) (hX : X.card = h) : h ≤ blockRank (Matrix.vandermonde x).transpose Yᶜ X + blockRank (Matrix.vandermonde x).transpose Y Xᶜ

Half cuts of a Vandermonde matrix. For distinct nodes, a set X of h columns with 2 h ≤ N, and any set Y of rows, h ≤ rank M[Yᶜ, X] + rank M[Y, Xᶜ].

theorem Algebraic.Cutwidth.MultiOutput.Internal.one_le_blockRank_of_ne_zero {F : Type u_1} [Field F] {m n : ℕ} {M : Matrix (Fin m) (Fin n) F} {Y : Finset (Fin m)} {X : Finset (Fin n)} {i : Fin m} {j : Fin n} (hi : i ∈ Y) (hj : j ∈ X) (hij : M i j ≠ 0) : 1 ≤ blockRank M Y X

A block with a nonzero entry has rank at least one.

The Fourier matrix

theorem Algebraic.Cutwidth.MultiOutput.Internal.dft_eq_transpose_vandermonde {F : Type u_1} [Field F] (ω : F) (N : ℕ) : dft ω N = (Matrix.vandermonde fun (c : Fin N) => ω ^ ↑c).transpose

The Fourier matrix is the transposed Vandermonde matrix of the powers of ω.

theorem Algebraic.Cutwidth.MultiOutput.Internal.injective_pow_of_isPrimitiveRoot {F : Type u_1} [Field F] {N : ℕ} {ω : F} (hω : IsPrimitiveRoot ω N) : Function.Injective fun (c : Fin N) => ω ^ ↑c

The powers ω ^ c, c < N, of a primitive N-th root of unity are distinct.

theorem Algebraic.Cutwidth.MultiOutput.Internal.le_blockRank_add_blockRank_dft {F : Type u_1} [Field F] {N : ℕ} {ω : F} (hω : IsPrimitiveRoot ω N) (Y X : Finset (Fin N)) (hX : X.card = N / 2) : N / 2 ≤ blockRank (dft ω N) Yᶜ X + blockRank (dft ω N) Y Xᶜ

Half cuts of the Fourier matrix. For a primitive N-th root of unity ω, a set X of ⌊N/2⌋ columns, and any set Y of rows, ⌊N/2⌋ ≤ rank F[Yᶜ, X] + rank F[Y, Xᶜ].

theorem Algebraic.Cutwidth.MultiOutput.Internal.dft_zero_ne_zero {F : Type u_1} [Field F] {N : ℕ} (ω : F) (hN : 0 < N) (j : Fin N) : dft ω N ⟨0, hN⟩ j ≠ 0

The first row of the Fourier matrix has no zero entry.

The layout bound

theorem Algebraic.Cutwidth.MultiOutput.Internal.half_le_of_rank_cuts {σ : Signature} {F : Type u_1} [Field F] {A η C : ℝ} (hAη : 0 ≤ A + η) (order : Multigraph.OrderingBound A η C) {N s m : ℕ} (p : Program σ N s) (hp : p.FanInAtMost 2) (out : Fin m → Wire N s) {M : Matrix (Fin m) (Fin N) F} {h : ℕ} (hrow : 0 < h → ∃ (i₀ : Fin m), ∀ (j : Fin N), M i₀ j ≠ 0) (hrank : ∀ (Y : Finset (Fin m)) (X : Finset (Fin N)), X.card = h → h ≤ blockRank M Yᶜ X + blockRank M Y Xᶜ) (hh : h ≤ N) (cuts : ∀ (S : Finset (Wire N s)), blockRank M (outputsIn out S)ᶜ (SingleCut.inputsIn S) + blockRank M (outputsIn out S) (SingleCut.inputsIn S)ᶜ ≤ (SingleCut.forward p S).card + (SingleCut.backward p S).card) : ↑h ≤ (A + η) * max (↑s - ↑N) 0 + 3 * Real.logb 2 (↑N + 3 * ↑s) + C

The layout bound for half cuts. Let a fan-in-two program carry a matrix M, in the sense that every split S satisfies the rank-cut inequality. If some row of M has no zero entry, and every set X of h ≤ N columns satisfies h ≤ rank M[Yᶜ, X] + rank M[Y, Xᶜ] for every set Y of rows, then h ≤ (A + η) (s - N)⁺ + 3 log₂ (N + 3 s) + C.

theorem Algebraic.Cutwidth.MultiOutput.Internal.half_le_of_dft {σ : Signature} {F : Type u_1} [Field F] {A η C : ℝ} (hAη : 0 ≤ A + η) (order : Multigraph.OrderingBound A η C) {N s : ℕ} (p : Program σ N s) (hp : p.FanInAtMost 2) (out : Fin N → Wire N s) {ω : F} (hω : IsPrimitiveRoot ω N) (cuts : ∀ (S : Finset (Wire N s)), blockRank (dft ω N) (outputsIn out S)ᶜ (SingleCut.inputsIn S) + blockRank (dft ω N) (outputsIn out S) (SingleCut.inputsIn S)ᶜ ≤ (SingleCut.forward p S).card + (SingleCut.backward p S).card) : ↑(N / 2) ≤ (A + η) * max (↑s - ↑N) 0 + 3 * Real.logb 2 (↑N + 3 * ↑s) + C

The layout bound for the Fourier matrix. A fan-in-two program carrying dft ω N, for a primitive N-th root of unity ω, and obeying the rank-cut inequality has ⌊N/2⌋ ≤ (A + η) (s - N)⁺ + 3 log₂ (N + 3 s) + C.

Asymptotics

theorem Algebraic.Cutwidth.MultiOutput.Internal.exists_eventually_lt_of_half_le {A : ℝ} (hA : 0 < A) (order : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), Multigraph.OrderingBound A η C) {ε : ℝ} (hε : 0 < ε) : ∃ (η : ℝ) (C : ℝ), 0 ≤ A + η ∧ Multigraph.OrderingBound A η C ∧ ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (s : ℕ), ↑(N / 2) ≤ (A + η) * max (↑s - ↑N) 0 + 3 * Real.logb 2 (↑N + 3 * ↑s) + C → (1 + 1 / (2 * A) - ε) * ↑N < ↑s

The numeric transfer for half cuts. For A > 0 and ε > 0 there are a slack η and a constant C with OrderingBound A η C such that, for all large N, every s with ⌊N/2⌋ ≤ (A + η) (s - N)⁺ + 3 log₂ (N + 3 s) + C exceeds (1 + 1/(2A) - ε) N.

theorem Algebraic.Cutwidth.MultiOutput.Internal.eventually_lt_size_of_dft_rank_cuts {A : ℝ} (hA : 0 < A) (order : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), Multigraph.OrderingBound A η C) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] (ω : F), IsPrimitiveRoot ω N → ∀ (σ : Signature) (c : Circuit σ N N), c.FanInAtMost 2 → (∀ (S : Finset (Wire N c.size)), blockRank (dft ω N) (outputsIn c.outputs S)ᶜ (SingleCut.inputsIn S) + blockRank (dft ω N) (outputsIn c.outputs S) (SingleCut.inputsIn S)ᶜ ≤ (SingleCut.forward c.program S).card + (SingleCut.backward c.program S).card) → (1 + 1 / (2 * A) - ε) * ↑N < ↑c.size

The asymptotic bound for the Fourier matrix under the rank-cut inequality, uniformly over fields, signatures and roots of unity.