OAI/Combinatorics/EditApproximation/Refinement/ComputedCoarseBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Polynomial coarse-sampling budgets for the computed dimensions.

  1. def OAI.EditApproximation.SymbolicComputedCoarseBudget line 25
  2. theorem OAI.EditApproximation.symbolicComputedCoarseWork_expected_le line 31
  3. theorem OAI.EditApproximation.symbolicComputedCoarseBudget_mono line 84