OAI/Analysis/CircleDomains/Sobolev/PotentialCutoffSmoothing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Positive smooth approximation of compactly localized pieces of the actual barrier, with convergence of both weak gradient components.

  1. theorem OAI.CircleDomainRigidity.potential_cutoff_positive_approx line 22