OAI/Combinatorics/EditApproximation/Geometry/LocalTraceProgram.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Extract the actual per-pass streams from a finite adaptive draw trace. Earlier-pass streams are preserved when a new draw is appended, and the lazy program's seed recurrence is exactly the trace's returned table.

  1. theorem OAI.EditApproximation.localSeedSequence_streams_congr line 13
  2. abbrev OAI.EditApproximation.LocalScheduledTrace line 46
  3. def OAI.EditApproximation.localTraceSeed line 49
  4. theorem OAI.EditApproximation.localTraceSeed_succ line 53
  5. def OAI.EditApproximation.localTraceInitial line 60
  6. def OAI.EditApproximation.localTraceGroup line 64
  7. def OAI.EditApproximation.localTraceInteger line 77
  8. theorem OAI.EditApproximation.localTraceGroup_before line 92
  9. theorem OAI.EditApproximation.localTraceInteger_before line 100
  10. theorem OAI.EditApproximation.localTracePassValue line 108
  11. theorem OAI.EditApproximation.localTraceSeed_eq line 125
  12. theorem OAI.EditApproximation.localTraceSeed_before line 164
  13. instance OAI.EditApproximation.localScheduledTrace_measurableSingleton line 185