OAI/Analysis/CircleDomains/Modulus/PriorBarrierConstruction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The compatible barrier theorem with the enlarged flags and the full controlled size, constructed from the actual first-arrival cost bound.

  1. theorem OAI.CircleDomainRigidity.exists_controlled_compatible_level_barrier line 21