ModulusBoundaryContinuation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A bounded holomorphic disk-valued map with modulus tending to one at a straight boundary has an actual holomorphic continuation there. Complex boundary continuity is constructed, rather than assumed.

lemma OAI.CircleDomainRigidity.exists_holomorphic_continuation_of_modulus_trace line 14