Documentation

LeanPool.MatrixMultiplicationAllFields.LinearAlgebra.MatrixMultiplication.AuxiliarySeparation.Growth.ProfileSlopes

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.

source
def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.shiftedTriplingIndex (c h : ℕ) :
ℕ → ℕ

The indices obtained by repeatedly applying the affine tripling map.

Equations
Instances For
    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.shiftedTriplingIndex_lower (c h : ℕ) (hh : 1 ≤ h) (j : ℕ) :
    h + j ≤ shiftedTriplingIndex c h j

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

    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.shiftedTriplingIndex_tendsto (c h : ℕ) (hh : 1 ≤ h) :
    Filter.Tendsto (shiftedTriplingIndex c h) Filter.atTop Filter.atTop
    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.shiftedTriplingIndex_cast (c h j : ℕ) :
    ↑(shiftedTriplingIndex c h j) + ↑c / 2 = 3 ^ j * (↑h + ↑c / 2)

    The exact affine solution, written without truncated natural subtraction.

    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.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)

    Iterating the tripling inequality multiplies the profile by powers of three.

    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.profile_le_affine_slope {P : ℕ → ℝ} {g : ℝ} {c h : ℕ} (hh : 1 ≤ h) (htrip : ∀ (n : ℕ), 1 ≤ n → 3 * P n ≤ P (3 * n + c)) (hlim : Filter.Tendsto (fun (n : ℕ) => P n / ↑n) Filter.atTop (nhds g)) :
    P h ≤ (↑h + ↑c / 2) * g

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

    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.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 → Filter.Tendsto (fun (h : ℕ) => P a h / ↑h) Filter.atTop (nhds (g a))) (a h : ℕ) (ha : 1 ≤ a) (hh : 1 ≤ h) :
    P a h ≤ (↑h + (↑a - 1) / 2) * g a

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

    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.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 → Filter.Tendsto (fun (h : ℕ) => P a h / ↑h) Filter.atTop (nhds (g a))) (a : ℕ) (ha : 1 ≤ a) :
    P a a ≤ (3 * ↑a - 1) / 2 * g a

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

    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.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)

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