OAI/Analysis/CircleDomains/Sobolev/CircleDifferentialClosed.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The intrinsic differential of a smooth circle coordinate is closed. The proof uses actual local real branches and symmetry of their Hessians.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.circleFDeriv_partial_commute line 16
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.circleFDeriv_closed_complex line 43