OAI/Analysis/CircleDomains/Topology/AnnularCutoffs.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Concentric smooth cutoffs whose transition annuli are disjoint. Each dilation has the same Dirichlet energy in dimension two.

  1. def OAI.CircleDomainRigidity.unitAnnularCutoff line 12
  2. theorem OAI.CircleDomainRigidity.dilated_unitCutoff_one line 14
  3. theorem OAI.CircleDomainRigidity.dilated_unitCutoff_support line 21
  4. theorem OAI.CircleDomainRigidity.dilated_unitCutoff_derivative_annulus line 31
  5. theorem OAI.CircleDomainRigidity.separated_dilatedCutoff_derivatives line 52