Rectangular matrix multiplication algorithms and their asymptotic exponents.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.rectangular_power_cost_padding_bound {F : Type u_1} [Field F] {a b : ℕ} (ha : 2 ≤ a) {k s C : ℝ} (hk : 0 ≤ k) (hab : ↑a ^ k ≤ ↑b) (hs : 0 ≤ s) (hC : 0 < C) (hpower : ∀ (t : ℕ), ∃ (P : MatrixAlgorithm F (a ^ t) (b ^ t) (a ^ t)), P.Correct ∧ ↑P.cost ≤ C * (↑a ^ s) ^ t) : ∃ (D : ℝ), 0 < D ∧ ∀ (n : ℕ), 1 ≤ n → ∃ (P : MatrixAlgorithm F n (innerSize n k) n), P.Correct ∧ ↑P.cost ≤ D * ↑n ^ s

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_of_power_costs {F : Type u_1} [Field F] {a b : ℕ} (ha : 2 ≤ a) {k τ : ℝ} (hk : 0 ≤ k) (hab : ↑a ^ k ≤ ↑b) (hτ : 0 ≤ τ) (hpower : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℕ), ∃ (P : MatrixAlgorithm F (a ^ t) (b ^ t) (a ^ t)), P.Correct ∧ ↑P.cost ≤ C * (↑a ^ (τ + ε)) ^ t) : RectangularAdmissibleExponent F k τ

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.rectangularBlockCost (a b R K : ℕ) : ℕ → ℕ

The recursive cost of rectangular block multiplication with explicit linear overhead.

Equations

• One or more equations did not get rendered due to their size.
• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.rectangularBlockCost a b R K 0 = 1

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.rectangularBlockCost_zero (a b R K : ℕ) : rectangularBlockCost a b R K 0 = 1

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.rectangularBlockCost_succ (a b R K t : ℕ) : rectangularBlockCost a b R K (t + 1) = R * rectangularBlockCost a b R K t + K * ((a * b) ^ t + (a ^ 2) ^ t)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.rectangularBlockCost_bound {a b R K : ℕ} (ha : 2 ≤ a) {τ ε : ℝ} (hε : 0 < ε) (hR : ↑R ≤ ↑a ^ τ) (hin : ↑(a * b) ≤ ↑a ^ τ) (hout : ↑a ^ 2 ≤ ↑a ^ τ) : ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℕ), ↑(rectangularBlockCost a b R K t) ≤ C * (↑a ^ (τ + ε)) ^ t

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.rectangular_power_programs_of_block_step {F : Type u_1} [Field F] {a b R K : ℕ} (hscalar : ∃ (P : MatrixAlgorithm F 1 1 1), P.Correct ∧ P.cost ≤ 1) (hstep : ∀ (m p : ℕ) (P : MatrixAlgorithm F m p m), P.Correct → ∃ (Q : MatrixAlgorithm F (a * m) (b * p) (a * m)), Q.Correct ∧ Q.cost ≤ R * P.cost + K * (m * p + m ^ 2)) (t : ℕ) : ∃ (P : MatrixAlgorithm F (a ^ t) (b ^ t) (a ^ t)), P.Correct ∧ P.cost ≤ rectangularBlockCost a b R K t

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_of_block_step {F : Type u_1} [Field F] {a b R K : ℕ} (ha : 2 ≤ a) {k τ : ℝ} (hk : 0 ≤ k) (hab : ↑a ^ k ≤ ↑b) (hτ : 0 ≤ τ) (hR : ↑R ≤ ↑a ^ τ) (hin : ↑(a * b) ≤ ↑a ^ τ) (hout : ↑a ^ 2 ≤ ↑a ^ τ) (hscalar : ∃ (P : MatrixAlgorithm F 1 1 1), P.Correct ∧ P.cost ≤ 1) (hstep : ∀ (m p : ℕ) (P : MatrixAlgorithm F m p m), P.Correct → ∃ (Q : MatrixAlgorithm F (a * m) (b * p) (a * m)), Q.Correct ∧ Q.cost ≤ R * P.cost + K * (m * p + m ^ 2)) : RectangularAdmissibleExponent F k τ