OAI/Analysis/CircleDomains/Probability/LastEntryCircleLaw.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact probabilities of the collar arc events used in alternation.

  1. def OAI.CircleDomainRigidity.lastEntryCircleLaw line 18
  2. theorem OAI.CircleDomainRigidity.lastEntryCircleLaw_apply line 23
  3. theorem OAI.CircleDomainRigidity.lastEntryCircleLaw_nullSingletonClass line 37