OAI/Analysis/CircleDomains/Sobolev/ModelPriorityWeakError.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Transfer the selected priority error to the actual compact source Sobolev witness. On the working disk the source cutoff is one.

  1. theorem OAI.CircleDomainRigidity.CompactScalarModel.priority_weak_error line 16