analysis icon indicating copy to clipboard operation
analysis copied to clipboard
verified publisher icon math-comp

Holomorphy

Open mkerjean opened this issue 5 years ago • 2 comments

Formalization of complex analysis, following the closed #192.

mkerjean avatar May 14 '20 13:05 mkerjean

@mkerjean @mkerjean CI fixed (cf https://github.com/math-comp/math-comp-nix/blob/e4d6c84698822d395832a6bc2c6d308356e2b08f/default.nix#L40)

CohenCyril avatar May 21 '20 17:05 CohenCyril

FYI, for the proof of (Differentiable /\ Cauchy-Riemann => Holomorphic), I tried to reintroduce two normed structure on R[i], in order to use the theory of differentiability already developed. However, it is still difficult to handle, as basic computations do not perform easily https://github.com/math-comp/analysis/blob/e2bab6f145d62cde3c15472175983733989e6e14/theories/holomorphy.v#L547. Would that be something which could be solved by this branch of real-closed @CohenCyril ?

mkerjean avatar Jul 12 '20 22:07 mkerjean