OAI/Combinatorics/EditApproximation/Refinement/ComputedEarlierInputBudget.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual earlier-input cover satisfies the polynomial branching budget at every seed, after substituting the computed time and grid parameters.

  1. theorem OAI.EditApproximation.computed_smallLog_le_height line 12
  2. theorem OAI.EditApproximation.computed_history_budget_le_height_sq line 19
  3. theorem OAI.EditApproximation.computed_window_le_height_cube line 30
  4. theorem OAI.EditApproximation.computed_cell_budget_le_height_pow line 39
  5. theorem OAI.EditApproximation.computed_queryEarlierInputCover_card line 54

    Source documentation

    Every literal earlier-input request lies in a cover of cardinality H^(256(p+1)). The only value premise is nonnegativity of the actual initial query value; no good-seed event is required.

    theorem computed_queryEarlierInputCover_card {nx ny : ℕ}
    (parent : TargetInterval nx) (N P : ℕ) (hN : 0 < N)
    (hell : 200 ≤ inputSmallLog N) (hPeq : P = (integerParameters N).P)
    (A : ℚ) (hA : A ≤ ((integerParameters N).initialFactor : ℚ))
    (initial : TargetInterval ny → ℚ) (q : TargetInterval ny) (hw : 0 ≤ initial q) :
    (queryEarlierInputCover (M := (integerParameters N).M) parent N P (inputSmallLog N)
…

    Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.inputSmallLog, OAI.EditApproximation.integerParameters, OAI.EditApproximation.queryEarlierInputCover