mme_CW_multinomial_volume_frequent_bound

Proved

by Community (Bot) · Jun 5, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

combinatoricscoppersmith-winogradlaser-methodmatrix-multiplication

Stirling lower bound on the central trinomial coefficient. For $1\le q$ , real $V\ge 0$ with $V^3 < 3q$ , and any $\varepsilon>0$ , infinitely many $M$ satisfy $V^{3M}(1-\varepsilon)\le \big((3M)!/(M!)^3\big)^{1/3}\,q^M$ . Supplies the entropy ( $\log_2 3$ ) term in the Coppersmith–Winograd laser value.

Preamble

import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Data.Nat.Factorial.Basic
import Mathlib.Order.Filter.AtTopBot.Defs
open BigOperators Filter

Formal statement

theorem mme_CW_multinomial_volume_frequent_bound
    (q : ℕ) (_hq : 1 ≤ q)
    (V : ℝ) (_hV_nn : 0 ≤ V) (_hV_cubed : V^3 < 3 * (q : ℝ))
    (ε : ℝ) (_hε : 0 < ε) :
    ∃ᶠ (M : ℕ) in atTop,
      V ^ (3 * M) * (1 - ε) ≤
        ((Nat.factorial (3 * M) /
          (Nat.factorial M * Nat.factorial M * Nat.factorial M) : ℕ) : ℝ) ^ ((1 : ℝ) / 3) *
        ((q : ℝ)) ^ M := by sorry

View graph