OAI/Analysis/CircleDomains/Sobolev/LocalScalarEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Small open neighborhoods of countably many values for the actual finite-energy scalar on an arbitrary open source domain.

  1. theorem OAI.CircleDomainRigidity.local_scalar_energy_nullSingleton line 13
  2. theorem OAI.CircleDomainRigidity.exists_small_open_local_energy_cover line 30