OAI/Analysis/CircleDomains/Sobolev/ScalarLocalLp.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The scalar weak limit is locally planar L², including on arbitrary compact regions that meet limiting complementary components.

  1. theorem OAI.CircleDomainRigidity.planarVolume_absolutelyContinuous_sphericalArea line 13
  2. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.ScalarWeakLimit.scalar_unit_spherical line 29
  3. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.ScalarWeakLimit.scalar_unit line 34
  4. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.ScalarWeakLimit.scalar_aestronglyMeasurable line 37
  5. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.ScalarWeakLimit.scalar_memLp_on line 40