OAI/Analysis/CircleDomains/Transfer/ScalarModelLinearRecovery.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Linear recovery of original signed tests from bounded retained tests preserves the same circle model and zero complementary gradients.

  1. theorem OAI.CircleDomainRigidity.sphereFromPlaneFunction_linear_difference line 14
  2. def OAI.CircleDomainRigidity.CompactScalarCircleModel.linearDifference line 23