ParameterDependencyAsymptotics.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

The actual pass/index count and the exponents in the dependency-path bound. These statements concern computed numbers, independently of the proof that an evaluator satisfies the dependency budgets.

theorem OAI.EditApproximation.le_fourth_root_of_fourth_power_le line 16
theorem OAI.EditApproximation.warmup_smallLog_square_div_height_tendsto line 22
theorem OAI.EditApproximation.computed_warmup_le_refinement_eventually line 46
theorem OAI.EditApproximation.computed_warmup_div_refinement_tendsto line 64
theorem OAI.EditApproximation.scalar_pass_count_bound line 75
theorem OAI.EditApproximation.computed_pass_count_bound line 98
def OAI.EditApproximation.computedDependencyIndexCount line 123
theorem OAI.EditApproximation.scalar_dependency_index_bound line 126
theorem OAI.EditApproximation.computed_dependency_index_bound_eventually line 140
theorem OAI.EditApproximation.coarse_shifted_square_div_smallExponent_tendsto line 158
theorem OAI.EditApproximation.scalar_weighted_dependency_bound line 170
theorem OAI.EditApproximation.weighted_dependency_div_height_tendsto line 187
Source documentation
The exponent of the earlier-index branching factor is o(H).
```
theorem weighted_dependency_div_height_tendsto :
    Tendsto (fun N => ((coarseExponent (inputSmallLog N) : ℝ) + 1) *
      computedDependencyIndexCount N * Real.log (inputHeight N : ℝ) / inputHeight N)
      atTop (𝓝 0) := by
…
```
Mentions: OAI.EditApproximation.coarseExponent, OAI.EditApproximation.inputSmallLog, OAI.EditApproximation.computedDependencyIndexCount, OAI.EditApproximation.inputHeight
def OAI.EditApproximation.computedMaxTreeDepth line 214
theorem OAI.EditApproximation.intervalTreeDepth_le_computedMax line 216
theorem OAI.EditApproximation.tree_logSmallLog_div_height_tendsto line 222
Source documentation
A uniform depth upper bound is obtained by using the total length as the source length.
```
theorem tree_logSmallLog_div_height_tendsto :
    Tendsto (fun N => (computedMaxTreeDepth N : ℝ) *
      Real.log (inputSmallLog N : ℝ) / inputHeight N) atTop (𝓝 0) := by
…
```
Mentions: OAI.EditApproximation.computedMaxTreeDepth, OAI.EditApproximation.inputSmallLog, OAI.EditApproximation.inputHeight
theorem OAI.EditApproximation.tree_depth_div_height_tendsto line 247
theorem OAI.EditApproximation.dependency_index_div_height_tendsto line 256
def OAI.EditApproximation.computedDependencyOverheadExponent line 271
theorem OAI.EditApproximation.computedDependencyOverheadExponent_tendsto line 279
Source documentation
Every fixed choice of the two branching-budget constants yields a sublinear logarithmic overhead in the dependency-path bound.
```
theorem computedDependencyOverheadExponent_tendsto (C₁ C₂ : ℝ) :
    Tendsto (fun N => computedDependencyOverheadExponent C₁ C₂ N / inputHeight N)
      atTop (𝓝 0) := by
…
```
Mentions: OAI.EditApproximation.computedDependencyOverheadExponent, OAI.EditApproximation.inputHeight