OAI/Combinatorics/EditApproximation/Refinement/PhysicalCoarseSeedLaw.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The clamped incoming seed table is the image of the actual complete coarse sampler. Its simultaneous initial accuracy is a derived fact.

  1. def OAI.EditApproximation.physicalCoarseSeedLaw line 28
  2. instance OAI.EditApproximation.physicalCoarseSeedLaw_probability line 35
  3. theorem OAI.EditApproximation.physicalCoarseSeedLaw_failure line 40