ParameterGrowth.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.LowerParameters.b_isTheta line 11
Source documentation
The actual multiplication order, without an extra conditional parameter hypothesis, has the growth asserted in the rank-method parameter lemma.
```
theorem b_isTheta :
    Asymptotics.IsTheta Filter.atTop (fun n : ℕ => (b n : ℝ))
      (fun n : ℕ => (n : ℝ) ^ 2 * Real.sqrt (n : ℝ)) := by
…
```
Mentions: OAI.Problem335.LowerParameters.b

theorem OAI.Problem335.LowerParameters.eventually_order_growth_bounds line 20

Source documentation

Simultaneous explicit growth bounds for the two rounded orders.

theorem eventually_order_growth_bounds :
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
      (n : ℝ) ^ 2 * Real.sqrt (n : ℝ) / 4 ≤ (a n : ℝ) ∧
      (a n : ℝ) ≤ 3 * (n : ℝ) ^ 2 * Real.sqrt (n : ℝ) ∧
      (n : ℝ) ^ 2 * Real.sqrt (n : ℝ) / 4 ≤ (b n : ℝ) ∧
      (b n : ℝ) ≤ 4 * (n : ℝ) ^ 2 * Real.sqrt (n : ℝ) := by
…

Mentions: OAI.Problem335.LowerParameters.a, OAI.Problem335.LowerParameters.b