OAI/Analysis/CircleDomains/Sobolev/DustSobolevExtension.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compact continuous Sobolev functions extend across removable dust. The approximate global gradients come from the actual recursive finite models, and a second weak limit removes the approximation error.

  1. theorem OAI.CircleDomainRigidity.dust_sobolev_extension_of_published_inputs line 19