Growth of the scalar profile

This file proves the scalar implication of Section 6 (Lemma 6.1). The profile properties are explicit hypotheses: the construction of a profile from a tensor character and the proof of those properties are separate arguments.

structure MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.ScalarProfile (t : ℝ) : Type

The scalar profile hypotheses used in Section 6. Only positive indices carry mathematical content; the values on either coordinate axis are unused.

• value : ℕ → ℕ → ℝ

  The scalar profile value at a pair of positive tensor dimensions.

• positive (a b : ℕ) : 1 ≤ a → 1 ≤ b → 0 < self.value a b
• symmetric (a b : ℕ) : 1 ≤ a → 1 ≤ b → self.value a b = self.value b a
• boundary (b : ℕ) : 1 ≤ b → self.value 1 b = ↑b
• concave (a h : ℕ) : 1 ≤ a → 2 ≤ h → self.value a (h - 1) + self.value a (h + 1) ≤ 2 * self.value a h
• tripling (a h : ℕ) : 1 ≤ a → 1 ≤ h → 3 * self.value a h ≤ self.value a (3 * h + a - 1)
• rank_bound (a b : ℕ) : 1 ≤ a → 1 ≤ b → self.value a b ≤ (↑a + ↑b - 1) ^ (1 / t)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.ScalarProfile.exists_row_slope {t : ℝ} (P : ScalarProfile t) (a : ℕ) (ha : 1 ≤ a) : ∃ (g : ℝ), 0 ≤ g ∧ (∀ (h : ℕ), 1 ≤ h → g ≤ P.value a (h + 1) - P.value a h) ∧ Filter.Tendsto (fun (h : ℕ) => P.value a h / ↑h) Filter.atTop (nhds g)

Each row has a nonnegative limiting slope that bounds every increment from below and equals the limit of the row divided by its index.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.ScalarProfile.exists_row_slopes {t : ℝ} (P : ScalarProfile t) : ∃ (g : ℕ → ℝ), ∀ (a : ℕ), 1 ≤ a → 0 ≤ g a ∧ (∀ (h : ℕ), 1 ≤ h → g a ≤ P.value a (h + 1) - P.value a h) ∧ Filter.Tendsto (fun (h : ℕ) => P.value a h / ↑h) Filter.atTop (nhds (g a))

Choose the row slopes together, retaining their bounds and limits on all positive rows.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.ScalarProfile.diagonal_fourth_power_lower {t : ℝ} (P : ScalarProfile t) (n : ℕ) (hn : 1 ≤ n) : ↑n ^ 4 ≤ P.value n n ^ 3

The exact polynomial lower bound on the diagonal, obtained from row concavity, shifted tripling, and the simultaneous scalar induction.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.ScalarProfile.exponent_le_three_quarters {t : ℝ} (P : ScalarProfile t) (ht : 0 < t) : t ≤ 3 / 4

Lemma 6.1: a positive symmetric profile satisfying the stated concavity, tripling, boundary, and rank bounds has exponent at most 3/4.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.profile_exponent_le_three_quarters {P : ℕ → ℕ → ℝ} {t : ℝ} (ht : 0 < t) (hpositive : ∀ (a b : ℕ), 1 ≤ a → 1 ≤ b → 0 < P a b) (hsymmetric : ∀ (a b : ℕ), 1 ≤ a → 1 ≤ b → P a b = P b a) (hboundary : ∀ (b : ℕ), 1 ≤ b → P 1 b = ↑b) (hconcave : ∀ (a h : ℕ), 1 ≤ a → 2 ≤ h → P a (h - 1) + P a (h + 1) ≤ 2 * P a h) (htripling : ∀ (a h : ℕ), 1 ≤ a → 1 ≤ h → 3 * P a h ≤ P a (3 * h + a - 1)) (hrank : ∀ (a b : ℕ), 1 ≤ a → 1 ≤ b → P a b ≤ (↑a + ↑b - 1) ^ (1 / t)) : t ≤ 3 / 4

The scalar profile implication, with every profile assumption displayed explicitly rather than bundled in ScalarProfile.