OAI/Analysis/CircleDomains/Sobolev/ScalarRegularCoordinates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual scalar coordinate maps with transverse real or imaginary coordinate. Their Jacobians are the corresponding nonzero scalar partials.

  1. lemma OAI.CircleDomainRigidity.planar_linear_isInvertible_of_det_ne_zero line 13
  2. def OAI.CircleDomainRigidity.scalarLevelCoordinate line 20
  3. def OAI.CircleDomainRigidity.scalarLevelDifferential line 23
  4. lemma OAI.CircleDomainRigidity.scalarLevelCoordinate_re line 26
  5. lemma OAI.CircleDomainRigidity.hasFDerivAt_scalarLevelCoordinate line 30
  6. lemma OAI.CircleDomainRigidity.scalarLevelDifferential_det line 36
  7. lemma OAI.CircleDomainRigidity.scalarLevelCoordinate_im_isInvertible line 41
  8. lemma OAI.CircleDomainRigidity.scalarLevelCoordinate_re_isInvertible line 49
  9. lemma OAI.CircleDomainRigidity.scalar_regular_im_weighted_coarea line 57
  10. lemma OAI.CircleDomainRigidity.scalar_regular_re_weighted_coarea line 66