OAI/Combinatorics/EditApproximation/Refinement/ComputedRefinementReadBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual refinement query, including the reads used to construct its initial and mass data, satisfies the two dependency branching budgets. Only nonnegativity of the actual initial query value is used.

  1. theorem OAI.EditApproximation.computed_data_support_budget line 13
  2. theorem OAI.EditApproximation.computed_physicalRefinement_current_reads line 69
  3. theorem OAI.EditApproximation.computed_physicalRefinement_earlier_reads line 109