OAI/Combinatorics/EditApproximation/Geometry/RefinementSupportBudget.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Cardinality of the actual raw initial-data and band-data lists. The counts apply before any good-seed event and include rejected candidates.

  1. theorem OAI.EditApproximation.list_eraseDups_length_le line 11
  2. theorem OAI.EditApproximation.rawRefinementCenters_length line 24
  3. theorem OAI.EditApproximation.cellTargetStates_length_dyadic line 40
  4. theorem OAI.EditApproximation.refinementInitialSupport_length line 57
  5. theorem OAI.EditApproximation.wideWarmupInputs_length line 79
  6. theorem OAI.EditApproximation.refinementBandInputList_length line 98