OAI/Analysis/CircleDomains/Sobolev/ScalarWeakLimits.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A common subsequence of the actual finite scalar fillings and their two differentials. The scalar is bounded in spherical L²; the differentials are bounded in ordinary planar L².

  1. def OAI.CircleDomainRigidity.planarSphericalArea line 16
  2. instance OAI.CircleDomainRigidity.finitePlanarSphericalArea line 19
  3. instance OAI.CircleDomainRigidity.separablePlanarSphericalArea line 22
  4. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.exists_filled_weak_limits line 33