OAI/Combinatorics/EditApproximation/Refinement/PhysicalRefinementReadWork.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Split the literal recursive reads by the unified table index. The current-index reads are physical-child requests; initial data, warmup mass and old history have strictly smaller indices.

  1. def OAI.EditApproximation.physicalCurrentReadWeight line 12
  2. def OAI.EditApproximation.physicalEarlierReadWeight line 15
  3. theorem OAI.EditApproximation.physicalRefinementWarmupRead_cost_current line 18
  4. theorem OAI.EditApproximation.physicalRefinementWarmupRead_cost_earlier line 28
  5. theorem OAI.EditApproximation.physicalRefinementMassQuery_cost_current line 38
  6. theorem OAI.EditApproximation.physicalRefinementMassQuery_cost_earlier line 47
  7. theorem OAI.EditApproximation.physicalRefinementCurrentQuery_cost_current line 57
  8. theorem OAI.EditApproximation.physicalRefinementCurrentQuery_cost_earlier line 65
  9. theorem OAI.EditApproximation.physicalRefinementEarlierQuery_cost_current line 73
  10. theorem OAI.EditApproximation.physicalRefinementEarlierQuery_cost_earlier line 85
  11. def OAI.EditApproximation.physicalReadMaskedAnswers line 97
  12. theorem OAI.EditApproximation.physicalRefinementDataRequest_cost_le line 140
  13. theorem OAI.EditApproximation.physicalRefinementDataRequest_current_reads line 165
  14. theorem OAI.EditApproximation.physicalRefinementDataRequest_earlier_reads line 180
  15. theorem OAI.EditApproximation.physicalRefinementWarmupRead_keys_bounded line 201
  16. theorem OAI.EditApproximation.physicalRefinementDataRequest_keys_bounded line 214