OAI/Combinatorics/EditApproximation/Queries/QueryDependencyCosts.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Weighted read counts are the actual same-index and earlier-index lengths used by the dependency expansion, after identifying its values with the local mathematical recurrence.

  1. theorem OAI.EditApproximation.list_filter_length_eq_sum line 12
  2. theorem OAI.EditApproximation.queryRequestList_expected line 29
  3. theorem OAI.EditApproximation.querySameRequests_length_eq_cost line 35
  4. theorem OAI.EditApproximation.queryEarlierRequests_length_eq_cost line 44