OAI/Combinatorics/EditApproximation/Queries/QueryProgramWidth.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Intermediate output widths for the executed adaptive refinement. These bounds concern the words produced before memo-table normalization.

  1. theorem OAI.EditApproximation.queryLocalRefinement_width line 29
  2. theorem OAI.EditApproximation.queryLocalRandomSources_width line 87
  3. theorem OAI.EditApproximation.queryLocalBand_width line 126
  4. theorem OAI.EditApproximation.queryLocalProgram_width line 165