OccupationParameterBounds.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.LowerParameters.b_scale_lower line 8
theorem OAI.Problem335.LowerParameters.b_scale_upper_of_beta_bound line 14
Source documentation
The eventual beta bound supplies the matching upper growth estimate for b.
```
theorem b_scale_upper_of_beta_bound {n : ℕ} (hn : 16 ≤ n)
    (hbeta : beta n ≤ 2 / Real.sqrt (n : ℝ)) :
    (b n : ℝ) ≤ 4 * (n : ℝ) ^ 2 * Real.sqrt (n : ℝ) := by
…
```
Mentions: OAI.Problem335.LowerParameters.beta, OAI.Problem335.LowerParameters.b
theorem OAI.Problem335.LowerParameters.sq_div_b_le line 34
theorem OAI.Problem335.LowerParameters.sq_div_u_le line 40
theorem OAI.Problem335.LowerParameters.occupation_parameter_loss_le line 49
Source documentation
A concrete bound for the combined occupation-comparison error in both groups.
```
theorem occupation_parameter_loss_le {n : ℕ} (hn : 16 ≤ n) :
    (n : ℝ) ^ 2 / (a n : ℝ) + (n : ℝ) ^ 2 / (v n : ℝ) +
      (n : ℝ) ^ 2 / (b n : ℝ) + (n : ℝ) ^ 2 / (u n : ℝ) ≤
      16 / Real.sqrt (n : ℝ) := by
…
```
Mentions: OAI.Problem335.LowerParameters.a, OAI.Problem335.LowerParameters.v, OAI.Problem335.LowerParameters.b, OAI.Problem335.LowerParameters.u
theorem OAI.Problem335.LowerParameters.occupation_order_loss_le line 76
Source documentation
Both finite occupation laws have uniformly small logarithmic comparison loss.
```
theorem occupation_order_loss_le {n : ℕ} (hn : 16 ≤ n) {H : ℝ}
    (hH : 0 ≤ H) (hHn : H ≤ 2 * (n : ℝ)) :
    H ^ 2 / (a n : ℝ) + H ^ 2 / (2 * (v n : ℝ)) +
      H ^ 2 / (b n : ℝ) + H ^ 2 / (2 * (u n : ℝ)) ≤
      64 / Real.sqrt (n : ℝ) := by
…
```
Mentions: OAI.Problem335.LowerParameters.a, OAI.Problem335.LowerParameters.v, OAI.Problem335.LowerParameters.b, OAI.Problem335.LowerParameters.u

theorem OAI.Problem335.LowerParameters.occupation_two_orders_loss_le line 100

Source documentation

Separate derivative and multiplication expansion orders obey the same loss bound.

theorem occupation_two_orders_loss_le {n : ℕ} (hn : 16 ≤ n) {H₁ H₂ : ℝ}
    (hH₁ : 0 ≤ H₁) (hH₁n : H₁ ≤ 2 * (n : ℝ))
    (hH₂ : 0 ≤ H₂) (hH₂n : H₂ ≤ 2 * (n : ℝ)) :
    H₁ ^ 2 / (a n : ℝ) + H₁ ^ 2 / (2 * (v n : ℝ)) +
      H₂ ^ 2 / (b n : ℝ) + H₂ ^ 2 / (2 * (u n : ℝ)) ≤
      64 / Real.sqrt (n : ℝ) := by
…

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

theorem OAI.Problem335.LowerParameters.b_isTheta_of_eventually_beta_bound line 115
Source documentation
The multiplication order has matching growth once the eventual beta estimate is known.
```
theorem b_isTheta_of_eventually_beta_bound
    (hbeta : ∀ᶠ n : ℕ in Filter.atTop, beta n ≤ 2 / Real.sqrt (n : ℝ)) :
    Asymptotics.IsTheta Filter.atTop (fun n : ℕ => (b n : ℝ))
      (fun n : ℕ => (n : ℝ) ^ 2 * Real.sqrt (n : ℝ)) := by
…
```
Mentions: OAI.Problem335.LowerParameters.beta, OAI.Problem335.LowerParameters.b