AlphaParameters.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.LowerParameters.sqrt_ge_four line 9
theorem OAI.Problem335.LowerParameters.a_ideal_le line 13
theorem OAI.Problem335.LowerParameters.a_lt_ideal_add_one line 16
theorem OAI.Problem335.LowerParameters.a_scale_lower line 22
theorem OAI.Problem335.LowerParameters.a_scale_upper line 37
theorem OAI.Problem335.LowerParameters.alpha_bounds line 60
theorem OAI.Problem335.LowerParameters.alpha_log_error_bounds line 69
Source documentation
The relative logarithmic rounding error is controlled by the rounded order.
```
theorem alpha_log_error_bounds {n : ℕ} (hn : 16 ≤ n) :
    0 ≤ Real.log (alpha n * Real.sqrt (n : ℝ)) ∧
      Real.log (alpha n * Real.sqrt (n : ℝ)) ≤ 2 / (a n : ℝ) := by
…
```
Mentions: OAI.Problem335.LowerParameters.alpha, OAI.Problem335.LowerParameters.a
theorem OAI.Problem335.LowerParameters.sq_div_a_le line 100
Source documentation
The occupation-moment error from differentiation is of order n^(-1/2).
```
theorem sq_div_a_le {n : ℕ} (hn : 16 ≤ n) :
    (n : ℝ) ^ 2 / (a n : ℝ) ≤ 4 / Real.sqrt (n : ℝ) := by
…
```
Mentions: OAI.Problem335.LowerParameters.a
theorem OAI.Problem335.LowerParameters.sq_div_v_le line 109
Source documentation
The ambient-variable occupation error has the better order 1/n.
```
theorem sq_div_v_le {n : ℕ} (hn : 16 ≤ n) :
    (n : ℝ) ^ 2 / (v n : ℝ) ≤ 8 / (3 * (n : ℝ)) := by
…
```
Mentions: OAI.Problem335.LowerParameters.v
theorem OAI.Problem335.LowerParameters.a_isTheta line 119
Source documentation
Uniform two-sided growth of the chosen differentiation order.
```
theorem a_isTheta :
    Asymptotics.IsTheta Filter.atTop (fun n : ℕ => (a n : ℝ))
      (fun n : ℕ => (n : ℝ) ^ 2 * Real.sqrt (n : ℝ)) := by
…
```
Mentions: OAI.Problem335.LowerParameters.a