OAI/NumberTheory/Ostmann/Arithmetic/MovingRootBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingNodeGuard_cost line 10
2. theorem OAI.Ostmann.MovingSlotData.formulaNodes_cost line 18
3. theorem OAI.Ostmann.movingTopRootCuts_card line 57

   Source documentation

   A uniform explicit bound for the number of real arithmetic cut points. It is independent of the values of both top giants and of the prime cutoffs.

   theorem movingTopRootCuts_card {σ : Type*} (value : σ → ℕ)
       (hvalue : ∀ i, value i ≠ 0) (childBound pivotBound : ℕ → ℕ) {n : ℕ}
       (T : MovingSlotData σ n) (hf : T.Frequencies (· ≠ 0)) (XR : ℕ) :
       (movingTopRootCuts value hvalue childBound pivotBound T hf XR).card ≤
         (2 ^ n - 1) * (3 * (7 * 2 ^ n)) := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingTopRootCuts