OAI/Combinatorics/EditApproximation/Geometry/CommonSeedTrace.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Adaptive seed passes driven by common per-pass random sources. The trace stores one source for the actual pass, with no seed-indexed family. Its returned seed has the original adaptive law.

  1. def OAI.EditApproximation.CommonSeedTrace line 13
  2. instance OAI.EditApproximation.commonSeedTraceFintype line 17
  3. instance OAI.EditApproximation.commonSeedTraceMeasurable line 24
  4. instance OAI.EditApproximation.commonSeedTraceSingleton line 32
  5. def OAI.EditApproximation.commonTraceValue line 56
  6. def OAI.EditApproximation.commonTraceLaw line 62
  7. instance OAI.EditApproximation.commonTraceLaw_probability line 67
  8. theorem OAI.EditApproximation.commonTraceLaw_map line 76