Rectangular matrix multiplication algorithms and their asymptotic exponents.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_of_rankAtMost {F : Type u_1} [Field F] {a b R : ℕ} (ha : 2 ≤ a) {k τ : ℝ} (hk : 0 ≤ k) (hab : ↑a ^ k ≤ ↑b) (hRank : (Foundation.Tensor.matrixCoefficients (Fin a) (Fin b) (Fin a)).RankAtMost R) (hτ : 0 ≤ τ) (hR : ↑R ≤ ↑a ^ τ) (hin : ↑(a * b) ≤ ↑a ^ τ) (hout : ↑a ^ 2 ≤ ↑a ^ τ) : RectangularAdmissibleExponent F k τ

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.rectangular_rpow_omega_le_of_rankAtMost {F : Type u_1} [Field F] {a b R : ℕ} {B k : ℝ} (ha : 2 ≤ a) (hk : 0 ≤ k) (hab : ↑a ^ k ≤ ↑b) (hRank : (Foundation.Tensor.matrixCoefficients (Fin a) (Fin b) (Fin a)).RankAtMost R) (hout : ↑a ^ 2 ≤ B) (hin : ↑(a * b) ≤ B) (hR : ↑R ≤ B) : ↑a ^ rectangularOmega F k ≤ B

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.rectangular_rpow_omega_le_of_rank_growth {F : Type u_1} [Field F] {a b : ℕ} {q C k : ℝ} (ha : 2 ≤ a) (hk : 0 ≤ k) (hab : ↑a ^ k ≤ ↑b) (hout : ↑a ^ 2 ≤ q) (hin : ↑(a * b) ≤ q) (R : ℕ → ℕ) (hRank : ∀ (t : ℕ), (Foundation.Tensor.matrixCoefficients (Fin (a ^ t)) (Fin (b ^ t)) (Fin (a ^ t))).RankAtMost (R t)) (hcost : ∀ (t : ℕ), ↑(R t) ≤ C * q ^ t) : ↑a ^ rectangularOmega F k ≤ q

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.equalRectangular_inequality {F : Type u_1} [Field F] {a b L r : ℕ} {k : ℝ} (ha : 2 ≤ a) (hk : 0 ≤ k) (hab : ↑a ^ k ≤ ↑b) (hbatch : (Foundation.Tensor.directSum fun (x : Fin L) => Foundation.Tensor.matrixCoefficients (Fin a) (Fin b) (Fin a)).RankAtMost r) : ↑L * ↑a ^ rectangularOmega F k ≤ ↑r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.power_le_of_forall_pow_le_square_linear_mul_pow (d : ℕ) {x r : ℝ} (hr : 0 ≤ r) (h : ∀ (n : ℕ), 0 < n → x ^ n ≤ ↑(d * n + 1) ^ 2 * r ^ n) : x ≤ r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.equalRectangular_inequality_of_polynomialApproximation {F : Type u_1} [Field F] {a b L r d D : ℕ} {k : ℝ} (ha : 2 ≤ a) (hk : 0 ≤ k) (hab : ↑a ^ k ≤ ↑b) (P : (Foundation.Tensor.directSum fun (x : Fin L) => Foundation.Tensor.matrixCoefficients (Fin a) (Fin b) (Fin a)).PolynomialApproximation r d D) : ↑L * ↑a ^ rectangularOmega F k ≤ ↑r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.equalRectangular_log_inequality_of_polynomialApproximation {F : Type u_1} [Field F] {a b L r d D : ℕ} {k : ℝ} (ha : 2 ≤ a) (hL : 0 < L) (hk : 0 ≤ k) (hab : ↑a ^ k ≤ ↑b) (P : (Foundation.Tensor.directSum fun (x : Fin L) => Foundation.Tensor.matrixCoefficients (Fin a) (Fin b) (Fin a)).PolynomialApproximation r d D) : rectangularOmega F k * Real.log ↑a ≤ Real.log ↑r - Real.log ↑L

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.equalSquare_inequality_of_polynomialApproximation {F : Type u_1} [Field F] {n L r d D : ℕ} (hn : 1 ≤ n) (P : (Foundation.Tensor.directSum fun (x : Fin L) => Foundation.Tensor.matrixCoefficients (Fin n) (Fin n) (Fin n)).PolynomialApproximation r d D) : ↑L * ↑n ^ omega F ≤ ↑r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.equalVolume_inequality_of_polynomialApproximation {F : Type u_1} [Field F] {a b c L r d D : ℕ} (ha : 1 ≤ a) (hb : 1 ≤ b) (hc : 1 ≤ c) (P : (Foundation.Tensor.directSum fun (x : Fin L) => Foundation.Tensor.matrixCoefficients (Fin a) (Fin b) (Fin c)).PolynomialApproximation r d D) : ↑L * ↑(a * b * c) ^ (omega F / 3) ≤ ↑r