SubexponentialTransfer.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Conversion from the computed-height bounds to asymptotics in the actual input length. The bounds concern scalar envelopes, not an uncharged program.

theorem OAI.EditApproximation.fixed_accuracy_large_branch_eventually line 14
theorem OAI.EditApproximation.subexponential_height_to_input line 19
theorem OAI.EditApproximation.sublinear_height_near_linear line 42
def OAI.EditApproximation.computedTotalOverheadExponent line 50
theorem OAI.EditApproximation.computedTotalOverheadExponent_tendsto line 56
theorem OAI.EditApproximation.computed_total_overhead_subpolynomial line 68
def OAI.EditApproximation.computedCompleteOverheadExponent line 75
theorem OAI.EditApproximation.computedCompleteOverheadExponent_tendsto line 78
theorem OAI.EditApproximation.computed_complete_overhead_subpolynomial line 91
Source documentation
The combined coarse, local-enumeration and dependency scalar envelope is subpolynomial in the actual total input length.
```
theorem computed_complete_overhead_subpolynomial (C₁ C₂ C₃ C₄ C₅ epsilon : ℝ)
    (hepsilon : 0 < epsilon) :
    ∀ᶠ N in atTop, Real.exp (computedCompleteOverheadExponent C₁ C₂ C₃ C₄ C₅ N) ≤
      (N + 2 : ℝ) ^ epsilon :=
…
```
Mentions: OAI.EditApproximation.computedCompleteOverheadExponent