OAI/Analysis/CircleDomains/Sobolev/ScaledCutoffEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Dirichlet energy of a smooth planar cutoff is unchanged by dilation. This supplies the fixed energy budget for disjoint concentric transition annuli used to make cutoffs of arbitrarily small energy.

  1. def OAI.CircleDomainRigidity.dilatedCutoff line 15
  2. theorem OAI.CircleDomainRigidity.dilatedCutoff_smooth line 17
  3. theorem OAI.CircleDomainRigidity.dilatedCutoff_compact line 20
  4. theorem OAI.CircleDomainRigidity.dilatedCutoff_fderiv line 25
  5. theorem OAI.CircleDomainRigidity.smooth_cutoff_energy_integrable line 33
  6. theorem OAI.CircleDomainRigidity.dilatedCutoff_energy line 46