OAI/Analysis/CircleDomains/Rigidity/ExactTraceTests.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Actual smooth replacements of the original scalar tests. Their full boundary traces, continuous representatives and global Sobolev errors are retained together for the circle-model construction.

  1. structure OAI.CircleDomainRigidity.ExactTraceTest line 16
  2. theorem OAI.CircleDomainRigidity.exists_exact_trace_test line 30
  3. theorem OAI.CircleDomainRigidity.ExactTraceTest.trace_on_sphere line 70