Finite type counts, hierarchy separation and tensor execution bounds.

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.Grid (d Q : ℕ) : Type

A d-dimensional integer grid with Q positions per coordinate.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.Grid d Q = (Fin d → Fin Q)

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.gridSquaredNorm {d Q : ℕ} (x : Grid d Q) : ℕ

Squared Euclidean norm of a grid point, computed in natural numbers.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.gridSquaredNorm x = ∑ i : Fin d, ↑(x i) ^ 2

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.gridDot {d Q : ℕ} (t u : Grid d Q) : ℕ

Dot product of two grid points, computed in natural numbers.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.gridDot t u = ∑ i : Fin d, ↑(t i) * ↑(u i)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.gridSquaredNorm_le {d Q : ℕ} (x : Grid d Q) : gridSquaredNorm x ≤ d * Q ^ 2

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.gridDot_le {d Q : ℕ} (t u : Grid d Q) : gridDot t u ≤ d * Q ^ 2

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.normColor {d Q : ℕ} (x : Grid d Q) : Fin (d * Q ^ 2 + 1)

Color a grid point by its bounded squared norm for the pigeonhole argument.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.normColor x = ⟨MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.gridSquaredNorm x, ⋯⟩

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.dotColor {d Q : ℕ} (t u : Grid d Q) : Fin (d * Q ^ 2 + 1)

Color a pair of grid points by their bounded dot product.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.dotColor t u = ⟨MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.gridDot t u, ⋯⟩

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.two_stage_pigeonhole {A : Type u_1} [Fintype A] {M K m : ℕ} (hM : 0 < M) (f : A → Fin M) (g : A → A → Fin M) (hK : M * K ≤ Fintype.card A) (hm : M * m ≤ Fintype.card A) : ∃ (tags : Finset A), tags.card = K ∧ (∃ (radius : Fin M), ∀ t ∈ tags, f t = radius) ∧ ∀ t ∈ tags, ∃ (slice : Finset A), slice.card = m ∧ ∃ (level : Fin M), ∀ u ∈ slice, g t u = level

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.grid_tags_slices {d Q K m : ℕ} (hK : (d * Q ^ 2 + 1) * K ≤ Q ^ d) (hm : (d * Q ^ 2 + 1) * m ≤ Q ^ d) : ∃ (tags : Finset (Grid d Q)), tags.card = K ∧ (∃ (radius : Fin (d * Q ^ 2 + 1)), ∀ t ∈ tags, normColor t = radius) ∧ ∀ t ∈ tags, ∃ (slice : Finset (Grid d Q)), slice.card = m ∧ ∃ (level : Fin (d * Q ^ 2 + 1)), ∀ u ∈ slice, dotColor t u = level