OAI/Analysis/CircleDomains/Sobolev/PrioritySmooth.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The priority formula is smooth off the closed source dust because its shrinking cutoff supports have a common locally vanishing tail.

  1. theorem OAI.CircleDomainRigidity.priorityBlend_contDiffAt line 14
  2. theorem OAI.CircleDomainRigidity.priorityInfiniteValue_contDiffAt line 24
  3. theorem OAI.CircleDomainRigidity.priorityInfiniteValue_smooth_off_dust line 38