OAI/Analysis/CircleDomains/Rigidity/AxialLineDifferentiation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The derivative of either target coordinate along a unit source axis is bounded by the complex derivative norm.

  1. theorem OAI.CircleDomainRigidity.complexCoordinateLine_contDiff line 13
  2. theorem OAI.CircleDomainRigidity.complexCoordinateLine_hasDerivAt line 17
  3. theorem OAI.CircleDomainRigidity.axial_complex_deriv line 25
  4. theorem OAI.CircleDomainRigidity.axial_coordinate_deriv_le line 35