OAI/Combinatorics/EditApproximation/Geometry/ParameterAsymptotics.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Growth of the computed parameters

These are scalar estimates for the literal integer parameters of Section 10. They do not assert an evaluator cost: the recursive-input and charged local work bounds must be connected to these estimates separately.

  1. theorem OAI.EditApproximation.heightExponent_tendsto line 18
  2. theorem OAI.EditApproximation.inputSmallLog_tendsto line 23
  3. theorem OAI.EditApproximation.smallLogExponent_tendsto line 28
  4. theorem OAI.EditApproximation.inputSmallLog_log_two line 34
  5. theorem OAI.EditApproximation.coarseExponent_tendsto line 38
  6. theorem OAI.EditApproximation.heightExponent_real_tendsto line 45
  7. theorem OAI.EditApproximation.inputSmallLog_real_tendsto line 49
  8. theorem OAI.EditApproximation.coarseExponent_real_tendsto line 53
  9. theorem OAI.EditApproximation.inputSmallLog_real_log line 57
  10. theorem OAI.EditApproximation.shifted_square_log_bound line 61
  11. theorem OAI.EditApproximation.coarse_shifted_square_log_bound line 73
  12. theorem OAI.EditApproximation.coarse_shifted_square_div_log_tendsto line 86

    Source documentation

    The central earlier-index dependency exponent in Section 10 is sublinear.

    theorem coarse_shifted_square_div_log_tendsto :
    Tendsto (fun N => ((coarseExponent (inputSmallLog N) : ℝ) + 1) ^ 2 /
      Real.log (inputSmallLog N : ℝ)) atTop (𝓝 0) := by
…

    Mentions: OAI.EditApproximation.coarseExponent, OAI.EditApproximation.inputSmallLog

  13. theorem OAI.EditApproximation.inputSmallLog_div_height_tendsto line 105
  14. theorem OAI.EditApproximation.log_smallLog_div_smallLog_tendsto line 119