OAI/Combinatorics/EditApproximation/Refinement/ComputedChargedQueryBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform edge budgets for the actual charged global interpreter. The bounds hold for every initial seed and every draw, including failed approximation events.

  1. theorem OAI.EditApproximation.computed_chargedGlobalQuery_current_reads line 28
  2. theorem OAI.EditApproximation.computed_chargedGlobalQuery_earlier_reads line 71