Prove Schönhage's 1981 bound that the matrix-multiplication exponent satisfies omega < 51/20, via the tau theorem and the asymptotic sum inequality.
theorem mme_omega_lt {K : Type u} [Field K] : matMulExp K < 51 / 20 := by sorrySchönhage's bound: .
The matrix-multiplication exponent governs the asymptotic cost of multiplying matrices: it is the infimum of exponents for which arithmetic operations suffice. Equivalently (the form used here) it is the tensor-rank exponent
where is the matrix-multiplication tensor and is tensor rank. This theorem asserts , the bound Schönhage obtained in 1981 via his (direct-sum) theorem and the asymptotic sum inequality. Here matMulExp is the tensor-rank exponent from definition mme_omega.
No open leaves. Every sub-goal is proved or awaiting decomposition.