OAI/Analysis/CircleDomains/Modulus/NormalizedArgumentBasic.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Elementary argument in turns on the punctured complex plane.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.normalizedArgument line 11
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.normalizedArgument_eq line 14
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.continuousAt_normalizedArgument line 20
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.normalizedArgument_mul line 25
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.normalizedArgument_neg line 33