Asymptotics.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Analytic conclusion of the ordered-matrix construction. The polynomial/geometric comparison uses tendsto_pow_const_div_const_pow_of_one_lt.

theorem OAI.Problem348.exists_depth_polynomial_decay line 20

Source documentation

Exponential decay beats the inverse-polynomial distance parameter.

theorem exists_depth_polynomial_decay (c C : ℝ) (hc : 0 < c) :
    ∃ h : ℕ, 1 ≤ h ∧
      (1 / ((386 * (h : ℝ) + 2) ^ 2)) * (1 / ((2 : ℝ) ^ h)) <
        c * Real.rpow (1 / ((386 * (h : ℝ) + 2) ^ 2)) C := by
…