ProfileSlopes.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Shifted tripling and diagonal increments

These are the two estimates on the limiting row slopes used in Section 6. Iteration retains the additive shift in the tripling inequality. Symmetry then expresses a diagonal step as one increment in each of two adjacent rows.

def OAI.MatrixMultiplication.AuxiliarySeparation.shiftedTriplingIndex line 19

Source documentation

The indices obtained by repeatedly applying the affine tripling map.

def shiftedTriplingIndex (c h : ℕ) : ℕ → ℕ
  | 0 => h
  | j + 1 => 3 * shiftedTriplingIndex c h j + c

/-- Starting at a positive index, affine tripling escapes to infinity. -/

theorem OAI.MatrixMultiplication.AuxiliarySeparation.shiftedTriplingIndex_lower line 24
Source documentation
Starting at a positive index, affine tripling escapes to infinity.
```
theorem shiftedTriplingIndex_lower (c h : ℕ) (hh : 1 ≤ h) (j : ℕ) :
    h + j ≤ shiftedTriplingIndex c h j := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.shiftedTriplingIndex
theorem OAI.MatrixMultiplication.AuxiliarySeparation.shiftedTriplingIndex_tendsto line 32
theorem OAI.MatrixMultiplication.AuxiliarySeparation.shiftedTriplingIndex_cast line 41
Source documentation
The exact affine solution, written without truncated natural subtraction.
```
theorem shiftedTriplingIndex_cast (c h j : ℕ) :
    (shiftedTriplingIndex c h j : ℝ) + (c : ℝ) / 2 =
      (3 : ℝ) ^ j * ((h : ℝ) + (c : ℝ) / 2) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.shiftedTriplingIndex
theorem OAI.MatrixMultiplication.AuxiliarySeparation.shiftedTripling_profile_lower line 52
Source documentation
Iterating the tripling inequality multiplies the profile by powers of three.
```
theorem shiftedTripling_profile_lower {P : ℕ → ℝ} {c h : ℕ} (hh : 1 ≤ h)
    (htrip : ∀ n : ℕ, 1 ≤ n → 3 * P n ≤ P (3 * n + c)) (j : ℕ) :
    (3 : ℝ) ^ j * P h ≤ P (shiftedTriplingIndex c h j) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.shiftedTriplingIndex

theorem OAI.MatrixMultiplication.AuxiliarySeparation.profile_le_affine_slope line 67

Source documentation

A row with a limiting linear slope and shifted tripling lies below the corresponding affine multiple of that slope.

theorem profile_le_affine_slope {P : ℕ → ℝ} {g : ℝ} {c h : ℕ}
    (hh : 1 ≤ h)
    (htrip : ∀ n : ℕ, 1 ≤ n → 3 * P n ≤ P (3 * n + c))
    (hlim : Tendsto (fun n : ℕ => P n / (n : ℝ)) atTop (𝓝 g)) :
    P h ≤ ((h : ℝ) + (c : ℝ) / 2) * g := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.profile_row_le_slope line 106

Source documentation

The row estimate in the positive-index notation of the paper.

theorem profile_row_le_slope {P : ℕ → ℕ → ℝ} {g : ℕ → ℝ}
    (htrip : ∀ a : ℕ, 1 ≤ a → ∀ h : ℕ, 1 ≤ h →
      3 * P a h ≤ P a (3 * h + a - 1))
    (hlim : ∀ a : ℕ, 1 ≤ a →
      Tendsto (fun h : ℕ => P a h / (h : ℝ)) atTop (𝓝 (g a)))
    (a h : ℕ) (ha : 1 ≤ a) (hh : 1 ≤ h) :
    P a h ≤ ((h : ℝ) + ((a : ℝ) - 1) / 2) * g a := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.profile_diagonal_le_slope line 124

Source documentation

The diagonal is bounded above by the limiting row slope with the precise coefficient (3a-1)/2.

theorem profile_diagonal_le_slope {P : ℕ → ℕ → ℝ} {g : ℕ → ℝ}
    (htrip : ∀ a : ℕ, 1 ≤ a → ∀ h : ℕ, 1 ≤ h →
      3 * P a h ≤ P a (3 * h + a - 1))
    (hlim : ∀ a : ℕ, 1 ≤ a →
      Tendsto (fun h : ℕ => P a h / (h : ℝ)) atTop (𝓝 (g a)))
    (a : ℕ) (ha : 1 ≤ a) :
    P a a ≤ ((3 * (a : ℝ) - 1) / 2) * g a := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.diagonal_increment_of_slope_lower line 136

Source documentation

Symmetry identifies a diagonal step with one increment in each adjacent row. Only positive-index symmetry and slope bounds are used.

theorem diagonal_increment_of_slope_lower {P : ℕ → ℕ → ℝ} {g : ℕ → ℝ}
    (hsymm : ∀ a : ℕ, 1 ≤ a → ∀ b : ℕ, 1 ≤ b → P a b = P b a)
    (hinc : ∀ a : ℕ, 1 ≤ a → ∀ h : ℕ, 1 ≤ h →
      g a ≤ P a (h + 1) - P a h)
    (n : ℕ) (hn : 1 ≤ n) :
    P n n + g n + g (n + 1) ≤ P (n + 1) (n + 1) := by
…