OAI/Analysis/CircleDomains/Rigidity/FiniteCoreAnalyticTrace.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite coordinates of the actual compact-core extension are continuous on boundary collars and holomorphic on their exterior side.

  1. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.finite_core_image_ne_infty line 18
  2. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.finite_core_trace_continuousOn line 26
  3. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.finite_core_trace_differentiableAt line 37