OAI/Analysis/CircleDomains/Sobolev/LocalComplexJacobianForm.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Local smooth Jacobian one-forms, on the actual open set where a map is smooth. Their curl is the determinant of its real differential.

  1. lemma OAI.CircleDomainRigidity.smooth_complex_partial_commute_at line 12
  2. lemma OAI.CircleDomainRigidity.smooth_complex_partial_on line 23
  3. lemma OAI.CircleDomainRigidity.smooth_complex_jacobian_curl line 30
  4. lemma OAI.CircleDomainRigidity.holomorphic_real_jacobian line 45