OAI/Analysis/CircleDomains/Sobolev/ScalarEnergyMeasure.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The pushforward of scalar Dirichlet energy has no atoms. This is applied on the whole support of an old test, or on the fixed bounded region used for the height.

  1. def OAI.CircleDomainRigidity.scalarEnergyMeasure line 15
  2. theorem OAI.CircleDomainRigidity.scalarEnergyMeasure_finite line 19
  3. theorem OAI.CircleDomainRigidity.scalarEnergyMeasure_nullSingleton line 29
  4. theorem OAI.CircleDomainRigidity.exists_small_open_energy_cover line 47