Skip to content

Holomorphy #204

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Draft
mkerjean wants to merge 3 commits into
base: master
Choose a base branch
from
Draft

Holomorphy #204

mkerjean wants to merge 3 commits into from

Conversation

@mkerjean
Copy link
Collaborator

@mkerjean mkerjean commented May 14, 2020 •
edited by CohenCyril
Loading

Formalization of complex analysis, following the closed #192.

@mkerjean mkerjean force-pushed the holomorphy branch 2 times, most recently from a320f3f to 8339fd8 Compare May 15, 2020 22:05
@mkerjean mkerjean marked this pull request as draft May 15, 2020 23:13
@CohenCyril
Copy link
Member

CohenCyril commented May 21, 2020 •
edited
Loading

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

@mkerjean
Copy link
Collaborator Author

mkerjean commented Jul 12, 2020 •
edited
Loading

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

analysis/theories/holomorphy.v

Line 547 in e2bab6f

have -> : fh = (f ( (x +i* y) + c) - ( (f c) + (x +i* y) *: ('D_1 f c)))by admit.
. Would that be something which could be solved by this branch of real-closed @CohenCyril ?

CohenCyril
CohenCyril reviewed Oct 25, 2020
View reviewed changes
theories/holomorphy.v Outdated
Comment on lines 154 to 205
Lemma complexV (*name ?*) (h: R) : h != 0 -> (h^-1)%:C = h%:C^-1.
Proof.
rewrite eqE_complex //=; split; last by rewrite mul0r oppr0.
by rewrite expr0n //= addr0 -exprVn expr2 mulrA mulrV ?unitfE ?mul1r //=.
Qed.
Copy link
Member

@CohenCyril CohenCyril Oct 25, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

apply: fmorphV did not work?

@mkerjean mkerjean force-pushed the holomorphy branch 3 times, most recently from 8cd8eb1 to 5c351f2 Compare December 11, 2020 08:44
@mkerjean mkerjean force-pushed the holomorphy branch 5 times, most recently from 10b830b to fc94508 Compare January 7, 2021 12:08
CohenCyril and others added 2 commits March 22, 2021 09:38
@CohenCyril @affeldt-aist
Mathcomp analysis now depends on real-closed
1d5e6af 
- fixed opam
- fixed nix

co-authored-by: Reynald Affeldt <[email protected]>
holomorphic
22f9c81 
Co-Authored-By : Reynald Affeldt
Co-Authored-By : Cyril Cohen
@proux01 proux01 added the TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done. label Jan 25, 2024
@Tragicus Tragicus mentioned this pull request May 22, 2025
Open
2 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@CohenCyril CohenCyril CohenCyril left review comments

Assignees

No one assigned

Labels

TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@mkerjean @CohenCyril @proux01