OAI/Combinatorics/EditApproximation/Geometry/ChargedRandomMemoWork.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Source reads and dictionary visits in the actual shared-cache evaluator are bounded by the width of its projected table dependency expansion.

  1. theorem OAI.EditApproximation.chargedRandomMemoEvaluate_requests_le_widthWork line 53
  2. theorem OAI.EditApproximation.chargedRandomMemoEvaluate_dictionaryVisits_le_widthWork line 80