OAI/Analysis/CircleDomains/Transfer/ModelAppendedTests.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite appended list consists of actual continuous compact tests with local Sobolev witnesses and all pair-null relations. Its ingredients are the constructed flattenings, priority cutoffs and descended height.

  1. theorem OAI.CircleDomainRigidity.CompactScalarModel.compact_appended_tests line 17