OAI/Analysis/CircleDomains/Sobolev/PhysicalCauchyRiemann.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The real Cauchy–Riemann equations in the actual physical plane coordinates imply complex differentiability.

  1. theorem OAI.CircleDomainRigidity.differentiableAt_complex_of_real_linear line 12
  2. def OAI.CircleDomainRigidity.complexifyPair line 27
  3. theorem OAI.CircleDomainRigidity.complexifyPair_differentiableAt line 30