OAI/Combinatorics/EditApproximation/Refinement/ComputedQueryReadBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.computedQueryReadDegree line 10

   Source documentation

   Degree contributed by guards, physical means, and scalar-source reads.

   def computedQueryReadDegree (K : ℕ) : ℕ := (K + 1) * queryCallbackShellDegree

   Mentions: OAI.EditApproximation.queryCallbackShellDegree

2. theorem OAI.EditApproximation.computedQueryReadBudget_cap line 12