OAI/Analysis/CircleDomains/Sobolev/RetainedSobolevContinuations.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual Sobolev continuations of the retained smooth scalar tests. The exterior coefficient area theorem controls the weak limits.

  1. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.exists_continuation_witness line 19
  2. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.continuedScalar_memW1p line 37