OAI/Analysis/CircleDomains/Rigidity/ProjectedZeroTrace.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The zero-trace error for a retained circle model has an actual global Sobolev continuation with zero complementary gradient.

  1. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.projectedPlaneFunction_zero_trace_witness line 20