OAI/Analysis/CircleDomains/Sobolev/ShrinkingOccupationEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Mean occupation has no mass off the physical domain. Its square density therefore has vanishing energy on collars shrinking to a dust fibre.

  1. theorem OAI.CircleDomainRigidity.square_density_null_of_density_null line 15
  2. theorem OAI.CircleDomainRigidity.meanCodeOccupation_compl line 32
  3. theorem OAI.CircleDomainRigidity.tendsto_shrinking_occupation_energy line 41