WordWeightParameters.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Concrete numerical hypotheses for the balanced path-word sum.

theorem OAI.Problem335.LowerParameters.one_le_inv_alpha line 11
theorem OAI.Problem335.LowerParameters.alpha_run_scale_le line 16
Source documentation
Every true run costs at most one factor of the matrix dimension.
```
theorem alpha_run_scale_le {n : ℕ} (hn : 4 ≤ n) :
    (alpha n) ^ (-(1 + rho n)) ≤ (n : ℝ) :=
…
```
Mentions: OAI.Problem335.LowerParameters.alpha, OAI.Problem335.LowerParameters.rho
theorem OAI.Problem335.LowerParameters.word_error_mul_n_le_half line 22
Source documentation
The accumulated beta rounding error is already bounded by one half.
```
theorem word_error_mul_n_le_half {n : ℕ} (hn : 16 ≤ n) :
    (2 / (b n : ℝ)) * (n : ℝ) ≤ 1 / 2 := by
…
```
Mentions: OAI.Problem335.LowerParameters.b
theorem OAI.Problem335.LowerParameters.word_error_mul_n_le_sqrt line 31

theorem OAI.Problem335.LowerParameters.word_weight_numeric_bounds line 38

Source documentation

All scalar premises of the corrected-word estimate, at the actual rounded parameters. No word-product or graph hypothesis is part of this statement.

theorem word_weight_numeric_bounds {n : ℕ} (hn : 16 ≤ n) :
    0 < alpha n ∧ alpha n ≤ 1 ∧
    1 ≤ (alpha n)⁻¹ ∧ (alpha n)⁻¹ ≤ Real.sqrt (n : ℝ) ∧
    0 ≤ beta n ∧
    beta n ≤ (alpha n) ^ (rho n) * Real.exp (2 / (b n : ℝ)) ∧
    (alpha n) ^ (-(1 + rho n)) ≤ (n : ℝ) ∧
    0 ≤ 2 / (b n : ℝ) ∧
    (2 / (b n : ℝ)) * (n : ℝ) ≤ Real.sqrt (n : ℝ) := by
…

Mentions: OAI.Problem335.LowerParameters.alpha, OAI.Problem335.LowerParameters.beta, OAI.Problem335.LowerParameters.rho, OAI.Problem335.LowerParameters.b