ChargedQueryAsymptotics.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Almost-linear bounds for the executed request tree. These count requests and depth-weighted source widths, independently of accuracy events. Local arithmetic and random-source costs are separate obligations.

theorem OAI.EditApproximation.DependencyExpansion.nodeCount_le_depthWeightedCount line 16
theorem OAI.EditApproximation.DependencyExpansion.nodeCount_le_widthWork line 24
theorem OAI.EditApproximation.computed_width_prefactor_le line 32
Source documentation
The deterministic balanced-tree prefactor is only N times a fixed polynomial in the logarithmic height.
```
theorem computed_width_prefactor_le (N n : ℕ) (hN : 0 < N) (hn : n ≤ N)
    (hell : 200 ≤ inputSmallLog N) (hH : 105 ≤ inputHeight N) :
    (intervalTreeDepth (integerParameters N).M n + 1) * n +
      4 * (integerParameters N).M * max 1 n ≤ (N + 2) * inputHeight N ^ 2 := by
…
```
Mentions: OAI.EditApproximation.inputSmallLog, OAI.EditApproximation.inputHeight, OAI.EditApproximation.intervalTreeDepth, OAI.EditApproximation.integerParameters

theorem OAI.EditApproximation.computed_weighted_widthWork_near_linear line 55

Source documentation

Fixed height-polynomial overheads can be included in the executed width-work estimate without changing its almost-linear exponent.

theorem computed_weighted_widthWork_near_linear (C : ℕ) (epsilon : ℝ)
    (hepsilon : 0 < epsilon) :
    ∀ᶠ N in atTop, ∀ n ≤ N, ∀ tree : DependencyExpansion,
      tree.Valid ((integerParameters N).M * inputSmallLog N ^ 257)
        (inputHeight N ^ (512 * (coarseExponent (inputSmallLog N) + 1))) →
      tree.depth = intervalTreeDepth (integerParameters N).M n →
      tree.rank ≤ computedDependencyIndexCount N →
      (tree.widthWork (integerParameters N).M n : ℝ) * (inputHeight N : ℝ) ^ C ≤
        (N + 2 : ℝ) ^ (1 + epsilon) := by
…

Mentions: OAI.EditApproximation.DependencyExpansion, OAI.EditApproximation.integerParameters, OAI.EditApproximation.inputSmallLog, OAI.EditApproximation.inputHeight, OAI.EditApproximation.coarseExponent, OAI.EditApproximation.intervalTreeDepth, OAI.EditApproximation.computedDependencyIndexCount

theorem OAI.EditApproximation.chargedMemoEvaluate_requests_le_widthWork line 126

Source documentation

The instrumented memo evaluator makes no more requests than there are nodes in its exact uncached expansion.

theorem chargedMemoEvaluate_requests_le_widthWork (hM : 1 ≤ M)
    (root : ChargedPhysicalRequest M J target.length passes copies T S) :
    (chargedMemoEvaluate source target N P (inputSmallLog N) (40 * smallLogExponent N)
      H (inputSmallLog N ^ 80) T S passes copies factor multiplier tau eta kappa delta
      group integer initial root).requests ≤
      (chargedDependencyTree source target N P H T S passes copies factor multiplier
        tau eta kappa delta group integer initial root).widthWork M source.length := by
…

Mentions: OAI.EditApproximation.ChargedPhysicalRequest, OAI.EditApproximation.chargedMemoEvaluate, OAI.EditApproximation.inputSmallLog, OAI.EditApproximation.smallLogExponent, OAI.EditApproximation.chargedDependencyTree

theorem OAI.EditApproximation.chargedDependencyTree_depth line 145
theorem OAI.EditApproximation.chargedDependencyTree_index_le line 153