OAI/Analysis/CircleDomains/Sobolev/SmoothExteriorReplacement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A local Sobolev scalar smooth off a compact set can be replaced by a smooth scalar without changing it near an exterior boundary. The removed part is an actual compactly supported global Sobolev function.

  1. theorem OAI.CircleDomainRigidity.exists_smooth_exterior_replacement line 14