OAI/Analysis/CircleDomains/Sobolev/ScalarSobolevLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The constructed scalar limit is Sobolev on every planar region of finite area, including across the finite-model holes.

  1. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.ScalarWeakLimit.memW1p_on line 22