SpectralLimit.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Removing positive slack from the spectral inequality

The positive slack in the exponent can be sent to zero with the matrix size fixed. A bound at all positive natural sizes then removes a fixed additive error term.

theorem OAI.MatrixMultiplication.AuxiliarySeparation.spectral_bound_of_positive_slack line 20

Source documentation

Continuity removes the positive slack in the spectral exponent.

theorem spectral_bound_of_positive_slack {ν k D : ℝ} {d n : ℕ}
    (hν : 0 < ν) (hn : 1 ≤ n)
    (hbound : ∀ δ : ℝ, 0 < δ →
      (d : ℝ) ^ ν * (n : ℝ) ^ (ν / (ν + δ)) ≤ (n : ℝ) * k + D) :
    (d : ℝ) ^ ν * (n : ℝ) ≤ (n : ℝ) * k + D := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.coefficient_le_of_nat_mul_bound line 48
Source documentation
A fixed additive error cannot enlarge a coefficient bounded at every positive natural size.
```
theorem coefficient_le_of_nat_mul_bound {a k D : ℝ}
    (hbound : ∀ n : ℕ, 1 ≤ n → a * (n : ℝ) ≤ (n : ℝ) * k + D) :
    a ≤ k := by
…
```

theorem OAI.MatrixMultiplication.AuxiliarySeparation.spectral_coefficient_le_of_all_nat line 65

Source documentation

Uniform spectral inequalities for all positive sizes and all positive slacks force the desired coefficient bound.

theorem spectral_coefficient_le_of_all_nat {ν k D : ℝ} {d : ℕ}
    (hν : 0 < ν)
    (hbound : ∀ n : ℕ, 1 ≤ n → ∀ δ : ℝ, 0 < δ →
      (d : ℝ) ^ ν * (n : ℝ) ^ (ν / (ν + δ)) ≤ (n : ℝ) * k + D) :
    (d : ℝ) ^ ν ≤ k := by
…