OAI/Analysis/CircleDomains/Modulus/SavedBarrierMargins.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Strict plateau and zero margins for the saved source barriers. Uniformly small coordinate changes preserve the exact barrier values.

  1. theorem OAI.CircleDomainRigidity.saved_barrier_values_stable line 12
  2. theorem OAI.CircleDomainRigidity.saved_barrier_one_on_neighborhood line 34