OAI/Analysis/CircleDomains/Reflection/SemidiskModulusExtension.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Continuity at a boundary arc follows from convergence of the modulus alone. The logarithm, the half-disk barrier and the derivative bound supply the missing complex boundary values.

  1. lemma OAI.CircleDomainRigidity.mem_closure_upperSemidisk line 13
  2. lemma OAI.CircleDomainRigidity.upperSemidisk_mono line 24
  3. lemma OAI.CircleDomainRigidity.exists_continuous_extension_of_modulus_trace line 27