OAI/Combinatorics/EditApproximation/Refinement/PhysicalGlobalValue.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The global query body computes the local pass recurrence on every seed and draw.

  1. theorem OAI.EditApproximation.physicalGlobalQuery_warmup line 19
  2. theorem OAI.EditApproximation.physicalGlobalQuery_refinement_value line 30
  3. theorem OAI.EditApproximation.globalSeedRead_value line 50
  4. theorem OAI.EditApproximation.localRequestValue_initial line 71
  5. theorem OAI.EditApproximation.localRequestValue_mass line 82
  6. theorem OAI.EditApproximation.localPassValue_step line 97
  7. theorem OAI.EditApproximation.physicalRefinementDataRequestQuery_localValue line 129
  8. theorem OAI.EditApproximation.physicalGlobalQuery_value line 155
  9. theorem OAI.EditApproximation.physicalGlobalProgramValue line 235