OAI/Combinatorics/EditApproximation/Refinement/ComputedChargedRandomBudget.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_chargedRandomGlobalQuery_current_reads line 42
  2. theorem OAI.EditApproximation.computed_chargedRandomGlobalQuery_earlier_reads line 98