OAI/Combinatorics/EditApproximation/Geometry/ChargedIndexCost.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The charged request index distinguishes previous passes and coarse leaves. For internal refinement its two index classes are exactly the current and earlier table-read counters.

  1. def OAI.EditApproximation.chargedSameWeight line 11
  2. def OAI.EditApproximation.chargedEarlierWeight line 15
  3. theorem OAI.EditApproximation.chargedSameWeight_table line 19
  4. theorem OAI.EditApproximation.chargedEarlierWeight_table line 27
  5. theorem OAI.EditApproximation.chargedGlobalQuery_current_cost line 50
  6. theorem OAI.EditApproximation.chargedGlobalQuery_earlier_cost line 79