OAI/Combinatorics/EditApproximation/Refinement/PhysicalWarmupQuery.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Adaptive finite queries for the literal local initial cones and warmup. Candidate lists are bounded local grid lists; no full target domain is tabulated.

  1. theorem OAI.EditApproximation.FiniteQuery.bind_value line 19
  2. theorem OAI.EditApproximation.FiniteQuery.collect_value line 28
  3. theorem OAI.EditApproximation.finiteAnswerTable_map line 42
  4. theorem OAI.EditApproximation.localInitialConeCenters_raw line 57
  5. theorem OAI.EditApproximation.localInitialConeCenters_congr_raw line 64
  6. theorem OAI.EditApproximation.localInitialConeTable_congr_raw line 76
  7. theorem OAI.EditApproximation.physicalInitialQuery_value line 95
  8. theorem OAI.EditApproximation.PhysicalTableRequest.combinedRank_lt_of_progress line 126
  9. theorem OAI.EditApproximation.PhysicalTableRequest.combinedRank_sameIndexChild line 136
  10. theorem OAI.EditApproximation.PhysicalTableRequest.combinedRank_previous_pass line 141
  11. theorem OAI.EditApproximation.PhysicalTableRequest.combinedRank_warmup_child line 148