Complex arithmetic programs and asymptotic matrix multiplication costs.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.exists_power_cover {b n : ℕ} (hb : 2 ≤ b) (hn : 1 ≤ n) : ∃ (k : ℕ), n ≤ b ^ k ∧ b ^ k ≤ b * n

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.geometric_cost_recurrence_bound (x : ℕ → ℝ) (a b d q : ℝ) (hx : 0 ≤ x 0) (ha : 0 ≤ a) (hb : 0 ≤ b) (hd : 0 ≤ d) (haq : a < q) (hdq : d ≤ q) (hstep : ∀ (k : ℕ), x (k + 1) ≤ a * x k + b * d ^ k) : ∃ (C : ℝ), 0 < C ∧ ∀ (k : ℕ), x k ≤ C * q ^ k

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.power_cost_padding_bound (hpad : ∀ {n m : ℕ}, n ≤ m → ∀ (P : MatrixAlgorithm m), P.Correct → ∃ (Q : MatrixAlgorithm n), Q.Correct ∧ Q.cost ≤ P.cost) {b : ℕ} (hb : 2 ≤ b) {s C : ℝ} (hs : 0 ≤ s) (hC : 0 < C) (hpower : ∀ (k : ℕ), ∃ (P : MatrixAlgorithm (b ^ k)), P.Correct ∧ ↑P.cost ≤ C * (↑b ^ s) ^ k) : ∃ (D : ℝ), 0 < D ∧ ∀ (n : ℕ), 1 ≤ n → ∃ (P : MatrixAlgorithm n), P.Correct ∧ ↑P.cost ≤ D * ↑n ^ s

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_of_uniform_power_costs (hpad : ∀ {n m : ℕ}, n ≤ m → ∀ (P : MatrixAlgorithm m), P.Correct → ∃ (Q : MatrixAlgorithm n), Q.Correct ∧ Q.cost ≤ P.cost) {b : ℕ} (hb : 2 ≤ b) {τ C : ℝ} (hτ : 0 ≤ τ) (hC : 0 < C) (hpower : ∀ (k : ℕ), ∃ (P : MatrixAlgorithm (b ^ k)), P.Correct ∧ ↑P.cost ≤ C * (↑b ^ τ) ^ k) : AdmissibleExponent τ

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_of_power_costs (hpad : ∀ {n m : ℕ}, n ≤ m → ∀ (P : MatrixAlgorithm m), P.Correct → ∃ (Q : MatrixAlgorithm n), Q.Correct ∧ Q.cost ≤ P.cost) {b : ℕ} (hb : 2 ≤ b) {τ : ℝ} (hτ : 0 ≤ τ) (hpower : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ), 0 < C ∧ ∀ (k : ℕ), ∃ (P : MatrixAlgorithm (b ^ k)), P.Correct ∧ ↑P.cost ≤ C * (↑b ^ (τ + ε)) ^ k) : AdmissibleExponent τ

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_of_recursive_costs (hpad : ∀ {n m : ℕ}, n ≤ m → ∀ (P : MatrixAlgorithm m), P.Correct → ∃ (Q : MatrixAlgorithm n), Q.Correct ∧ Q.cost ≤ P.cost) {b R K : ℕ} (hb : 2 ≤ b) {τ : ℝ} (hτ : 2 ≤ τ) (hR : ↑R ≤ ↑b ^ τ) (P : (k : ℕ) → MatrixAlgorithm (b ^ k)) (hP : ∀ (k : ℕ), (P k).Correct) (hstep : ∀ (k : ℕ), (P (k + 1)).cost ≤ R * (P k).cost + K * (b ^ k) ^ 2) : AdmissibleExponent τ

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.blockRecurrenceCost (b R K : ℕ) : ℕ → ℕ

The recursive arithmetic cost for a fixed block size, rank bound and linear overhead.

Equations

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

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.blockRecurrenceCost_zero (b R K : ℕ) : blockRecurrenceCost b R K 0 = 1

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.blockRecurrenceCost_succ (b R K k : ℕ) : blockRecurrenceCost b R K (k + 1) = R * blockRecurrenceCost b R K k + K * (b ^ k) ^ 2

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.power_programs_of_block_step {b R K : ℕ} (hstep : ∀ (m : ℕ) (P : MatrixAlgorithm m), P.Correct → ∃ (Q : MatrixAlgorithm (b * m)), Q.Correct ∧ Q.cost ≤ R * P.cost + K * m ^ 2) (k : ℕ) : ∃ (P : MatrixAlgorithm (b ^ k)), P.Correct ∧ P.cost ≤ blockRecurrenceCost b R K k

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_of_block_step_of_padding (hpad : ∀ {n m : ℕ}, n ≤ m → ∀ (P : MatrixAlgorithm m), P.Correct → ∃ (Q : MatrixAlgorithm n), Q.Correct ∧ Q.cost ≤ P.cost) {b R K : ℕ} (hb : 2 ≤ b) {τ : ℝ} (hτ : 2 ≤ τ) (hR : ↑R ≤ ↑b ^ τ) (hstep : ∀ (m : ℕ) (P : MatrixAlgorithm m), P.Correct → ∃ (Q : MatrixAlgorithm (b * m)), Q.Correct ∧ Q.cost ≤ R * P.cost + K * m ^ 2) : AdmissibleExponent τ

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_of_block_step {b R K : ℕ} (hb : 2 ≤ b) {τ : ℝ} (hτ : 2 ≤ τ) (hR : ↑R ≤ ↑b ^ τ) (hstep : ∀ (m : ℕ) (P : MatrixAlgorithm m), P.Correct → ∃ (Q : MatrixAlgorithm (b * m)), Q.Correct ∧ Q.cost ≤ R * P.cost + K * m ^ 2) : AdmissibleExponent τ

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_of_rankAtMost {n R : ℕ} (hn : 2 ≤ n) (hRank : (Tensor.matrixMultiplication n n n).RankAtMost R) {τ : ℝ} (hτ : 2 ≤ τ) (hR : ↑R ≤ ↑n ^ τ) : AdmissibleExponent τ