OAI/Analysis/CircleDomains/Topology/CompactPriorityTest.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual priority coordinate gives a compact admissible source test. Its classical differential on the cutoff plateau is the original one.

  1. theorem OAI.CircleDomainRigidity.fderiv_cutoff_one_on line 13
  2. theorem OAI.CircleDomainRigidity.CompactScalarModel.compact_priority_test line 24