OAI/Analysis/CircleDomains/Modulus/FilledFirstArrivalBarrier.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The first-arrival barrier can be chosen equal to one throughout a closed terminal collar while retaining its path inequality and all dust-band bounds.

  1. theorem OAI.CircleDomainRigidity.exists_filled_first_arrival_barrier_potential line 21