OAI/Analysis/CircleDomains/Sobolev/SmallEnergyCutoff.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Smooth planar cutoffs with arbitrarily small Dirichlet energy, constructed by averaging disjoint concentric transition annuli.

  1. def OAI.CircleDomainRigidity.annularAverage line 13
  2. theorem OAI.CircleDomainRigidity.annularAverage_smooth line 16
  3. theorem OAI.CircleDomainRigidity.annularAverage_compact line 19
  4. theorem OAI.CircleDomainRigidity.annularAverage_mem_unit line 24
  5. theorem OAI.CircleDomainRigidity.annularAverage_one line 28
  6. theorem OAI.CircleDomainRigidity.annularAverage_tsupport line 35
  7. theorem OAI.CircleDomainRigidity.annularAverage_energy line 61
  8. theorem OAI.CircleDomainRigidity.exists_small_energy_cutoff_zero line 72