The scalar simultaneous induction in Section 6

The two diagonal inequalities imply, simultaneously, lower bounds for the limiting row slopes and for the diagonal profile. All profile properties needed for this argument are expressed as hypotheses below.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.growthRecurrence_step_real {n Dprev Dnext gprev gnext Gprev : ℝ} (hn : 0 < n) (hupper : Dnext ≤ (3 * (n + 1) - 1) / 2 * gnext) (hincrement : Dprev + gprev + gnext ≤ Dnext) (hgprev : Gprev ≤ gprev) (hDprev : (3 * n - 1) / 2 * Gprev ≤ Dprev) : (1 + 1 / (3 * n)) * Gprev ≤ gnext ∧ (3 * (n + 1) - 1) / 2 * ((1 + 1 / (3 * n)) * Gprev) ≤ Dnext

One step of the Section 6 simultaneous induction, with a positive real index. The proof uses the diagonal increment inequality to obtain the second conclusion as well as the first.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.growthRecurrence_step {n : ℕ} (hn : 1 ≤ n) {Dprev Dnext gprev gnext Gprev : ℝ} (hupper : Dnext ≤ (3 * (↑n + 1) - 1) / 2 * gnext) (hincrement : Dprev + gprev + gnext ≤ Dnext) (hgprev : Gprev ≤ gprev) (hDprev : (3 * ↑n - 1) / 2 * Gprev ≤ Dprev) : (1 + 1 / (3 * ↑n)) * Gprev ≤ gnext ∧ (3 * (↑n + 1) - 1) / 2 * ((1 + 1 / (3 * ↑n)) * Gprev) ≤ Dnext

The natural-number form of the scalar induction step, indexed by n + 1 so that no truncated subtraction occurs in the recurrence.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.growthRecurrence_induction (D g G : ℕ → ℝ) (hGbase : G 1 = 1) (hgbase : 1 ≤ g 1) (hDbase : 1 ≤ D 1) (hGstep : ∀ (n : ℕ), 1 ≤ n → G (n + 1) = (1 + 1 / (3 * ↑n)) * G n) (hupper : ∀ (n : ℕ), 1 ≤ n → D n ≤ (3 * ↑n - 1) / 2 * g n) (hincrement : ∀ (n : ℕ), 1 ≤ n → D n + g n + g (n + 1) ≤ D (n + 1)) (n : ℕ) : 1 ≤ n → G n ≤ g n ∧ (3 * ↑n - 1) / 2 * G n ≤ D n

The simultaneous slope and diagonal estimates, conditional only on the initial values, the recurrence for G, and the two diagonal inequalities.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.growthRecurrence_induction_shifted (D g H : ℕ → ℝ) (hHbase : H 0 = 1) (hgbase : 1 ≤ g 1) (hDbase : 1 ≤ D 1) (hHstep : ∀ (n : ℕ), H (n + 1) = (1 + 1 / (3 * (↑n + 1))) * H n) (hupper : ∀ (n : ℕ), 1 ≤ n → D n ≤ (3 * ↑n - 1) / 2 * g n) (hincrement : ∀ (n : ℕ), 1 ≤ n → D n + g n + g (n + 1) ≤ D (n + 1)) (n : ℕ) : H n ≤ g (n + 1) ∧ (3 * (↑n + 1) - 1) / 2 * H n ≤ D (n + 1)

A zero-indexed version of growthRecurrence_induction, convenient when the initial term of the comparison sequence is stored at index zero.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.growthProduct_le_slope_and_diagonal (D g : ℕ → ℝ) (hgbase : 1 ≤ g 1) (hDbase : 1 ≤ D 1) (hupper : ∀ (n : ℕ), 1 ≤ n → D n ≤ (3 * ↑n - 1) / 2 * g n) (hincrement : ∀ (n : ℕ), 1 ≤ n → D n + g n + g (n + 1) ≤ D (n + 1)) (n : ℕ) : growthProduct n ≤ g (n + 1) ∧ (3 * (↑n + 1) - 1) / 2 * growthProduct n ≤ D (n + 1)

The simultaneous bounds for the explicit comparison product from Section 6.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.diagonal_fourth_power_lower (D g : ℕ → ℝ) (hgbase : 1 ≤ g 1) (hDbase : 1 ≤ D 1) (hupper : ∀ (n : ℕ), 1 ≤ n → D n ≤ (3 * ↑n - 1) / 2 * g n) (hincrement : ∀ (n : ℕ), 1 ≤ n → D n + g n + g (n + 1) ≤ D (n + 1)) (n : ℕ) : (↑n + 1) ^ 4 ≤ D (n + 1) ^ 3

Combining the scalar induction with the elementary product estimate gives an exact fourth-power lower bound on the cube of each diagonal value.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.diagonal_fourth_power_lower_of_one_le (D g : ℕ → ℝ) (hgbase : 1 ≤ g 1) (hDbase : 1 ≤ D 1) (hupper : ∀ (n : ℕ), 1 ≤ n → D n ≤ (3 * ↑n - 1) / 2 * g n) (hincrement : ∀ (n : ℕ), 1 ≤ n → D n + g n + g (n + 1) ≤ D (n + 1)) (n : ℕ) (hn : 1 ≤ n) : ↑n ^ 4 ≤ D n ^ 3

The diagonal fourth-power lower bound using the paper's positive indices.