OAI/Analysis/CircleDomains/Rigidity/ConductivityExterior.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The constructed principal conductivity homeomorphism is holomorphic off its coefficient support. Its principal Laurent germ and uniform exterior decay follow from the proved local Weyl lemma.

  1. theorem OAI.CircleDomainRigidity.PlaneLocalWeakComplex.conductivity_holomorphic_off line 16
  2. theorem OAI.CircleDomainRigidity.exists_principal_conductivity_holomorphic line 32
  3. theorem OAI.CircleDomainRigidity.principal_conductivity_exterior_decay line 51