ActualBalancedWordSum.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.LowerParameters.actual_balanced_word_sum_bound line 13
Source documentation
The complete corrected path-word estimate at the actual lower-bound parameters and balanced schedule. There are no remaining weight assumptions.
```
theorem actual_balanced_word_sum_bound {n : ℕ} (hn : 16 ≤ n) :
    (∑ w : Fin n → Bool,
      IsolatedWeight.weight (BalancedSchedule.internalEdges n)
        (Finset.univ.filter (fun i => balancedLayer (show 4 ≤ n by omega) i = true))
        BalancedSchedule.adjacent (alpha n)⁻¹ (beta n) ((n : ℝ)⁻¹) w) ≤
      Real.exp (8 * Real.sqrt (n : ℝ)) := by
…
```
Mentions: OAI.Problem335.IsolatedWeight.weight, OAI.Problem335.BalancedSchedule.internalEdges, OAI.Problem335.LowerParameters.balancedLayer, OAI.Problem335.BalancedSchedule.adjacent, OAI.Problem335.LowerParameters.alpha, OAI.Problem335.LowerParameters.beta