OAI/Combinatorics/EditApproximation/Geometry/LocalCommonSeed.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Concrete common-source seed passes. The sampler range cap is proved for every seed; no good-seed event is used to define or bound the draws.

  1. abbrev OAI.EditApproximation.LocalCommonDraw line 27
  2. def OAI.EditApproximation.localCommonDrawLaw line 30
  3. instance OAI.EditApproximation.localCommonDrawLaw_probability line 35
  4. def OAI.EditApproximation.localCommonSample line 40
  5. theorem OAI.EditApproximation.localCommonSample_law line 49
  6. abbrev OAI.EditApproximation.LocalCommonTrace line 68
  7. instance OAI.EditApproximation.localCommonTraceFintype line 71
  8. instance OAI.EditApproximation.localCommonTraceSingleton line 77
  9. def OAI.EditApproximation.localCommonSeed line 83
  10. def OAI.EditApproximation.localCommonTraceLaw line 88
  11. instance OAI.EditApproximation.localCommonTraceLaw_probability line 92
  12. theorem OAI.EditApproximation.localCommonSeed_law line 99