OAI/Combinatorics/EditApproximation/Probability/AdaptiveSeedTrace.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Preserve the finite draw history of adaptive seed passes. The final seed has exactly the existing sequential law, while the history remains available to the lazy evaluator when it asks for an earlier pass.

  1. def OAI.EditApproximation.AdaptiveSeedTrace line 13
  2. instance OAI.EditApproximation.adaptiveSeedTraceFintype line 17
  3. instance OAI.EditApproximation.adaptiveSeedTraceMeasurable line 25
  4. instance OAI.EditApproximation.adaptiveSeedTraceSingleton line 33
  5. def OAI.EditApproximation.adaptiveTraceValue line 54
  6. def OAI.EditApproximation.adaptiveTraceLaw line 60
  7. instance OAI.EditApproximation.adaptiveTraceLaw_probability line 64
  8. theorem OAI.EditApproximation.adaptiveTraceLaw_map line 74