Profile.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

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 OAI.MatrixMultiplication.AuxiliarySeparation.ScalarProfile line 23
Source documentation
The scalar profile hypotheses used in Section 6. Only positive indices carry mathematical content; the values on either coordinate axis are unused.
```
structure ScalarProfile (t : ℝ) where
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.ScalarProfile.exists_row_slope line 39
Source documentation
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 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) ∧
      Tendsto (fun h : ℕ => P.value a h / (h : ℝ)) atTop (𝓝 g) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.ScalarProfile

theorem OAI.MatrixMultiplication.AuxiliarySeparation.ScalarProfile.exists_row_slopes line 61

Source documentation

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

theorem 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) ∧
      Tendsto (fun h : ℕ => P.value a h / (h : ℝ)) atTop (𝓝 (g a)) := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.ScalarProfile

theorem OAI.MatrixMultiplication.AuxiliarySeparation.ScalarProfile.diagonal_fourth_power_lower line 78
Source documentation
The exact polynomial lower bound on the diagonal, obtained from row concavity, shifted tripling, and the simultaneous scalar induction.
```
theorem diagonal_fourth_power_lower {t : ℝ} (P : ScalarProfile t)
    (n : ℕ) (hn : 1 ≤ n) : (n : ℝ) ^ 4 ≤ P.value n n ^ 3 := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.ScalarProfile
theorem OAI.MatrixMultiplication.AuxiliarySeparation.ScalarProfile.exponent_le_three_quarters line 108
Source documentation
Lemma 6.1: a positive symmetric profile satisfying the stated concavity, tripling, boundary, and rank bounds has exponent at most 3/4.
```
theorem exponent_le_three_quarters {t : ℝ} (P : ScalarProfile t) (ht : 0 < t) :
    t ≤ 3 / 4 := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.ScalarProfile

theorem OAI.MatrixMultiplication.AuxiliarySeparation.profile_exponent_le_three_quarters line 122

Source documentation

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

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