Recurrence.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

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 OAI.MatrixMultiplication.AuxiliarySeparation.growthRecurrence_step_real line 18

Source documentation

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 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 := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.growthRecurrence_step line 47

Source documentation

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

theorem 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 := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.growthRecurrence_induction line 65

Source documentation

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

theorem 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 := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.growthRecurrence_induction_shifted line 91

Source documentation

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

theorem 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) ∧
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.growthProduct_le_slope_and_diagonal line 121

Source documentation

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

theorem 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) := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.growthProduct

theorem OAI.MatrixMultiplication.AuxiliarySeparation.diagonal_fourth_power_lower line 140

Source documentation

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

theorem 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 := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.diagonal_fourth_power_lower_of_one_le line 166

Source documentation

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

theorem 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 := by
…