OAI/Analysis/CircleDomains/Sobolev/FilledSmoothBarrier.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual compatible smooth barrier from the first-arrival obstruction. The norm outside the penalty region depends only on the original density; the perturbation is used solely to obtain the plateaus and path inequality.

  1. theorem OAI.CircleDomainRigidity.exists_compatible_smooth_first_arrival_barrier line 23