LowerAsymptotics.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.size_lower_bound_of_rank_bounds line 13

Source documentation

The numerical comparison in the lower-bound argument, with an explicit sufficient logarithmic threshold. No algebraic complexity hypotheses enter here.

theorem size_lower_bound_of_rank_bounds
    (x S D R C₁ C₂ : ℝ)
    (hx : 1 ≤ x) (hS : 0 ≤ S) (hD : 0 < D)
    (hlog : 400 * (|C₁| + |C₂| + 1) ≤ Real.log x)
    (hlower : D * Real.exp (-C₁ * Real.sqrt x) ≤ R)
    (hupper : R ≤ 2 * S ^ 2 * D * Real.exp (C₂ * Real.sqrt x) *
      x ^ (-Real.sqrt x / 100)) :
    x ^ (Real.sqrt x / 400) ≤ S := by
…

theorem OAI.Problem335.eventual_size_lower_bound_of_rank_bounds line 55

Source documentation

Fixed exponential losses can be absorbed uniformly into the power saving. The threshold is independent of S, D, and the rank value R.

theorem eventual_size_lower_bound_of_rank_bounds (C₁ C₂ : ℝ) :
    ∃ n₀ : ℕ, ∀ n : ℕ, n₀ ≤ n → ∀ S D R : ℝ,
      0 ≤ S → 0 < D →
      D * Real.exp (-C₁ * Real.sqrt (n : ℝ)) ≤ R →
      R ≤ 2 * S ^ 2 * D * Real.exp (C₂ * Real.sqrt (n : ℝ)) *
        (n : ℝ) ^ (-Real.sqrt (n : ℝ) / 100) →
      (n : ℝ) ^ (Real.sqrt (n : ℝ) / 400) ≤ S := by
…