OAI/Analysis/CircleDomains/Sobolev/PhysicalMeanIndexSobolev.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The locally lifted geometric mean has actual L² weak derivatives. Both ACL directions follow from physical occupation and published coarea; boundedness follows from the compact family of lifted terminal rays.

  1. theorem OAI.CircleDomainRigidity.sliceChartDensity_memLp_rectangle line 25
  2. theorem OAI.CircleDomainRigidity.physicalMeanIndex_rectangle_weak_gradient line 36