OAI/Analysis/CircleDomains/Sobolev/LocalizedSobolevRange.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A range bound on the smooth region propagates across the set where the weak gradient is zero. Cutoff transitions lie in the smooth region.

  1. theorem OAI.CircleDomainRigidity.localized_sobolev_range line 13