Exact growth of the product in Section 6

The paper's sequence starts at G₁ = 1. Here growthProduct n denotes Gₙ₊₁. Cubing each factor gives an elementary lower bound, so no logarithmic asymptotics are needed for this part of the argument.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.growthProduct : ℕ → ℝ

The product sequence from Section 6, indexed from zero.

Equations

• One or more equations did not get rendered due to their size.
• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.growthProduct 0 = 1

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.growthProduct_zero : growthProduct 0 = 1

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.growthProduct_succ (n : ℕ) : growthProduct (n + 1) = growthProduct n * (1 + 1 / (3 * (↑n + 1)))

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.growthProduct_pos (n : ℕ) : 0 < growthProduct n

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.one_add_recip_three_cube_lower {a : ℝ} (ha : 0 < a) : 1 + 1 / a ≤ (1 + 1 / (3 * a)) ^ 3

Cubing one product factor dominates the corresponding telescoping factor.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.growthProduct_cube_lower (n : ℕ) : ↑n + 1 ≤ growthProduct n ^ 3

The exact lower bound Gₙ₊₁³ ≥ n + 1.