OAI/Analysis/CircleDomains/Reflection/PrincipalComplexCoefficientData.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Retain the actual smooth coefficient convergence together with the principal homeomorphism limit. It comes from the same bounded mollification used in constructing the principal solution.

  1. lemma OAI.CircleDomainRigidity.exists_principal_complex_coefficient_data line 14