Finite coefficient tensors and their algebraic transformations.

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.batchCount (R k : ℕ) : ℕ

Number of batches of size k needed to cover rank R, with natural-number division.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.batchCount R k = (R + k - 1) / k

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.batchCount_zero (k : ℕ) : batchCount 0 k = 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.le_batchCount_mul (R : ℕ) {k : ℕ} (hk : 0 < k) : R ≤ batchCount R k * k

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.batchCount_le_iff {R k B : ℕ} (hk : 0 < k) : batchCount R k ≤ B ↔ R ≤ B * k

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.batchCount_mul_lt (R : ℕ) {k : ℕ} (hk : 0 < k) : batchCount R k * k < R + k

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.batchCount_pos_iff {R k : ℕ} (hk : 0 < k) : 0 < batchCount R k ↔ 0 < R

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.batchCount_cast_lt (R : ℕ) {k : ℕ} (hk : 0 < k) : ↑(batchCount R k) < ↑R / ↑k + 1

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.batchCount_cast_le (R : ℕ) {k : ℕ} (hk : 0 < k) : ↑(batchCount R k) ≤ ↑R / ↑k + 1

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.batchCount_mul_cast_le (R r : ℕ) {k : ℕ} (hk : 0 < k) : ↑(batchCount R k * r) ≤ ↑r / ↑k * ↑R + ↑r

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.batchRank (k r : ℕ) : ℕ → ℕ

Rank bound obtained by repeatedly applying the finite batching recurrence.

Equations

• One or more equations did not get rendered due to their size.
• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.batchRank k r 0 = 1

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.batchRank_zero (k r : ℕ) : batchRank k r 0 = 1

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.batchRank_succ (k r t : ℕ) : batchRank k r (t + 1) = batchCount (batchRank k r t) k * r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.batchRank_succ_le_affine {k : ℕ} (hk : 0 < k) (r t : ℕ) : ↑(batchRank k r (t + 1)) ≤ ↑r / ↑k * ↑(batchRank k r t) + ↑r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.batchRank_pos {k r : ℕ} (hk : 0 < k) (hr : 0 < r) (t : ℕ) : 0 < batchRank k r t

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.repeat_batch_ceiling {K : Type u_1} {U : Type u_5} {V : Type u_6} {W : Type u_7} [CommSemiring K] {S : Tensor K U V W} {k r R : ℕ} (hbatch : (directSum fun (x : Fin k) => S).RankAtMost r) (hk : 0 < k) : (directSum fun (x : Fin R) => S).RankAtMost (batchCount R k * r)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.batch_product_ceiling {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {U : Type u_5} {V : Type u_6} {W : Type u_7} [CommSemiring K] [Finite U] [Finite V] [Finite W] {T : Tensor K X Y Z} {S : Tensor K U V W} {R k r : ℕ} (hT : T.RankAtMost R) (hbatch : (directSum fun (x : Fin k) => S).RankAtMost r) (hk : 0 < k) : (T.product S).RankAtMost (batchCount R k * r)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_batch_rank_ceiling {K : Type u_1} {A : Type u_8} {B : Type u_9} [CommSemiring K] [DecidableEq A] [DecidableEq B] [Finite B] {R k r : ℕ} (houter : (matrixCoefficients A A A).RankAtMost R) (hbatch : (directSum fun (x : Fin k) => matrixCoefficients B B B).RankAtMost r) (hk : 0 < k) : (matrixCoefficients (A × B) (A × B) (A × B)).RankAtMost (batchCount R k * r)