OAI/Combinatorics/EditApproximation/Refinement/PhysicalFamilyRuntime.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The source family is the projection of terminating rejection-sampling executions.

  1. def OAI.EditApproximation.physicalFamilyRuntimeLaw line 31
  2. instance OAI.EditApproximation.physicalFamilyRuntimeLaw_probability line 35
  3. theorem OAI.EditApproximation.physicalFamilyRuntimeAccepted_law line 44
  4. def OAI.EditApproximation.physicalFamilyRuntimeAnswer line 54
  5. theorem OAI.EditApproximation.physicalFamilyRuntimeAnswer_event line 62