OAI/Combinatorics/EditApproximation/Refinement/PhysicalQueryBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The literal online loop is bounded by the applicable scale window, which is polynomial in ell throughout the computed factor schedule.

  1. theorem OAI.EditApproximation.refinement_query_window_length line 13
  2. theorem OAI.EditApproximation.physicalProgramOnline_query_indices_window line 41
  3. theorem OAI.EditApproximation.physicalProgramOnline_length_window line 70