OAI/Analysis/CircleDomains/Rigidity/MatchedMaskGlobalSobolev.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The constructed matched masks extend across their actual residual removable dust. All conditional inputs are exactly those of the proved dust Sobolev theorem; no trace or extension conclusion is assumed.

  1. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRealMask.global_sobolev_of_published_inputs line 22