Finite type counts, hierarchy separation and tensor execution bounds.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.grid_modular_collision (Q c t u v : ℤ) (hc : 0 ≤ c ∧ c < Q) (ht : 0 ≤ t ∧ t < Q) (hu : 0 ≤ u ∧ u < Q) (hv : 0 ≤ v ∧ v < Q) (hmod : c ≡ t + u - v [ZMOD 4 * Q]) : c = t + u - v

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.squaredNorm {ι : Type u_1} [Fintype ι] (t : ι → ℝ) : ℝ

Squared Euclidean norm of a finitely indexed real vector.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.squaredNorm t = ∑ i : ι, t i ^ 2

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.dot {ι : Type u_1} [Fintype ι] (t u : ι → ℝ) : ℝ

Euclidean dot product of two finitely indexed real vectors.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.dot t u = ∑ i : ι, t i * u i

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.squaredNorm_displacement {ι : Type u_1} [Fintype ι] (t u v : ι → ℝ) : (squaredNorm fun (i : ι) => t i + u i - v i) = squaredNorm t + 2 * (dot t u - dot t v) + squaredNorm fun (i : ι) => u i - v i

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.sphere_slice_collision {ι : Type u_1} [Fintype ι] (t c u v : ι → ℝ) (hsphere : squaredNorm c = squaredNorm t) (hslice : dot t u = dot t v) (hcollision : ∀ (i : ι), c i = t i + u i - v i) : u = v ∧ c = t