p2m_Tensor_matMulExp

import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Definitions.Def_p2m_StrassenPreorder
import Definitions.Def_p2m_StrassenPreorder_rank
import Definitions.Def_p2m_TensorObj_p1
import Definitions.Def_p2m_TensorObj_p2
import Definitions.Def_p2m_TensorObj_p3
import Definitions.Def_p2m_TensorObj_p4
import Definitions.Def_p2m_Tensor_quot
import Definitions.Def_p2m_Restriction
import Definitions.Def_p2m_MM

universe u

namespace Tensor

variable {K : Type u} [Field K]

/-- The matrix multiplication exponent `ω`, defined as
    `inf_{n ≥ 2} { log Rk(MM n n n) / log n }` where `Rk` is the ordinary
    integer rank with respect to the canonical `Restrict`-based Strassen
    preorder on `Tensor K 3`. This is an intrinsic invariant of the
    semiring, not depending on any abstract preorder `P`. -/
noncomputable def matMulExp : ℝ :=
  iInf (fun n : ℕ =>
    if 1 < n then
      Real.log (StrassenPreorder.rank Tensor.instStrassenPreorder
        (MM (K := K) n n n) : ℝ) / Real.log n
    else 3)

end Tensor