OAI/Analysis/CircleDomains/Transfer/RetainedOriginalTest.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Add the constructed zero-trace error back to a retained smooth test. The result is the continuation of the original test on the same model.

  1. theorem OAI.CircleDomainRigidity.sphereFromPlaneFunction_sub line 19
  2. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.original_test_witness line 29