Finite coefficient tensors and their algebraic transformations.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_rank_of_injective {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [DecidableEq A] [DecidableEq B] {R : ℕ} (h : (matrixCoefficients A A A).RankAtMost R) (f : B → A) (hf : Function.Injective f) : (matrixCoefficients B B B).RankAtMost R

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_directSum_rank_of_injective {K : Type u_1} {ι : Type u_2} {κ : Type u_3} {A : Type u_4} {B : Type u_5} [CommSemiring K] [DecidableEq ι] [DecidableEq κ] [DecidableEq A] [DecidableEq B] {R : ℕ} (h : (directSum fun (x : ι) => matrixCoefficients A A A).RankAtMost R) (f : κ → ι) (hf : Function.Injective f) (g : B → A) (hg : Function.Injective g) : (directSum fun (x : κ) => matrixCoefficients B B B).RankAtMost R

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_directSum_power_rank {K : Type u_1} [CommSemiring K] {n k R t : ℕ} (h : ((directSum fun (x : Fin k) => matrixCoefficients (Fin n) (Fin n) (Fin n)).power t).RankAtMost R) : (directSum fun (x : Fin (k ^ t)) => matrixCoefficients (Fin (n ^ t)) (Fin (n ^ t)) (Fin (n ^ t))).RankAtMost R

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.square_directSum_power_rank {n k r d D : ℕ} (A : (directSum fun (x : Fin k) => matrixMultiplication n n n).PolynomialApproximation r d D) (t : ℕ) : (directSum fun (x : Fin (k ^ t)) => matrixMultiplication (n ^ t) (n ^ t) (n ^ t)).RankAtMost ((D * t + 1) * r ^ t)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_fin_one_rank {K : Type u_1} [CommSemiring K] : (matrixCoefficients (Fin 1) (Fin 1) (Fin 1)).RankAtMost 1

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_pow_batchRank {K : Type u_1} [CommSemiring K] {n k r : ℕ} (hk : 0 < k) (hbatch : (directSum fun (x : Fin k) => matrixCoefficients (Fin n) (Fin n) (Fin n)).RankAtMost r) (t : ℕ) : (matrixCoefficients (Fin (n ^ t)) (Fin (n ^ t)) (Fin (n ^ t))).RankAtMost (batchRank k r t)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.rpow_omega_le_of_rankAtMost {n R : ℕ} {B : ℝ} (hn : 2 ≤ n) (hRank : (Tensor.matrixMultiplication n n n).RankAtMost R) (hquad : ↑n ^ 2 ≤ B) (hR : ↑R ≤ B) : ↑n ^ omega ≤ B

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.rpow_omega_le_of_rank_growth {n : ℕ} {q C : ℝ} (hn : 2 ≤ n) (hquad : ↑n ^ 2 ≤ q) (R : ℕ → ℕ) (hRank : ∀ (t : ℕ), (Tensor.matrixMultiplication (n ^ t) (n ^ t) (n ^ t)).RankAtMost (R t)) (hcost : ∀ (t : ℕ), ↑(R t) ≤ C * q ^ t) : ↑n ^ omega ≤ q

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.equalSummand_inequality_of_quadratic_bound {n k r : ℕ} (hn : 2 ≤ n) (hk : 0 < k) (hbatch : (Tensor.directSum fun (x : Fin k) => Tensor.matrixMultiplication n n n).RankAtMost r) (hquad : ↑n ^ 2 ≤ ↑r / ↑k) : ↑k * ↑n ^ omega ≤ ↑r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.equalSummand_inequality {n k r : ℕ} (hn : 1 ≤ n) (hbatch : (Tensor.directSum fun (x : Fin k) => Tensor.matrixMultiplication n n n).RankAtMost r) : ↑k * ↑n ^ omega ≤ ↑r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.equalSummand_inequality_of_polynomialApproximation {n k r d D : ℕ} (hn : 1 ≤ n) (A : (Tensor.directSum fun (x : Fin k) => Tensor.matrixMultiplication n n n).PolynomialApproximation r d D) : ↑k * ↑n ^ omega ≤ ↑r