Product.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

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.

def OAI.MatrixMultiplication.AuxiliarySeparation.growthProduct line 17
Source documentation
The product sequence from Section 6, indexed from zero.
```
noncomputable def growthProduct : ℕ → ℝ
  | 0 => 1
  | n + 1 => growthProduct n * (1 + 1 / (3 * ((n : ℝ) + 1)))
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.growthProduct_zero line 21
theorem OAI.MatrixMultiplication.AuxiliarySeparation.growthProduct_succ line 23
theorem OAI.MatrixMultiplication.AuxiliarySeparation.growthProduct_pos line 26
theorem OAI.MatrixMultiplication.AuxiliarySeparation.one_add_recip_three_cube_lower line 34
Source documentation
Cubing one product factor dominates the corresponding telescoping factor.
```
theorem one_add_recip_three_cube_lower {a : ℝ} (ha : 0 < a) :
    1 + 1 / a ≤ (1 + 1 / (3 * a)) ^ 3 := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.growthProduct_cube_lower line 44
Source documentation
The exact lower bound Gₙ₊₁³ ≥ n + 1.
```
theorem growthProduct_cube_lower (n : ℕ) :
    (n : ℝ) + 1 ≤ growthProduct n ^ 3 := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.growthProduct