OAI/Analysis/CircleDomains/Rigidity/GlobalSmoothMatchedMasks.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every compact smooth target test has an actual countable family of global Sobolev masks. The scalar, its energy, the open domain and the removable residual dust have all been constructed.

  1. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.exists_global_smooth_masks line 23