SemidiskLogarithm.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A genuine holomorphic logarithm on the half disk. Its imaginary coordinate records only the modulus of the original function.