OAI/Analysis/CircleDomains/Probability/GatedRecursiveLaw.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Failure of a small compatible real barrier constructs the recursive law with the prescribed collar gates and actual prior-law presentation. The code space is Borel because the gates are closed on their contours.

  1. theorem OAI.CircleDomainRigidity.exists_gated_recursive_law_of_no_small_barrier line 19