OAI/Analysis/CircleDomains/Sobolev/LocalSmoothPartition.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compact smooth partition functions on an open planar domain. The family is locally finite in the domain, allowing accumulation at its boundary.

  1. structure OAI.CircleDomainRigidity.OpenPlanePartition line 16
  2. theorem OAI.CircleDomainRigidity.exists_openPlanePartition line 26