OAI/Combinatorics/EditApproximation/Geometry/LocalTraceMemoOutput.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The bounded-key adaptive trace drives the actual charged memo program. Its final root query has the same distribution as the local answer. The program uses all previous-pass copies from the trace and one fresh terminal copy.

  1. abbrev OAI.EditApproximation.LocalTraceFinalOutcome line 32
  2. def OAI.EditApproximation.localTraceAppendFinal line 36
  3. def OAI.EditApproximation.localTraceMemoResult line 43
  4. def OAI.EditApproximation.localTraceFinalProjection line 53
  5. theorem OAI.EditApproximation.localTraceMemoResult_value line 59
  6. def OAI.EditApproximation.localTraceMemoAnswer line 90
  7. theorem OAI.EditApproximation.localTraceMemoAnswer_eq line 96
  8. def OAI.EditApproximation.localTraceFinalLaw line 104
  9. instance OAI.EditApproximation.localTraceFinalLaw_probability line 110
  10. theorem OAI.EditApproximation.localTraceFinalLaw_map line 115
  11. theorem OAI.EditApproximation.localTraceMemoAnswer_event line 134