OAI/Analysis/CircleDomains/Sobolev/SmoothedBarrierPlateaus.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Apply the smoothing construction to the actual anchor and terminal constant regions, choosing the averaging neighborhoods and compact exterior.

  1. theorem OAI.CircleDomainRigidity.smooth_barrier_with_anchor_and_terminal line 18