From d1ed227a829591d431449d96ddc492a9d0012902 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Mon, 4 May 2020 17:54:48 +0200 Subject: [PATCH 01/11] Mathcomp analysis now depends on real-closed - fixed opam - fixed nix co-authored-by: Reynald Affeldt --- .travis.yml | 9 +++++---- default.nix | 11 +++++++---- opam | 1 + 3 files changed, 13 insertions(+), 8 deletions(-) diff --git a/.travis.yml b/.travis.yml index 2cb49ebfa6..fbdd28ee1f 100644 --- a/.travis.yml +++ b/.travis.yml @@ -21,9 +21,10 @@ install: - docker pull ${DOCKERIMAGE} - docker tag ${DOCKERIMAGE} ci:current - docker run --env=OPAMYES --init -id --name=CI -v ${TRAVIS_BUILD_DIR}:/home/coq/${CONTRIB} -w /home/coq/${CONTRIB} ci:current -- docker exec CI /bin/bash --login -c "cd ..; curl -LO https://github.com/math-comp/finmap/archive/1.5.0.tar.gz; tar -xvzf 1.5.0.tar.gz; cd finmap-1.5.0/; opam pin add -y -n coq-mathcomp-finmap.1.5.0 .; opam install coq-mathcomp-finmap.1.5.0; cd /home/coq/${CONTRIB}" -- docker exec CI /bin/bash --login -c "opam pin add -y -n coq-mathcomp-${CONTRIB} ." -- docker exec CI /bin/bash --login -c "opam install --deps-only coq-mathcomp-${CONTRIB}" +- docker exec CI /bin/bash --login -c "opam repo add coq-released https://coq.inria.fr/opam/released" +- docker exec CI /bin/bash --login -c "opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev" +# - docker exec CI /bin/bash --login -c "opam pin add -y -n coq-mathcomp-${CONTRIB} ." +- docker exec CI /bin/bash --login -c "opam install --deps-only ." script: -- docker exec CI /bin/bash --login -c "opam install -vvv coq-mathcomp-${CONTRIB}" +- docker exec CI /bin/bash --login -c "opam install -vvv ." diff --git a/default.nix b/default.nix index 20843850b3..a6e08dceaa 100644 --- a/default.nix +++ b/default.nix @@ -32,10 +32,13 @@ let }; } // (cfg-fun all-pkgs); in { - # mathcomp-extra-config = lib.recursiveUpdate super.mathcomp-extra-config { - # for-coq-and-mc.${self.coq.coq-version}.${self.mathcomp.version} = - # removeAttrs cfg ["mathcomp" "coq"]; - # }; + mathcomp-extra-config = lib.recursiveUpdate super.mathcomp-extra-config { + initial = { + mathcomp-analysis = version: + let mca = super.mathcomp-extra-config.initial.mathcomp-analysis version; in + mca // { propagatedBuildInputs = mca.propagatedBuildInputs ++ [self.mathcomp-real-closed]; }; + }; + }; mathcomp = if cfg?mathcomp then self.mathcomp_ cfg.mathcomp else super.mathcomp_ "1.11.0+beta1"; } // mapAttrs (package: version: coqPackages.mathcomp-extra package version) diff --git a/opam b/opam index bd9641ec0f..e9c0b0b856 100644 --- a/opam +++ b/opam @@ -22,6 +22,7 @@ depends: [ "coq" { ((>= "8.7" & < "8.12~") | = "dev") } "coq-mathcomp-field" {(>= "1.11.0" & < "1.12~")} "coq-mathcomp-finmap" {(>= "1.5.0" & < "1.6~")} + "coq-mathcomp-real-closed" {(>= "1.0.5" & < "1.1~")} ] synopsis: "An analysis library for mathematical components" description: """ From 7fba627792b9f41bab642beb70b7fc76eb0888a0 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 6 Sep 2019 13:37:23 +0200 Subject: [PATCH 02/11] proof of Cauchy thm; derivx, derivy --- theories/cauchyetoile.v | 459 +++++++++++++++ theories/complex_holomorphy.v | 1005 +++++++++++++++++++++++++++++++++ 2 files changed, 1464 insertions(+) create mode 100644 theories/cauchyetoile.v create mode 100644 theories/complex_holomorphy.v diff --git a/theories/cauchyetoile.v b/theories/cauchyetoile.v new file mode 100644 index 0000000000..e21e6c1937 --- /dev/null +++ b/theories/cauchyetoile.v @@ -0,0 +1,459 @@ +(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +Require Import Reals. +From mathcomp Require Import ssreflect ssrfun ssrbool. +From mathcomp Require Import ssrnat eqtype choice fintype bigop ssralg ssrnum. +From mathcomp Require Import complex. +From mathcomp Require Import boolp reals Rstruct Rbar derive. +Require Import classical_sets posnum topology normedtype landau integral. + + +(*TODO : Definition integrale sur chemin et segment, holomorhpe, ouvert étoilé *) +(* TODO : cloner depuis integrale et commiter. Admettre la mesure sur R *) + + +(*Pour distinguer fonctions mesurables et integrables, utiliser des structures comme posrel. *) +Import GRing.Theory Num.Theory ComplexField Num.Def. +Local Open Scope ring_scope. +Local Open Scope classical_set_scope. +Local Open Scope complex_scope. + + + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. +(* Obligation Tactic := idtac. *) + + Local Notation sgr := Num.sg. + Local Notation sqrtr := Num.sqrt. + Local Notation C := R[i]. + + Notation Re:= (complex.Re). + Notation Im:= (complex.Im). + + +(*Adapting lemma eq_complex from complex.v, which was done in boolean style*) + Lemma eqE_complex : forall (x y : C), (x = y) = ((Re x = Re y) /\ (Im x = Im y)). + Proof. + move => [a b] [c d]; apply : propositional_extensionality ; split. + by move => -> ; split. + by case => //= -> ->. + Qed. + + Lemma Re0 : Re 0 = 0 :> R. + Proof. by []. Qed. + + Lemma Im0 : Im 0 = 0 :> R. + Proof. by []. Qed. + + Lemma ReIm_eq0 (x : C) : (x=0) = ((Re x = 0)/\(Im x = 0)). + Proof. + by rewrite -[in Re x= _]Re0 -Im0 -eqE_complex. + Qed. + + Lemma normc0 : normc 0 = 0 :> R . + Proof. + by rewrite /normc //= expr0n //= add0r sqrtr0. + Qed. + + Lemma normc_r (x : R) : normc (x%:C) = normr (x). + Proof. by rewrite /normc/= expr0n //= addr0 sqrtr_sqr. Qed. + + + Lemma normc_i (x : R) : normc (x*i) = normr (x). + Proof. by rewrite /normc/= expr0n //= add0r sqrtr_sqr. Qed. + + Lemma normcN1 : normc (-1%:C) = 1 :> R. + Proof. + by rewrite /normc/= oppr0 expr0n addr0 -signr_odd expr0 sqrtr1. + Qed. + + Lemma realtocomplex_additive : forall x y : R, (x + y)%:C = x%:C + y%:C. + Proof. + move => x y ; rewrite -!complexr0 eqE_complex //=. + by split ; last by rewrite addr0. + Qed. + + + + Lemma real_complex_inv : forall x : R, x%:C^-1 = (x^-1)%:C. + Proof. Admitted. + + Lemma Im_inv : ('i%C)^-1 = (-1*i) :> C. + Proof. Admitted. + + Lemma invcM : forall x y : C, (x*y)^-1 = x^-1 * y^-1. (*Maybe another lemma is doing that, or invrM *) + Proof. Admitted. + + Lemma Im_mul : forall x : R, (x*i) = (x%:C * 'i%C). + Proof. by move => x ; simpc. Qed. + + Lemma normcD : forall ( x y : C), normc (x+y) <= (normc x + normc y). + Proof. + by move => x y ; rewrite -lecR realtocomplex_additive ; apply :lec_normD . + Qed. + + Lemma normcZ : forall (l : R) (x : C), normc (l *: x) = `|l| * (normc x). + Proof. + move => l [a b] ; rewrite /normc //= !exprMn. + rewrite -mulrDr sqrtrM ; last by rewrite sqr_ge0. + by rewrite sqrtr_sqr. + Qed. + + Lemma scalecr : forall w : C^o, forall r : R, (r *: w = r%:C *: w). + Proof. by move => [a b ] r ; rewrite eqE_complex //= ; split ; simpc. Qed. + + +Section C_Rnormed. + + (* Uniform.mixin_of takes a locally but does not expect a TopologicalType, which is inserted in the Uniform.class_of *) + (* Whereas NormedModule.mixin_of asks for a Uniform.mixin_of loc *) + +(*Context (K : absRingType). Nor working with any K, how to close the real scope ? Do it before ? *) + + + Program Definition uniformmixin_of_normaxioms (V : lmodType R) (norm : V -> R) + (ax1 : forall x y : V, norm (x + y) <= norm x + norm y) + ( ax2 : forall (l : R) (x : V), norm (l *: x) = `|l| * (norm x)) + ( ax4 : forall x : V, norm x = 0 -> x = 0 ) : Uniform.mixin_of (locally_ (ball_ norm)) + := @Uniform.Mixin V (locally_ (ball_ norm)) (ball_ norm) _ _ _ _. + Next Obligation. + move => V norm _ H _ ; rewrite /ball_ => x e. + have -> : x - x = 0 . by rewrite addrN. + suff -> : norm 0 = 0 by []. + have -> : 0 = 0 *: x by rewrite scale0r. + by rewrite H normr0 mul0r. + Qed. + Next Obligation. + move => V norm _ H _ ; rewrite /ball_ => x e e0. + have -> : x - e = (-1) *: (e-x) by rewrite -opprB scaleN1r. + by rewrite (H (-1) (e-x)) normrN1 mul1r. + Qed. + Next Obligation. + move => V norm H _ _ ; rewrite /ball_ => x y z e1 e2 normxy normyz. + by rewrite (subr_trans y) (ler_lt_trans (H _ _)) ?ltr_add. + Qed. + Next Obligation. by []. Qed. + + (*C as a R-lmodule *) + Definition C_RlmodMixin := (complex_lmodMixin R_rcfType). (*R instead of R_rcfType is not working *) + (*LmodType is hard to use, not findable through Search and not checkable as abbreviation is not applied enough*) + Definition C_RlmodType := @LmodType R C C_RlmodMixin. + Definition C_pointedType := PointedType C 0. + Canonical C_pointedType. + Definition C_filteredType := FilteredType C C (locally_ (ball_ (@normc R_rcfType))). + Canonical C_filteredType. + (*Are we sure that the above is canonical *) + + Program Definition C_RuniformMixin := @uniformmixin_of_normaxioms C_RlmodType (@normc R_rcfType) normcD normcZ (@eq0_normc R_rcfType). + Definition C_RtopologicalMixin := topologyOfBallMixin C_RuniformMixin. + Definition C_RtopologicalType := TopologicalType C_filteredType C_RtopologicalMixin. + Definition C_RuniformType := @UniformType C_RtopologicalType C_RuniformMixin. + + + Program Definition C_RnormedMixin + := @NormedModMixin R_absRingType C_RlmodType _ C_RuniformMixin (@normc R_rcfType) normcD normcZ _ (@eq0_normc R_rcfType) . + Next Obligation. by []. Qed. + + + Definition C_RnormedType : normedModType R := @NormedModType R C_RuniformType C_RnormedMixin. +End C_Rnormed. +Section C_absRing. + + Definition C_AbsRingMixin := @AbsRingMixin (complex_ringType R_rcfType) (@normc R_rcfType) normc0 normcN1 normcD (@normcM R_rcfType ) (@eq0_normc R_rcfType). + + + + Definition C_absRingType := AbsRingType C C_AbsRingMixin. + Canonical C_absRingType. + Definition C_topologicalType := [topologicalType of C for C_absRingType]. + Canonical C_topologicalType. + Definition C_uniformType := [uniformType of C for C_absRingType]. + Canonical C_uniformType. + Definition Co_pointedType := [pointedType of C^o for C_absRingType]. + (*Canonical Co_pointedType.*) + Locate Ro_pointedType. + Definition Co_filteredType := [filteredType C^o of C^o for C_absRingType]. + Definition Co_topologicalType := [topologicalType of C^o for C_absRingType]. + Definition Co_uniformType := [uniformType of C^o for C_absRingType]. + Definition Co_normedType := AbsRing_NormedModType C_absRingType. + (*Canonical Co_normedType.*) + (*Why is this Canonical, when the normed type on Ro is defined for R of the reals ? *) + + Lemma absCE : forall x : C, `|x|%real = normc x. + Proof. by []. Qed. + + + Lemma absring_real_complex : forall r: R, forall x : R, AbsRing_ball 0 r x -> (@AbsRing_ball C_absRingType 0%:C r x%:C). + Proof. + move => r x ballrx. + rewrite /AbsRing_ball /ball_ absCE. + rewrite addrC addr0 -scaleN1r normcZ normrN1 mul1r normc_r. + move : ballrx ; rewrite /AbsRing_ball /ball_ absRE. + by rewrite addrC addr0 normrN. + Qed. + + + Lemma absring_real_Im : forall r: R, forall x : R, AbsRing_ball 0 r x -> (@AbsRing_ball C_absRingType 0%:C r x*i). + Proof. + move => r x ballrx. + rewrite /AbsRing_ball /ball_ absCE. + rewrite addrC addr0 -scaleN1r normcZ normrN1 mul1r normc_i. + move : ballrx ; rewrite /AbsRing_ball /ball_ absRE. + by rewrite addrC addr0 normrN. + Qed. + + Lemma scalei_muli : forall z : C^o, ('i * z) = ('i *: z). + Proof. + by []. + Qed. + + Lemma iE : 'i%C = 'i :> C. + Proof. by []. Qed. + +End C_absRing. + +Section Holomorphe. + +Print differentiable_def. +(* used in derive.v, what does center means*) +(*CoInductive +differentiable_def (K : absRingType) (V W : normedModType K) (f : V -> W) +(x : filter_on V) (phF : phantom (set (set V)) x) : Prop := + DifferentiableDef : continuous 'd f x /\ f = (cst (f (lim x)) + 'd f x) \o + center (lim x) +o_x center (lim x) -> differentiable_def f phF *) +(*Diff is defined from any normedmodule of any absringtype, so C is a normedmodul on itsself *) +(*Vague idea that this should work, as we see C^o as a vector space on C and not R*) + + +(*Important : differentiable in derive.v, means continuoulsy differentiable, not just that the limit exists. *) +(*derivable concerns only the existence of the derivative *) + +Definition holomorphic (f : Co_normedType -> Co_normedType) c := forall v, +cvg ((fun h => h^-1 *: ((f \o shift c) (h *: v) - f c)) @ locally' (0 : Co_normedType)). + +Definition complex_realfun (f : C^o -> C^o) : C_RnormedType -> C_RnormedType := f. + +Definition complex_Rnormed_absring : C_RnormedType -> C^o := id. (* Coercion ? *) (*Avec C tout seul au lieu de C_absRIng ça devrait passer *) + + +(* Variable ( h : C_RnormedType -> C_RnormedType) (x : C_RnormedType). *) + +(* Check ('D_x h 0). (*This has a weird type *) *) + +Definition CauchyRiemanEq_R2 (f : C_RnormedType -> C_RnormedType) c := + let u := (fun c => Re ( f c)): C_RnormedType -> R^o in + let v:= (fun c => Im (f c)) : C_RnormedType -> R^o in + (* ('D_(1%:C) u = 'D_('i) v) /\ ('D_('i) u = 'D_(1%:C) v). *) + (((derive u c (1%:C)) = + (derive v c ('i))) /\ ((derive v c (1%:C)) = -(derive u c ('i)))). + + +Definition deriveC (V W : normedModType C)(f : V -> W) c v := + lim ((fun h => h^-1 *: ((f \o shift c) (h *: v) - f c)) @ locally' (0 : C^o)). + + +Definition CauchyRiemanEq (f : C -> C) z:= + 'i * lim ((fun h : R => h^-1 *: ((f \o shift z) (h *: 1%:C) - f z)) @ locally' (0 : R^o)) = + lim ((fun h : R => h^-1 *: ((f \o shift z) (h *: 'i%C) - f z)) @ locally' (0 : R^o)). + + +Lemma eqCr (R : rcfType) (r s : R) : (r%:C == s%:C) = (r == s). +Proof. exact: (inj_eq (@complexI _)). Qed. + +Lemma eqCI (R : rcfType) (r s : R) : (r*i == s*i) = (r == s). +Proof. Admitted. + + +(*Lemma lim_trans (T : topologicalType) (F : set (set T)) (G : set (set T)) (l : T) : ( F `=>` G ) -> (G --> l) -> ( F --> l). + move => FG Gl A x. + Search "lim" "trans". + *) + +Lemma cvg_translim (T : topologicalType) (F G: set (set T)) (l :T) : + F `=>` G -> (G --> l) -> (F --> l). +Proof. + move => FG Gl. apply : cvg_trans. + exact : FG. + exact : Gl. +Qed. + + +Lemma cvg_scaler (K : absRingType) (V : normedModType K) (T : topologicalType) + (F : set (set T)) (H :Filter F) (f : T -> V) (k : K) : + cvg (f @ F) -> cvg ((k \*: f) @ F ). +Proof. + by move => /cvg_ex [l H0] ; apply : cvgP ; apply :(@cvgZr _ _ _ F _ f k l). +Qed. + +About cvgZr. + + +Lemma limin_scaler (K : absRingType) (V : normedModType K) (T : topologicalType) + (F : set (set T)) (FF :Filter F) (f : T -> V) (k : K) : + cvg(f@F) -> k *: lim (f @ F) = lim ((k \*: f) @ F ). +Proof. + move => /cvg_ex [l H]. + (*rewrite (cvg_lim H). *) +(* The LHS of (cvg_lim H) *) +(* (lim (f @ F)) *) +(* matches but type classes inference fails *) +(* Check (cvg_lim (@cvgZr K V T F FF f k l H)). *) + Admitted. + + +(*this could be done for scale also ... *) + +(*I needed filter_of_filterE to make things easier - looked a long time of it as I was lookin for a [filter of lim]* instead of a [filter of filter]*) + +(*There whould be a lemma analogous to [filter of lim] to ease the search *) + +(* + +Lemma filter_of_filterE {T : Type} (F : set (set T)) : [filter of F] = F. +Proof. by []. Qed. + +Lemma locally_filterE {T : Type} (F : set (set T)) : locally F = F. +Proof. by []. Qed. + +Module Export LocallyFilter. +Definition locally_simpl := (@filter_of_filterE, @locally_filterE). +End LocallyFilter. + +Definition cvg_to {T : Type} (F G : set (set T)) := G `<=` F. +Notation "F `=>` G" := (cvg_to F G) : classical_set_scope. +Lemma cvg_refl T (F : set (set T)) : F `=>` F. +Proof. exact. Qed. + +Lemma cvg_trans T (G F H : set (set T)) : + (F `=>` G) -> (G `=>` H) -> (F `=>` H). +Proof. by move=> FG GH P /GH /FG. Qed. + +Notation "F --> G" := (cvg_to [filter of F] [filter of G]) : classical_set_scope. +Definition type_of_filter {T} (F : set (set T)) := T. + +Definition lim_in {U : Type} (T : filteredType U) := + fun F : set (set U) => get (fun l : T => F --> l). +Notation "[ 'lim' F 'in' T ]" := (@lim_in _ T [filter of F]) : classical_set_scope. +Notation lim F := [lim F in [filteredType _ of @type_of_filter _ [filter of F]]]. +Notation "[ 'cvg' F 'in' T ]" := (F --> [lim F in T]) : classical_set_scope. +Notation cvg F := [cvg F in [filteredType _ of @type_of_filter _ [filter of F]]]. +*) + + + +Lemma holo_derivable (f : C^o -> C^o) c : ((holomorphic f c)) + -> (forall v : C, derivable (complex_realfun f) c v). +Proof. + move => H; rewrite /derivable => v. + move : (H v) => /cvg_ex [l H0] {H}. (* eapply*) + apply : (cvgP (l := l)). + - have eqnear0 : {near (@locally' R_topologicalType 0), + (fun h : C_absRingType => h^-1 *: ((f \o shift c) (h *: (complex_Rnormed_absring v)) - f c)) + \o (real_complex R) =1 + (fun h0 : R_absRingType => h0^-1 *: ((complex_realfun f \o shift c) (h0 *: v ) + - complex_realfun f c)) }. + exists 1 ; first by [] ; move => h _ neq0h //=; rewrite real_complex_inv -scalecr. + by apply : (scalerI (neq0h)) ; rewrite !scalerA //= (divff neq0h) !scale1r //= -scalecr. + pose subsetfilters:= (cvg_eq_loc eqnear0). + apply : (@cvg_trans _ ( (fun h : C_absRingType => h^-1 *: ((f \o shift c) (h *: (complex_Rnormed_absring v)) - f c)) \o (real_complex R) @ (@locally' R_topologicalType 0))). + exact : (subsetfilters (@locally'_filter R_topologicalType 0)). +- unshelve apply : cvg_comp. + exact (locally' 0%:C). +- move => //= A [r [leq0r ballrA]] ; exists r ; first by []. + move => b ballrb neqb0. + have ballCrb : (AbsRing_ball 0%:C r b%:C). + by apply : absring_real_complex. + have bneq0C : (b%:C != 0%:C) by move : neqb0 ; apply : contra ; rewrite eqCr. + by apply : (ballrA b%:C ballCrb bneq0C). +by []. +Qed. + +Lemma holo_CauchyRieman (f : C^o -> C^o) c : (holomorphic f c) -> (CauchyRiemanEq f c). +Proof. + move => H. (* move : (H 1%:C) => /cvg_ex [l H0] {H}. *) + (* move : l H0 ; rewrite filter_of_filterE => l H0. *) + pose quotC := (fun h : C_absRingType => h^-1 *: ((f \o shift c) (h * 1%:C) - f c)). + pose quotR := (fun h : R_absRingType => h^-1 *: ((f \o shift c) (h *: 1%:C ) - f c)). + pose quotiR := (fun (h : R) => h^-1 *: ((f \o shift c) (h *: 'i%C) - f c)). + have eqnear0x : {near (@locally' R_topologicalType 0), quotC \o ( fun h => h *: 1%:C) =1 quotR }. + exists 1 ; first by [] ; move => h _ _ //= ; simpc. + by rewrite /quotC /quotR real_complex_inv -scalecr ; simpc. + pose subsetfiltersx := (cvg_eq_loc eqnear0x). + rewrite /CauchyRiemanEq. + have -> : lim (quotR @ (@locally' R_topologicalType 0)) + = lim (quotC @ (@locally' C_topologicalType 0) ). + apply: (@cvg_map_lim _ _ _ (@locally' R_topologicalType 0) _ _ (lim (quotC @ (@locally' C_topologicalType 0) ))). + suff : quotR @ (@locally' R_topologicalType 0) `=>` (quotC @ (@locally' C_topologicalType 0)). + by move => H1 ; apply : (cvg_translim H1) ; exact : H. + apply : cvg_trans. + - exact : (subsetfiltersx (@locally'_filter R_topologicalType 0)). + move => {subsetfiltersx eqnear0x}. + - unshelve apply : cvg_comp. + (*just showing that linear maps preserve balls - general lemma ? *) + - exact (@locally' C_topologicalType 0). + - move => A //= [r leq0r] absringrA. + exists r ; first by []. + move => h absrh hneq0 ; simpc. + apply : (absringrA h%:C). + - by apply : absring_real_complex. + - by rewrite eqCr . + by []. + have eqnear0y : {near (@locally' R_topologicalType 0), 'i \*:quotC \o ( fun h => h *: 'i%C) =1 + quotiR }. + exists 1 ; first by [] ; move => h _ _ //= ; simpc . rewrite /quotC /quotiR (Im_mul h) invcM. + rewrite scalerA real_complex_inv Im_inv !scalecr; simpc ; rewrite (Im_mul h). + by rewrite !real_complexE. + pose subsetfiltersy := (cvg_eq_loc eqnear0y). + have <- : lim (quotiR @ (@locally' R_topologicalType 0)) + = 'i * lim (quotC @ (@locally' C_topologicalType 0)). + have -> : 'i * lim (quotC @ (@locally' C_topologicalType 0)) + = lim ('i \*: quotC @ (@locally' C_topologicalType 0)). + rewrite scalei_muli ; rewrite (limin_scaler _ ('i) ). + - by []. + - exact : H. + apply : (@cvg_map_lim _ _ _ (@locally' R_topologicalType 0) _ _ (lim ('i \*:quotC @ (@locally' C_topologicalType 0) ))). + suff : quotiR @ (@locally' R_topologicalType 0) + `=>` ('i \*: quotC @ (@locally' C_topologicalType 0)). + move => H1 ; apply : (cvg_translim H1) . + by apply :(@cvg_scaler _ _ _ _ _ quotC ('i) ) ; exact : H. + apply : cvg_trans. + - apply : (subsetfiltersy (@locally'_filter R_topologicalType 0)). + move => {subsetfiltersx eqnear0x}. + - unshelve apply : cvg_comp. + - exact (@locally' C_topologicalType 0). + - move => A //= [r leq0r] absringrA. + exists r ; first by []. + move => h absrh hneq0 ; simpc. + apply : (absringrA h*i). + - by apply : absring_real_Im. + - by rewrite eqCI. + rewrite filter_of_filterE. + by []. + by []. +Qed. + + + Lemma Diff_CR_holo (f : C^o -> C^o) c: + (forall v : C, derivable (complex_realfun f) c v) /\ (CauchyRiemanEq f c) -> + ((holomorphic f c)) . + Proof. + move => [der CR] v. + move : (der v); move => /cvg_ex {der} [l der]. + apply : (@cvgP _ _ _ l). + move => //= A loclA. + have lem : locally ((fun h : R => h^-1 *: (complex_realfun f (h *: v + c) - complex_realfun f c)) + @ (@locally' R_topologicalType 0)) A by exact : (der A loclA). + move : loclA ; move =>[r leq0r] absrA ; exists r ; first by []. + - move => [x y] ballrh neq0h //=. + move : lem ; move => //=. +Admitted. + +Theorem CauchyRiemann (f : C^o -> C^o) c: ((holomorphic f c)) + <-> (forall v : C, derivable (complex_realfun f) c v) /\ (CauchyRiemanEq f c). +Proof. +Admitted. + + + + +End Holomorphe. diff --git a/theories/complex_holomorphy.v b/theories/complex_holomorphy.v new file mode 100644 index 0000000000..2d097d4095 --- /dev/null +++ b/theories/complex_holomorphy.v @@ -0,0 +1,1005 @@ +(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) + + +(* This is the tentative adaptation of the real-closed/complex.v file to a self-contained *) +(* description of complex theory and holomorphy *) +Require Import Reals. +From mathcomp Require Import ssreflect ssrfun ssrbool. +From mathcomp Require Import ssrnat eqtype choice fintype bigop ssralg ssrnum seq . +Require Import boolp reals Rstruct Rbar derive. +From mathcomp Require Import bigop ssrint div ssrnum rat poly closed_field. +From mathcomp Require Import matrix mxalgebra tuple mxpoly zmodp binomial. +Require Import classical_sets posnum topology normedtype landau integral reals. + + +(* Require Import bigop ssralg ssrint div ssrnum rat poly closed_field. *) +(* Require Import classical_sets posnum topology normedtype landau integral. *) +(* From mathcomp *) +(* Require Import matrix mxalgebra tuple mxpoly zmodp binomial. *) + +(*TODO : Definition integrale sur chemin et segment, holomorhpe, ouvert étoilé *) +(* TODO : cloner depuis integrale et commiter. Admettre la mesure sur R *) + + +(*Pour distinguer fonctions mesurables et integrables, utiliser des structures comme posrel. *) +Import GRing.Theory Num.Theory (*ComplexField*) Num.Def. +Local Open Scope ring_scope. +Local Open Scope classical_set_scope. + + + +(* Set Implicit Arguments. *) +(* Unset Strict Implicit. *) +(* Unset Printing Implicit Defensive. *) +(* (* Obligation Tactic := idtac. *) *) + + +Import GRing.Theory Num.Theory. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Obligation Tactic := idtac. + +Local Open Scope ring_scope. + +Reserved Notation "x +i* y" + (at level 40, left associativity, format "x +i* y"). +Reserved Notation "x -i* y" + (at level 40, left associativity, format "x -i* y"). +Reserved Notation "R [i]" + (at level 2, left associativity, format "R [i]"). + +Local Notation sgr := Num.sg. +Local Notation sqrtr := Num.sqrt. + +Record complex (R : Type) : Type := Complex { Re : R; Im : R }. + +Delimit Scope complex_scope with C. +Local Open Scope complex_scope. + +Definition real_complex_def (F : ringType) (phF : phant F) (x : F) := + Complex x 0. +Notation real_complex F := (@real_complex_def _ (Phant F)). +Notation "x %:C" := (real_complex _ x) + (at level 2, left associativity, format "x %:C") : complex_scope. +Notation "x +i* y" := (Complex x y) : complex_scope. +Notation "x -i* y" := (Complex x (- y)) : complex_scope. +Notation "x *i " := (Complex 0 x) (at level 8, format "x *i") : complex_scope. +Notation "''i'" := (Complex 0 1) : complex_scope. +Notation "R [i]" := (complex R) + (at level 2, left associativity, format "R [i]"). + +(* Module ComplexInternal. *) +Module ComplexEqChoice. +Section ComplexEqChoice. + +Variable R : Type. + +Definition sqR_of_complex (x : R[i]) := let: a +i* b := x in [:: a ; b]. +Definition complex_of_sqR (x : seq R) := + if x is [:: a; b] then Some (a +i* b) else None. + +Lemma complex_of_sqRK : pcancel sqR_of_complex complex_of_sqR. +Proof. by case. Qed. + +End ComplexEqChoice. +End ComplexEqChoice. + +Definition complex_eqMixin (R : eqType) := + PcanEqMixin (@ComplexEqChoice.complex_of_sqRK R). +Definition complex_choiceMixin (R : choiceType) := + PcanChoiceMixin (@ComplexEqChoice.complex_of_sqRK R). +Definition complex_countMixin (R : countType) := + PcanCountMixin (@ComplexEqChoice.complex_of_sqRK R). + +Canonical complex_eqType (R : eqType) := + EqType R[i] (complex_eqMixin R). +Canonical complex_choiceType (R : choiceType) := + ChoiceType R[i] (complex_choiceMixin R). +Canonical complex_countType (R : countType) := + CountType R[i] (complex_countMixin R). + +Lemma eq_complex : forall (x y : complex R), + (x == y) = (Re x == Re y) && (Im x == Im y). +Proof. +move=> [a b] [c d] /=. +apply/eqP/andP; first by move=> [-> ->]; split. +by case; move/eqP->; move/eqP->. +Qed. + +Lemma complexr0 : forall (x : R), x +i* 0 = x%:C. Proof. by []. Qed. + +Module ComplexField. +Section ComplexField. + +Local Notation C := R[i]. +Local Notation C0 := ((0 : R)%:C). +Local Notation C1 := ((1 : R)%:C). + +Definition addc (x y : R[i]) := let: a +i* b := x in let: c +i* d := y in + (a + c) +i* (b + d). +Definition oppc (x : R[i]) := let: a +i* b := x in (- a) +i* (- b). + +Program Definition complex_zmodMixin := @ZmodMixin _ C0 oppc addc _ _ _ _. +Next Obligation. by move=> [a b] [c d] [e f] /=; rewrite !addrA. Qed. +Next Obligation. by move=> [a b] [c d] /=; congr (_ +i* _); rewrite addrC. Qed. +Next Obligation. by move=> [a b] /=; rewrite !add0r. Qed. +Next Obligation. by move=> [a b] /=; rewrite !addNr. Qed. +Canonical complex_zmodType := ZmodType R[i] complex_zmodMixin. + +Definition scalec (a : R) (x : R[i]) := + let: b +i* c := x in (a * b) +i* (a * c). + +Program Definition complex_lmodMixin := @LmodMixin _ _ scalec _ _ _ _. +Next Obligation. by move=> a b [c d] /=; rewrite !mulrA. Qed. +Next Obligation. by move=> [a b] /=; rewrite !mul1r. Qed. +Next Obligation. by move=> a [b c] [d e] /=; rewrite !mulrDr. Qed. +Next Obligation. by move=> [a b] c d /=; rewrite !mulrDl. Qed. +Canonical complex_lmodType := LmodType R R[i] complex_lmodMixin. + +Definition mulc (x y : R[i]) := let: a +i* b := x in let: c +i* d := y in + ((a * c) - (b * d)) +i* ((a * d) + (b * c)). + +Lemma mulcC : commutative mulc. +Proof. +move=> [a b] [c d] /=. +by rewrite [c * b + _]addrC ![_ * c]mulrC ![_ * d]mulrC. +Qed. + +Lemma mulcA : associative mulc. +Proof. +move=> [a b] [c d] [e f] /=. +rewrite !mulrDr !mulrDl !mulrN !mulNr !mulrA !opprD -!addrA. +by congr ((_ + _) +i* (_ + _)); rewrite !addrA addrAC; + congr (_ + _); rewrite addrC. +Qed. + +Definition invc (x : R[i]) := let: a +i* b := x in let n2 := (a ^+ 2 + b ^+ 2) in + (a / n2) -i* (b / n2). + +Lemma mul1c : left_id C1 mulc. +Proof. by move=> [a b] /=; rewrite !mul1r !mul0r subr0 addr0. Qed. + +Lemma mulc_addl : left_distributive mulc addc. +Proof. +move=> [a b] [c d] [e f] /=; rewrite !mulrDl !opprD -!addrA. +by congr ((_ + _) +i* (_ + _)); rewrite addrCA. +Qed. + +Lemma nonzero1c : C1 != C0. Proof. by rewrite eq_complex /= oner_eq0. Qed. + +Definition complex_comRingMixin := + ComRingMixin mulcA mulcC mul1c mulc_addl nonzero1c. +Canonical complex_ringType :=RingType R[i] complex_comRingMixin. +Canonical complex_comRingType := ComRingType R[i] mulcC. + +Lemma mulVc : forall x, x != C0 -> mulc (invc x) x = C1. +Proof. +move=> [a b]; rewrite eq_complex => /= hab; rewrite !mulNr opprK. +rewrite ![_ / _ * _]mulrAC [b * a]mulrC subrr complexr0 -mulrDl mulfV //. +by rewrite paddr_eq0 -!expr2 ?expf_eq0 ?sqr_ge0. +Qed. + +Lemma invc0 : invc C0 = C0. Proof. by rewrite /= !mul0r oppr0. Qed. + +Definition complex_fieldUnitMixin := FieldUnitMixin mulVc invc0. +Canonical complex_unitRingType := UnitRingType C complex_fieldUnitMixin. +Canonical complex_comUnitRingType := Eval hnf in [comUnitRingType of R[i]]. + +Lemma field_axiom : GRing.Field.mixin_of complex_unitRingType. +Proof. by []. Qed. + +Definition ComplexFieldIdomainMixin := (FieldIdomainMixin field_axiom). +Canonical complex_idomainType := IdomainType R[i] (FieldIdomainMixin field_axiom). +Canonical complex_fieldType := FieldType R[i] field_axiom. + +Ltac simpc := do ? + [ rewrite -[(_ +i* _) - (_ +i* _)]/(_ +i* _) + | rewrite -[(_ +i* _) + (_ +i* _)]/(_ +i* _) + | rewrite -[(_ +i* _) * (_ +i* _)]/(_ +i* _)]. + +Lemma real_complex_is_rmorphism : rmorphism (real_complex R). +Proof. +split; [|split=> //] => a b /=; simpc; first by rewrite subrr. +by rewrite !mulr0 !mul0r addr0 subr0. +Qed. + +Canonical real_complex_rmorphism := + RMorphism real_complex_is_rmorphism. +Canonical real_complex_additive := + Additive real_complex_is_rmorphism. + +Lemma Re_is_scalar : scalar (@Re R). +Proof. by move=> a [b c] [d e]. Qed. + +Canonical Re_additive := Additive Re_is_scalar. +Canonical Re_linear := Linear Re_is_scalar. + +Lemma Im_is_scalar : scalar (@Im R). +Proof. by move=> a [b c] [d e]. Qed. + +Canonical Im_additive := Additive Im_is_scalar. +Canonical Im_linear := Linear Im_is_scalar. + +Definition lec (x y : R[i]) := + let: a +i* b := x in let: c +i* d := y in + (d == b) && (a <= c). + +Definition ltc (x y : R[i]) := + let: a +i* b := x in let: c +i* d := y in + (d == b) && (a < c). + +Definition normc (x : R[i]) : R := + let: a +i* b := x in sqrtr (a ^+ 2 + b ^+ 2). + +Notation normC x := (normc x)%:C. + +Lemma ltc0_add : forall x y, ltc 0 x -> ltc 0 y -> ltc 0 (x + y). +Proof. +move=> [a b] [c d] /= /andP [/eqP-> ha] /andP [/eqP-> hc]. +by rewrite addr0 eqxx addr_gt0. +Qed. + +Lemma eq0_normc x : normc x = 0 -> x = 0. +Proof. +case: x => a b /= /eqP; rewrite sqrtr_eq0 ler_eqVlt => /orP [|]; last first. + by rewrite ltrNge addr_ge0 ?sqr_ge0. +by rewrite paddr_eq0 ?sqr_ge0 ?expf_eq0 //= => /andP[/eqP -> /eqP ->]. +Qed. + +Lemma eq0_normC x : normC x = 0 -> x = 0. Proof. by case=> /eq0_normc. Qed. + +Lemma ge0_lec_total x y : lec 0 x -> lec 0 y -> lec x y || lec y x. +Proof. +move: x y => [a b] [c d] /= /andP[/eqP -> a_ge0] /andP[/eqP -> c_ge0]. +by rewrite eqxx ler_total. +Qed. + +Lemma normcM x y : normc (x * y) = normc x * normc y. +Proof. +move: x y => [a b] [c d] /=; rewrite -sqrtrM ?addr_ge0 ?sqr_ge0 //. +rewrite sqrrB sqrrD mulrDl !mulrDr -!exprMn. +rewrite mulrAC [b * d]mulrC !mulrA. +suff -> : forall (u v w z t : R), (u - v + w) + (z + v + t) = u + w + (z + t). + by rewrite addrAC !addrA. +by move=> u v w z t; rewrite [_ - _ + _]addrAC [z + v]addrC !addrA addrNK. +Qed. + +Lemma normCM x y : normC (x * y) = normC x * normC y. +Proof. by rewrite -rmorphM normcM. Qed. + +Lemma subc_ge0 x y : lec 0 (y - x) = lec x y. +Proof. by move: x y => [a b] [c d] /=; simpc; rewrite subr_ge0 subr_eq0. Qed. + +Lemma lec_def x y : lec x y = (normC (y - x) == y - x). +Proof. +rewrite -subc_ge0; move: (_ - _) => [a b]; rewrite eq_complex /= eq_sym. +have [<- /=|_] := altP eqP; last by rewrite andbF. +by rewrite [0 ^+ _]mul0r addr0 andbT sqrtr_sqr ger0_def. +Qed. + +Lemma ltc_def x y : ltc x y = (y != x) && lec x y. +Proof. +move: x y => [a b] [c d] /=; simpc; rewrite eq_complex /=. +by have [] := altP eqP; rewrite ?(andbF, andbT) //= ltr_def. +Qed. + +Lemma lec_normD x y : lec (normC (x + y)) (normC x + normC y). +Proof. +move: x y => [a b] [c d] /=; simpc; rewrite addr0 eqxx /=. +rewrite -(@ler_pexpn2r _ 2) -?topredE /= ?(ler_paddr, sqrtr_ge0) //. +rewrite [X in _ <= X] sqrrD ?sqr_sqrtr; + do ?by rewrite ?(ler_paddr, sqrtr_ge0, sqr_ge0, mulr_ge0) //. +rewrite -addrA addrCA (monoRL (addrNK _) (ler_add2r _)) !sqrrD. +set u := _ *+ 2; set v := _ *+ 2. +rewrite [a ^+ _ + _ + _]addrAC [b ^+ _ + _ + _]addrAC -addrA. +rewrite [u + _] addrC [X in _ - X]addrAC [b ^+ _ + _]addrC. +rewrite [u]lock [v]lock !addrA; set x := (a ^+ 2 + _ + _ + _). +rewrite -addrA addrC addKr -!lock addrC. +have [huv|] := ger0P (u + v); last first. + by move=> /ltrW /ler_trans -> //; rewrite pmulrn_lge0 // mulr_ge0 ?sqrtr_ge0. +rewrite -(@ler_pexpn2r _ 2) -?topredE //=; last first. + by rewrite ?(pmulrn_lge0, mulr_ge0, sqrtr_ge0) //. +rewrite -mulr_natl !exprMn !sqr_sqrtr ?(ler_paddr, sqr_ge0) //. +rewrite -mulrnDl -mulr_natl !exprMn ler_pmul2l ?exprn_gt0 ?ltr0n //. +rewrite sqrrD mulrDl !mulrDr -!exprMn addrAC -!addrA ler_add2l !addrA. +rewrite [_ + (b * d) ^+ 2]addrC -addrA ler_add2l. +have: 0 <= (a * d - b * c) ^+ 2 by rewrite sqr_ge0. +by rewrite sqrrB addrAC subr_ge0 [_ * c]mulrC mulrACA [d * _]mulrC. +Qed. + +Definition complex_numMixin := NumMixin lec_normD ltc0_add eq0_normC + ge0_lec_total normCM lec_def ltc_def. +Canonical complex_numDomainType := NumDomainType R[i] complex_numMixin. + +End ComplexField. +End ComplexField. + +Canonical ComplexField.complex_zmodType. +Canonical ComplexField.complex_lmodType. +Canonical ComplexField.complex_ringType. +Canonical ComplexField.complex_comRingType. +Canonical ComplexField.complex_unitRingType. +Canonical ComplexField.complex_comUnitRingType. +Canonical ComplexField.complex_idomainType. +Canonical ComplexField.complex_fieldType. +Canonical ComplexField.complex_numDomainType. +Canonical complex_numFieldType := [numFieldType of complex R]. +Canonical ComplexField.real_complex_rmorphism. +Canonical ComplexField.real_complex_additive. +Canonical ComplexField.Re_additive. +Canonical ComplexField.Im_additive. + +Definition conjc {R : ringType} (x : R[i]) := let: a +i* b := x in a -i* b. +Notation "x ^*" := (conjc x) (at level 2, format "x ^*") : complex_scope. +Local Open Scope complex_scope. +Delimit Scope complex_scope with C. + +Ltac simpc := do ? + [ rewrite -[- (_ +i* _)%C]/(_ +i* _)%C + | rewrite -[(_ +i* _)%C - (_ +i* _)%C]/(_ +i* _)%C + | rewrite -[(_ +i* _)%C + (_ +i* _)%C]/(_ +i* _)%C + | rewrite -[(_ +i* _)%C * (_ +i* _)%C]/(_ +i* _)%C + | rewrite -[(_ +i* _)%C ^*]/(_ +i* _)%C + | rewrite -[_ *: (_ +i* _)%C]/(_ +i* _)%C + | rewrite -[(_ +i* _)%C <= (_ +i* _)%C]/((_ == _) && (_ <= _)) + | rewrite -[(_ +i* _)%C < (_ +i* _)%C]/((_ == _) && (_ < _)) + | rewrite -[`|(_ +i* _)%C|]/(sqrtr (_ + _))%:C%C + | rewrite (mulrNN, mulrN, mulNr, opprB, opprD, mulr0, mul0r, + subr0, sub0r, addr0, add0r, mulr1, mul1r, subrr, opprK, oppr0, + eqxx) ]. + + +Section ComplexTheory. + + +Lemma ReiNIm : forall x : R[i], Re (x * 'i%C) = - Im x. +Proof. by case=> a b; simpc. Qed. + +Lemma ImiRe : forall x : R[i], Im (x * 'i%C) = Re x. +Proof. by case=> a b; simpc. Qed. + +Lemma complexE x : x = (Re x)%:C + 'i%C * (Im x)%:C :> R[i]. +Proof. by case: x => *; simpc. Qed. + +Lemma real_complexE x : x%:C = x +i* 0 :> R[i]. Proof. done. Qed. + +Lemma sqr_i : 'i%C ^+ 2 = -1 :> R[i]. +Proof. by rewrite exprS; simpc; rewrite -real_complexE rmorphN. Qed. + +Lemma complexI : injective (real_complex R). Proof. by move=> x y []. Qed. + +Lemma ler0c (x : R) : (0 <= x%:C) = (0 <= x). Proof. by simpc. Qed. + +Lemma lecE : forall x y : R[i], (x <= y) = (Im y == Im x) && (Re x <= Re y). +Proof. by move=> [a b] [c d]. Qed. + +Lemma ltcE : forall x y : R[i], (x < y) = (Im y == Im x) && (Re x < Re y). +Proof. by move=> [a b] [c d]. Qed. + +Lemma lecR : forall x y : R, (x%:C <= y%:C) = (x <= y). +Proof. by move=> x y; simpc. Qed. + +Lemma ltcR : forall x y : R, (x%:C < y%:C) = (x < y). +Proof. by move=> x y; simpc. Qed. + + +Lemma conjc_is_rmorphism : rmorphism (@conjc R_ringType). +Proof. +split=> [[a b] [c d] | ] /=; first by simpc; rewrite [d - _]addrC. +by split=> [[a b] [c d] | ] /=; simpc. +Qed. + +Lemma conjc_is_scalable : scalable (@conjc R_ringType ). +Proof. by move=> a [b c]; simpc. Qed. + +Canonical conjc_rmorphism := RMorphism conjc_is_rmorphism. +Canonical conjc_additive := Additive conjc_is_rmorphism. +Canonical conjc_linear := AddLinear conjc_is_scalable. + +Lemma conjcK : involutive (@conjc R_ringType). +Proof. by move=> [a b] /=; rewrite opprK. Qed. + +Lemma mulcJ_ge0 (x : R[i]) : 0 <= x * x^*%C. +Proof. +by move: x=> [a b]; simpc; rewrite mulrC addNr eqxx addr_ge0 ?sqr_ge0. +Qed. + +Lemma conjc_real (x : R) : x%:C^* = x%:C. +Proof. by rewrite /= oppr0. Qed. + +Lemma ReJ_add (x : R[i]) : (Re x)%:C = (x + x^*%C) / 2%:R. +Proof. +case: x => a b; simpc; rewrite [0 ^+ 2]mul0r addr0 /=. +rewrite -!mulr2n -mulr_natr -mulrA [_ * (_ / _)]mulrA. +by rewrite divff ?mulr1 // -natrM pnatr_eq0. +Qed. + +Lemma ImJ_sub (x : R[i]) : (Im x)%:C = (x^*%C - x) / 2%:R * 'i%C. +Proof. +case: x => a b; simpc; rewrite [0 ^+ 2]mul0r addr0 /=. +rewrite -!mulr2n -mulr_natr -mulrA [_ * (_ / _)]mulrA. +by rewrite divff ?mulr1 ?opprK // -natrM pnatr_eq0. +Qed. + +Lemma ger0_Im (x : R[i]) : 0 <= x -> Im x = 0. +Proof. by move: x=> [a b] /=; simpc => /andP [/eqP]. Qed. + +(* Todo : extend theory of : *) +(* - signed exponents *) + +Lemma conj_ge0 : forall x : R[i], (0 <= x ^* ) = (0 <= x). +Proof. by move=> [a b] /=; simpc; rewrite oppr_eq0. Qed. + +Lemma conjc_nat : forall n, (n%:R : R[i])^* = n%:R. +Proof. exact: rmorph_nat. Qed. + +Lemma conjc0 : (0 : R[i]) ^* = 0. +Proof. exact: (conjc_nat 0). Qed. + +Lemma conjc1 : (1 : R[i]) ^* = 1. +Proof. exact: (conjc_nat 1). Qed. + +Lemma conjc_eq0 : forall x : R[i], (x ^* == 0) = (x == 0). +Proof. by move=> [a b]; rewrite !eq_complex /= eqr_oppLR oppr0. Qed. + +Lemma conjc_inv: forall x : R[i], (x^-1)^* = (x^*%C )^-1. +Proof. exact: fmorphV. Qed. + +Lemma complex_root_conj (p : {poly R[i]}) (x : R[i]) : + root (map_poly conjc p) x = root p x^*. +Proof. by rewrite /root -{1}[x]conjcK horner_map /= conjc_eq0. Qed. + + +(* Lemma complex_algebraic_trans (T : comRingType) (toR : {rmorphism T -> R}) : *) +(* integralRange toR -> integralRange (real_complex R \o toR). *) +(* Proof. *) +(* set f := _ \o _ => R_integral [a b]. *) +(* have integral_real x : integralOver f (x%:C) by apply: integral_rmorph. *) +(* rewrite [_ +i* _]complexE. *) +(* apply: integral_add => //; apply: integral_mul => //=. *) +(* exists ('X^2 + 1). *) +(* by rewrite monicE lead_coefDl ?size_polyXn ?size_poly1 ?lead_coefXn. *) +(* by rewrite rmorphD rmorph1 /= ?map_polyXn rootE !hornerE -expr2 sqr_i addNr. *) +(* Qed. *) + +Lemma normc_def (z : R[i]) : `|z| = (sqrtr ((Re z)^+2 + (Im z)^+2))%:C. +Proof. by case: z. Qed. + +Lemma add_Re2_Im2 (z : R[i]) : ((Re z)^+2 + (Im z)^+2)%:C = `|z|^+2. +Proof. by rewrite normc_def -rmorphX sqr_sqrtr ?addr_ge0 ?sqr_ge0. Qed. + +Lemma addcJ (z : R[i]) : z + z^*%C = 2%:R * (Re z)%:C. +Proof. by rewrite ReJ_add mulrC mulfVK ?pnatr_eq0. Qed. + +Lemma subcJ (z : R[i]) : z - z^*%C = 2%:R * (Im z)%:C * 'i%C. +Proof. +rewrite ImJ_sub mulrCA mulrA mulfVK ?pnatr_eq0 //. +by rewrite -mulrA ['i%C * _]sqr_i mulrN1 opprB. +Qed. + +Lemma complex_real (a b : R) : a +i* b \is Num.real = (b == 0). +Proof. +rewrite realE; simpc; rewrite [0 == _]eq_sym. +by have [] := ltrgtP 0 a; rewrite ?(andbF, andbT, orbF, orbb). +Qed. + +Lemma complex_realP (x : R[i]) : reflect (exists y, x = y%:C) (x \is Num.real). +Proof. +case: x=> [a b] /=; rewrite complex_real. +by apply: (iffP eqP) => [->|[c []//]]; exists a. +Qed. + +Lemma RRe_real (x : R[i]) : x \is Num.real -> (Re x)%:C = x. +Proof. by move=> /complex_realP [y ->]. Qed. + +Lemma RIm_real (x : R[i]) : x \is Num.real -> (Im x)%:C = 0. +Proof. by move=> /complex_realP [y ->]. Qed. + +End ComplexTheory. + + +Section ComplexClosedTheory. + + +(* Lemma complexiE : 'i%C = 'i%R :> R[i]. *) +(* Proof. by []. Qed. *) + +(* Lemma complexRe (x : R[i]) : (Re x)%:C = 'Re x. *) +(* Proof. *) +(* rewrite {1}[x]Crect raddfD /= mulrC ReiNIm rmorphB /=. *) +(* by rewrite ?RRe_real ?RIm_real ?Creal_Im ?Creal_Re // subr0. *) +(* Qed. *) + +(* Lemma complexIm (x : R[i]) : (Im x)%:C = 'Im x. *) +(* Proof. *) +(* rewrite {1}[x]Crect raddfD /= mulrC ImiRe rmorphD /=. *) +(* by rewrite ?RRe_real ?RIm_real ?Creal_Im ?Creal_Re // add0r. *) +(* Qed. *) + +(* End ComplexClosedTheory *) +(* . *) + + +Import ComplexField. + +(* Local Notation sgr := Num.sg. *) +(* Local Notation sqrtr := Num.sqrt. *) +Local Notation C := R[i]. +Local Open Scope complex_scope. (* *) +(* Notation Re:= Re. *) +(* Notation Im:= (complex.Im). *) + + + + +(*Adapting lemma eq_complex from complex.v, which was done in boolean style*) +Lemma eqE_complex : forall (x y : C), (x = y) = ((Re x = Re y) /\ (Im x = Im y)). +Proof. + move => [a b] [c d]; apply : propositional_extensionality ; split. + by move => -> ; split. + by case => //= -> ->. +Qed. + +Lemma Re0 : Re 0 = 0 :> R. +Proof. by []. Qed. + +Lemma Im0 : Im 0 = 0 :> R. +Proof. by []. Qed. + +Lemma ReIm_eq0 (x : C) : (x=0) = ((Re x = 0)/\(Im x = 0)). +Proof. + by rewrite -[in Re x= _]Re0 -Im0 -eqE_complex. +Qed. + +Lemma normc0 : normc 0 = 0 :> R . +Proof. + by rewrite /normc //= expr0n //= add0r sqrtr0. +Qed. + +Lemma normc_r (x : R) : normc (x%:C) = normr (x). +Proof. by rewrite /normc/= expr0n //= addr0 sqrtr_sqr. Qed. + + +Lemma normc_i (x : R) : normc (x*i) = normr (x). +Proof. by rewrite /normc/= expr0n //= add0r sqrtr_sqr. Qed. + +Lemma normcN1 : normc (-1%:C) = 1 :> R. +Proof. + by rewrite /normc/= oppr0 expr0n addr0 -signr_odd expr0 sqrtr1. +Qed. + +Lemma realtocomplex_additive : forall x y : R, (x + y)%:C = x%:C + y%:C. +Proof. + move => x y ; rewrite -!complexr0 eqE_complex //=. + by split ; last by rewrite addr0. +Qed. + + + +Lemma real_complex_inv : forall x : R, x%:C^-1 = (x^-1)%:C. +Proof. Admitted. + +Lemma Im_inv : ('i%C)^-1 = (-1*i) :> C. +Proof. Admitted. + +Lemma invcM : forall x y : C, (x*y)^-1 = x^-1 * y^-1. (*Maybe another lemma is doing that, or invrM *) +Proof. Admitted. + +Lemma Im_mul : forall x : R, (x*i) = (x%:C * 'i%C). +Proof. by move => x ; simpc. Qed. + +Lemma normcD : forall ( x y : C), normc (x+y) <= (normc x + normc y). +Proof. + by move => x y ; rewrite -lecR realtocomplex_additive ; apply :lec_normD . +Qed. + +Lemma normcZ : forall (l : R) (x : C), normc (l *: x) = `|l| * (normc x). +Proof. + move => l [a b] ; rewrite /normc //= !exprMn. + rewrite -mulrDr sqrtrM ; last by rewrite sqr_ge0. + by rewrite sqrtr_sqr. +Qed. + +Lemma scalecr : forall w : C^o, forall r : R, (r *: w = r%:C *: w). +Proof. by move => [a b ] r ; rewrite eqE_complex //= ; split ; simpc. Qed. + +About AbsRing_ball. + + +Section C_Rnormed. + + (* Uniform.mixin_of takes a locally but does not expect a TopologicalType, which is inserted in the Uniform.class_of *) + (* Whereas NormedModule.mixin_of asks for a Uniform.mixin_of loc *) + +(*Context (K : absRingType). Nor working with any K, how to close the real scope ? Do it before ? *) + + +Program Definition uniformmixin_of_normaxioms (V : lmodType R) (norm : V -> R) + (ax1 : forall x y : V, norm (x + y) <= norm x + norm y) + ( ax2 : forall (l : R) (x : V), norm (l *: x) = `|l| * (norm x)) + ( ax4 : forall x : V, norm x = 0 -> x = 0 ) : Uniform.mixin_of (locally_ (ball_ norm)) + := @Uniform.Mixin V (locally_ (ball_ norm)) (ball_ norm) _ _ _ _. +Next Obligation. + move => V norm _ H _ ; rewrite /ball_ => x e. + have -> : x - x = 0 . by rewrite addrN. + suff -> : norm 0 = 0 by []. + have -> : 0 = 0 *: x by rewrite scale0r. + by rewrite H normr0 mul0r. +Qed. +Next Obligation. + move => V norm _ H _ ; rewrite /ball_ => x e e0. + have -> : x - e = (-1) *: (e-x) by rewrite -opprB scaleN1r. + by rewrite (H (-1) (e-x)) normrN1 mul1r. +Qed. +Next Obligation. + move => V norm H _ _ ; rewrite /ball_ => x y z e1 e2 normxy normyz. + by rewrite (subr_trans y) (ler_lt_trans (H _ _)) ?ltr_add. +Qed. +Next Obligation. by []. Qed. + +(*C as a R-lmodule *) + +Variable (R : rcfType). + +Definition C_RlmodMixin := complex_lmodMixin. (*R instead of R_rcfType is not working *) +(*LmodType is hard to use, not findable through Search and not checkable as abbreviation is not applied enough*) +Definition C_RlmodType := @LmodType R C C_RlmodMixin. + +(* C as a uniformtype *) +Definition C_pointedType := PointedType C 0. +Canonical C_pointedType. +Definition C_filteredType := FilteredType C C (locally_ (ball_ (@normc R))). +Canonical C_filteredType. +(*Are we sure that the above is canonical *) + +Program Definition C_RuniformMixin := @uniformmixin_of_normaxioms C_RlmodType (@normc R) normcD normcZ (@eq0_normc R). +Definition C_RtopologicalMixin := topologyOfBallMixin C_RuniformMixin. +Definition C_RtopologicalType := TopologicalType C_filteredType C_RtopologicalMixin. +Definition C_RuniformType := @UniformType C_RtopologicalType C_RuniformMixin. + + +Program Definition C_RnormedMixin + := @NormedModMixin R_absRingType C_RlmodType _ C_RuniformMixin (@normc R) normcD normcZ _ (@eq0_normc R) . +Next Obligation. by []. Qed. + + +Definition C_RnormedType : normedModType R := @NormedModType R C_RuniformType C_RnormedMixin. +End C_Rnormed. + + +Section C_absRing. + + Definition C_AbsRingMixin := @AbsRingMixin (complex_ringType R_rcfType) (@normc R_rcfType) normc0 normcN1 normcD (@normcM R_rcfType ) (@eq0_normc R_rcfType). + Definition C_absRingType := AbsRingType C C_AbsRingMixin. + Canonical C_absRingType. + + + + Definition C_lmodtype := @LmodType C C C_AbsRingMixin. Definition lmodType := @GRing.Lmodule.Pack K phK cT xclass + Canonical C_absRingType. + Definition C_topologicalType := [topologicalType of C for C_absRingType]. + Canonical C_topologicalType. + Definition C_uniformType := [uniformType of C for C_absRingType]. + Canonical C_uniformType. + Definition Co_pointedType := [pointedType of C^o for C_absRingType]. + (*Canonical Co_pointedType.*) + Locate Ro_pointedType. + Definition Co_filteredType := [filteredType C^o of C^o for C_absRingType]. + Definition Co_topologicalType := [topologicalType of C^o for C_absRingType]. + Definition Co_uniformType := [uniformType of C^o for C_absRingType]. + Definition Co_normedType := AbsRing_NormedModType C_absRingType. + (*Canonical Co_normedType.*) + (*Why is this Canonical, when the normed type on Ro is defined for R of the reals ? *) + + Lemma absCE : forall x : C, `|x|%real = normc x. + Proof. by []. Qed. + + + Lemma absring_real_complex : forall r: R, forall x : R, AbsRing_ball 0 r x -> (@AbsRing_ball C_absRingType 0%:C r x%:C). + Proof. + move => r x ballrx. + rewrite /AbsRing_ball /ball_ absCE. + rewrite addrC addr0 -scaleN1r normcZ normrN1 mul1r normc_r. + move : ballrx ; rewrite /AbsRing_ball /ball_ absRE. + by rewrite addrC addr0 normrN. + Qed. + + + Lemma absring_real_Im : forall r: R, forall x : R, AbsRing_ball 0 r x -> (@AbsRing_ball C_absRingType 0%:C r x*i). + Proof. + move => r x ballrx. + rewrite /AbsRing_ball /ball_ absCE. + rewrite addrC addr0 -scaleN1r normcZ normrN1 mul1r normc_i. + move : ballrx ; rewrite /AbsRing_ball /ball_ absRE. + by rewrite addrC addr0 normrN. + Qed. + Check scalec. + Unset Printing Notations. + (* Lemma scalei_muli : forall z : C^o, (mulc 'i z) = ('i *: z). *) + (* Proof. *) + (* by []. *) + (* Qed. *) + + Lemma iE : 'i%C = 'i :> C. + Proof. by []. Qed. + +End C_absRing. + +Section Holomorphe. + +Print differentiable_def. +(* used in derive.v, what does center means*) +(*CoInductive +differentiable_def (K : absRingType) (V W : normedModType K) (f : V -> W) +(x : filter_on V) (phF : phantom (set (set V)) x) : Prop := + DifferentiableDef : continuous 'd f x /\ f = (cst (f (lim x)) + 'd f x) \o + center (lim x) +o_x center (lim x) -> differentiable_def f phF *) +(*Diff is defined from any normedmodule of any absringtype, so C is a normedmodul on itsself *) +(*Vague idea that this should work, as we see C^o as a vector space on C and not R*) + + +(*Important : differentiable in derive.v, means continuoulsy differentiable, not just that the limit exists. *) +(*derivable concerns only the existence of the derivative *) + +Definition holomorphic (f : Co_normedType -> Co_normedType) c := forall v, +cvg ((fun h => h^-1 *: ((f \o shift c) (h *: v) - f c)) @ locally' (0 : Co_normedType)). + +Definition complex_realfun (f : C^o -> C^o) : C_RnormedType -> C_RnormedType := f. + +Definition complex_Rnormed_absring : C_RnormedType -> C^o := id. (* Coercion ? *) (*Avec C tout seul au lieu de C_absRIng ça devrait passer *) + + +(* Variable ( h : C_RnormedType -> C_RnormedType) (x : C_RnormedType). *) + +(* Check ('D_x h 0). (*This has a weird type *) *) + +Definition CauchyRiemanEq_R2 (f : C_RnormedType -> C_RnormedType) c := + let u := (fun c => Re ( f c)): C_RnormedType -> R^o in + let v:= (fun c => Im (f c)) : C_RnormedType -> R^o in + (* ('D_(1%:C) u = 'D_('i) v) /\ ('D_('i) u = 'D_(1%:C) v). *) + (((derive u c (1%:C)) = + (derive v c ('i))) /\ ((derive v c (1%:C)) = -(derive u c ('i)))). +Check derive. (*derive is explicitely for R normed spaces *) +Check derivable. + +Definition deriveC (V W : normedModType C)(f : V -> W) c v := + lim ((fun h => h^-1 *: ((f \o shift c) (h *: v) - f c)) @ locally' (0 : C^o)). + + +Definition CauchyRiemanEq (f : C -> C) z:= + 'i * lim ((fun h : R => h^-1 *: ((f \o shift z) (h *: 1%:C) - f z)) @ locally' (0 : R^o)) = + lim ((fun h : R => h^-1 *: ((f \o shift z) (h *: 'i%C) - f z)) @ locally' (0 : R^o)). + + +Lemma eqCr (R : rcfType) (r s : R) : (r%:C == s%:C) = (r == s). +Proof. exact: (inj_eq (@complexI _)). Qed. + +Lemma eqCI (R : rcfType) (r s : R) : (r*i == s*i) = (r == s). +Proof. Admitted. + + +(*Lemma lim_trans (T : topologicalType) (F : set (set T)) (G : set (set T)) (l : T) : ( F `=>` G ) -> (G --> l) -> ( F --> l). + move => FG Gl A x. + Search "lim" "trans". + *) + +Lemma cvg_translim (T : topologicalType) (F G: set (set T)) (l :T) : + F `=>` G -> (G --> l) -> (F --> l). +Proof. + move => FG Gl. apply : cvg_trans. + exact : FG. + exact : Gl. +Qed. + + +Lemma cvg_scaler (K : absRingType) (V : normedModType K) (T : topologicalType) + (F : set (set T)) (H :Filter F) (f : T -> V) (k : K) : + cvg (f @ F) -> cvg ((k \*: f) @ F ). +Proof. + by move => /cvg_ex [l H0] ; apply : cvgP ; apply :(@cvgZr _ _ _ F _ f k l). +Qed. + +About cvgZr. + + +Lemma limin_scaler (K : absRingType) (V : normedModType K) (T : topologicalType) + (F : set (set T)) (FF :Filter F) (f : T -> V) (k : K) : + cvg(f@F) -> k *: lim (f @ F) = lim ((k \*: f) @ F ). +Proof. + move => /cvg_ex [l H]. + (*rewrite (cvg_lim H). *) +(* The LHS of (cvg_lim H) *) +(* (lim (f @ F)) *) +(* matches but type classes inference fails *) +(* Check (cvg_lim (@cvgZr K V T F FF f k l H)). *) + Admitted. + + +(*this could be done for scale also ... *) + +(*I needed filter_of_filterE to make things easier - looked a long time of it as I was lookin for a [filter of lim]* instead of a [filter of filter]*) + +(*There whould be a lemma analogous to [filter of lim] to ease the search *) + +(* + +Lemma filter_of_filterE {T : Type} (F : set (set T)) : [filter of F] = F. +Proof. by []. Qed. + +Lemma locally_filterE {T : Type} (F : set (set T)) : locally F = F. +Proof. by []. Qed. + +Module Export LocallyFilter. +Definition locally_simpl := (@filter_of_filterE, @locally_filterE). +End LocallyFilter. + +Definition cvg_to {T : Type} (F G : set (set T)) := G `<=` F. +Notation "F `=>` G" := (cvg_to F G) : classical_set_scope. +Lemma cvg_refl T (F : set (set T)) : F `=>` F. +Proof. exact. Qed. + +Lemma cvg_trans T (G F H : set (set T)) : + (F `=>` G) -> (G `=>` H) -> (F `=>` H). +Proof. by move=> FG GH P /GH /FG. Qed. + +Notation "F --> G" := (cvg_to [filter of F] [filter of G]) : classical_set_scope. +Definition type_of_filter {T} (F : set (set T)) := T. + +Definition lim_in {U : Type} (T : filteredType U) := + fun F : set (set U) => get (fun l : T => F --> l). +Notation "[ 'lim' F 'in' T ]" := (@lim_in _ T [filter of F]) : classical_set_scope. +Notation lim F := [lim F in [filteredType _ of @type_of_filter _ [filter of F]]]. +Notation "[ 'cvg' F 'in' T ]" := (F --> [lim F in T]) : classical_set_scope. +Notation cvg F := [cvg F in [filteredType _ of @type_of_filter _ [filter of F]]]. +*) + + + +Lemma holo_derivable (f : C^o -> C^o) c : ((holomorphic f c)) + -> (forall v : C, derivable (complex_realfun f) c v). +Proof. + move => H; rewrite /derivable => v. + move : (H v) => /cvg_ex [l H0] {H}. (* eapply*) + apply : (cvgP (l := l)). + - have eqnear0 : {near (@locally' R_topologicalType 0), + (fun h : C_absRingType => h^-1 *: ((f \o shift c) (h *: (complex_Rnormed_absring v)) - f c)) + \o (real_complex R) =1 + (fun h0 : R_absRingType => h0^-1 *: ((complex_realfun f \o shift c) (h0 *: v ) + - complex_realfun f c)) }. + exists 1 ; first by [] ; move => h _ neq0h //=; rewrite real_complex_inv -scalecr. + by apply : (scalerI (neq0h)) ; rewrite !scalerA //= (divff neq0h) !scale1r //= -scalecr. + pose subsetfilters:= (cvg_eq_loc eqnear0). + apply : (@cvg_trans _ ( (fun h : C_absRingType => h^-1 *: ((f \o shift c) (h *: (complex_Rnormed_absring v)) - f c)) \o (real_complex R) @ (@locally' R_topologicalType 0))). + exact : (subsetfilters (@locally'_filter R_topologicalType 0)). +- unshelve apply : cvg_comp. + exact (locally' 0%:C). +- move => //= A [r [leq0r ballrA]] ; exists r ; first by []. + move => b ballrb neqb0. + have ballCrb : (AbsRing_ball 0%:C r b%:C). + by apply : absring_real_complex. + have bneq0C : (b%:C != 0%:C) by move : neqb0 ; apply : contra ; rewrite eqCr. + by apply : (ballrA b%:C ballCrb bneq0C). +by []. +Qed. + +Lemma holo_CauchyRieman (f : C^o -> C^o) c : (holomorphic f c) -> (CauchyRiemanEq f c). +Proof. + move => H. (* move : (H 1%:C) => /cvg_ex [l H0] {H}. *) + (* move : l H0 ; rewrite filter_of_filterE => l H0. *) + pose quotC := (fun h : C_absRingType => h^-1 *: ((f \o shift c) (h * 1%:C) - f c)). + pose quotR := (fun h : R_absRingType => h^-1 *: ((f \o shift c) (h *: 1%:C ) - f c)). + pose quotiR := (fun (h : R) => h^-1 *: ((f \o shift c) (h *: 'i%C) - f c)). + have eqnear0x : {near (@locally' R_topologicalType 0), quotC \o ( fun h => h *: 1%:C) =1 quotR }. + exists 1 ; first by [] ; move => h _ _ //= ; simpc. + by rewrite /quotC /quotR real_complex_inv -scalecr ; simpc. + pose subsetfiltersx := (cvg_eq_loc eqnear0x). + rewrite /CauchyRiemanEq. + have -> : lim (quotR @ (@locally' R_topologicalType 0)) + = lim (quotC @ (@locally' C_topologicalType 0) ). + apply: (@cvg_map_lim _ _ _ (@locally' R_topologicalType 0) _ _ (lim (quotC @ (@locally' C_topologicalType 0) ))). + suff : quotR @ (@locally' R_topologicalType 0) `=>` (quotC @ (@locally' C_topologicalType 0)). + by move => H1 ; apply : (cvg_translim H1) ; exact : H. + apply : cvg_trans. + - exact : (subsetfiltersx (@locally'_filter R_topologicalType 0)). + move => {subsetfiltersx eqnear0x}. + - unshelve apply : cvg_comp. + (*just showing that linear maps preserve balls - general lemma ? *) + - exact (@locally' C_topologicalType 0). + - move => A //= [r leq0r] absringrA. + exists r ; first by []. + move => h absrh hneq0 ; simpc. + apply : (absringrA h%:C). + - by apply : absring_real_complex. + - by rewrite eqCr . + by []. + have eqnear0y : {near (@locally' R_topologicalType 0), 'i \*:quotC \o ( fun h => h *: 'i%C) =1 + quotiR }. + exists 1 ; first by [] ; move => h _ _ //= ; simpc . rewrite /quotC /quotiR (Im_mul h) invcM. + rewrite scalerA real_complex_inv Im_inv !scalecr; simpc ; rewrite (Im_mul h). + by rewrite !real_complexE. + pose subsetfiltersy := (cvg_eq_loc eqnear0y). + have <- : lim (quotiR @ (@locally' R_topologicalType 0)) + = 'i * lim (quotC @ (@locally' C_topologicalType 0)). + have -> : 'i * lim (quotC @ (@locally' C_topologicalType 0)) + = lim ('i \*: quotC @ (@locally' C_topologicalType 0)). + rewrite scalei_muli ; rewrite (limin_scaler _ ('i) ). + - by []. + - exact : H. + apply : (@cvg_map_lim _ _ _ (@locally' R_topologicalType 0) _ _ (lim ('i \*:quotC @ (@locally' C_topologicalType 0) ))). + suff : quotiR @ (@locally' R_topologicalType 0) + `=>` ('i \*: quotC @ (@locally' C_topologicalType 0)). + move => H1 ; apply : (cvg_translim H1) . + by apply :(@cvg_scaler _ _ _ _ _ quotC ('i) ) ; exact : H. + apply : cvg_trans. + - apply : (subsetfiltersy (@locally'_filter R_topologicalType 0)). + move => {subsetfiltersx eqnear0x}. + - unshelve apply : cvg_comp. + - exact (@locally' C_topologicalType 0). + - move => A //= [r leq0r] absringrA. + exists r ; first by []. + move => h absrh hneq0 ; simpc. + apply : (absringrA h*i). + - by apply : absring_real_Im. + - by rewrite eqCI. + rewrite filter_of_filterE. + by []. + by []. +Qed. + + +Theorem CauchyRiemann (f : C^o -> C^o) c: ((holomorphic f c)) + <-> (forall v : C, derivable (complex_realfun f) c v) /\ (CauchyRiemanEq f c). +Proof. +Admitted. + + + + +End Holomorphe. + + + + + + + +Module real_integral (M: INTEGRAL). +Import M. + +Parameter borel_real : sigma_algebra R. +Definition R_measurable := Measurable.Pack borel_real. +(* Notation AbsRingType T m := (@pack T _ m _ _ id _ id). *) +(* Canonical R_absRingType := AbsRingType R R_AbsRingMixin. *) +Canonical R_measurableType := @Measurable.Pack R borel_real. + + +Inductive borel_top (T : topologicalType) : set (set T) := + | borel_open : forall A, open A -> borel_top A + | borel_union : forall ( F : nat -> set T ), + (forall n , borel_top (F n)) -> + borel_top ( \bigcup_n (F n)) + + | borel_compl : forall A, borel_top (~`A) -> borel_top A. + + +Lemma borel_measurable : forall A : set R, borel_top A -> @measurable R_measurable A. +Admitted. + +Variable lebesgue : set R -> Rbar. + + +Record path (T : topologicalType) := Path { + base : R -> T ; + cont : forall x : R, `|x| <= 1 -> (base @ x --> base x ) }. + +Check base. + (*Local Coercion base T : path T >-> (R -> T). J'arrive pas à faire une coercion *) + +Definition segment01 := fun (x : R) => is_true (`|x| <= 1 ). + +Definition integral_path (T : topologicalType) (p : path T) (f : T -> Rbar) := integral lebesgue (segment01) (Basics.compose f (base p)). + + +End real_integral. From e3289d549168fefcbf4a04c1801fe9a46ae88d0e Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 18 Sep 2019 16:50:13 +0200 Subject: [PATCH 03/11] holomorphic is derivable, holomorphic implies Cauchy-Riemann --- theories/cauchyetoile.v | 463 +++++++++++------- theories/newcomplex.v | 1026 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 1303 insertions(+), 186 deletions(-) create mode 100644 theories/newcomplex.v diff --git a/theories/cauchyetoile.v b/theories/cauchyetoile.v index e21e6c1937..02d848d7da 100644 --- a/theories/cauchyetoile.v +++ b/theories/cauchyetoile.v @@ -4,14 +4,10 @@ From mathcomp Require Import ssreflect ssrfun ssrbool. From mathcomp Require Import ssrnat eqtype choice fintype bigop ssralg ssrnum. From mathcomp Require Import complex. From mathcomp Require Import boolp reals Rstruct Rbar derive. -Require Import classical_sets posnum topology normedtype landau integral. +Require Import classical_sets posnum topology normedtype landau integral. - -(*TODO : Definition integrale sur chemin et segment, holomorhpe, ouvert étoilé *) -(* TODO : cloner depuis integrale et commiter. Admettre la mesure sur R *) - - -(*Pour distinguer fonctions mesurables et integrables, utiliser des structures comme posrel. *) +(*Pour distinguer fonctions mesurables et integrables, +utiliser des structures comme posrel. *) Import GRing.Theory Num.Theory ComplexField Num.Def. Local Open Scope ring_scope. Local Open Scope classical_set_scope. @@ -31,7 +27,8 @@ Local Open Scope complex_scope. Notation Im:= (complex.Im). -(*Adapting lemma eq_complex from complex.v, which was done in boolean style*) + (*Adapting lemma eq_complex from complex.v, + which was done in boolean style*) Lemma eqE_complex : forall (x y : C), (x = y) = ((Re x = Re y) /\ (Im x = Im y)). Proof. move => [a b] [c d]; apply : propositional_extensionality ; split. @@ -55,6 +52,9 @@ Local Open Scope complex_scope. by rewrite /normc //= expr0n //= add0r sqrtr0. Qed. + Lemma normcN ( x : C) : normc (-x) = (normc x). + Admitted. + Lemma normc_r (x : R) : normc (x%:C) = normr (x). Proof. by rewrite /normc/= expr0n //= addr0 sqrtr_sqr. Qed. @@ -69,21 +69,28 @@ Local Open Scope complex_scope. Lemma realtocomplex_additive : forall x y : R, (x + y)%:C = x%:C + y%:C. Proof. + (*real_complex_additive*) move => x y ; rewrite -!complexr0 eqE_complex //=. by split ; last by rewrite addr0. Qed. - - - Lemma real_complex_inv : forall x : R, x%:C^-1 = (x^-1)%:C. - Proof. Admitted. + Lemma real_complex_inv : forall x : R, x%:C^-1 = (x^-1)%:C. + Proof. + Search _ (rmorphism _). + Admitted. Lemma Im_inv : ('i%C)^-1 = (-1*i) :> C. Proof. Admitted. - Lemma invcM : forall x y : C, (x*y)^-1 = x^-1 * y^-1. (*Maybe another lemma is doing that, or invrM *) + Lemma invcM : forall x y : C, (x*y)^-1 = x^-1 * y^-1. + (*Maybe another lemma is doing that, or invrM *) Proof. Admitted. +Lemma scale_inv : forall (h : R) (v : C), (h*:v)^-1 = h^-1 *: v^-1. + (*Maybe another lemma is doing that, or invrM *) + Proof. Admitted. + + Lemma Im_mul : forall x : R, (x*i) = (x%:C * 'i%C). Proof. by move => x ; simpc. Qed. @@ -100,9 +107,10 @@ Local Open Scope complex_scope. Qed. Lemma scalecr : forall w : C^o, forall r : R, (r *: w = r%:C *: w). - Proof. by move => [a b ] r ; rewrite eqE_complex //= ; split ; simpc. Qed. + Proof. by move => [a b ] r; rewrite eqE_complex //=; split; simpc. Qed. + Section C_Rnormed. (* Uniform.mixin_of takes a locally but does not expect a TopologicalType, which is inserted in the Uniform.class_of *) @@ -143,8 +151,10 @@ Section C_Rnormed. Definition C_filteredType := FilteredType C C (locally_ (ball_ (@normc R_rcfType))). Canonical C_filteredType. (*Are we sure that the above is canonical *) + - Program Definition C_RuniformMixin := @uniformmixin_of_normaxioms C_RlmodType (@normc R_rcfType) normcD normcZ (@eq0_normc R_rcfType). + Program Definition C_RuniformMixin := + @uniformmixin_of_normaxioms C_RlmodType (@normc R_rcfType) normcD normcZ (@eq0_normc R_rcfType). Definition C_RtopologicalMixin := topologyOfBallMixin C_RuniformMixin. Definition C_RtopologicalType := TopologicalType C_filteredType C_RtopologicalMixin. Definition C_RuniformType := @UniformType C_RtopologicalType C_RuniformMixin. @@ -156,34 +166,58 @@ Section C_Rnormed. Definition C_RnormedType : normedModType R := @NormedModType R C_RuniformType C_RnormedMixin. + + + Lemma scalecAl : forall (h : R) ( x y : C_RnormedType), + h *: ( x * y) = h *: x * y. + Proof. move => h [a b] [c d]. simpc. Admitted. + + + Definition C_RLalg := LalgType R C_RlmodType scalecAl. + End C_Rnormed. -Section C_absRing. + - Definition C_AbsRingMixin := @AbsRingMixin (complex_ringType R_rcfType) (@normc R_rcfType) normc0 normcN1 normcD (@normcM R_rcfType ) (@eq0_normc R_rcfType). +Section C_absRing. - - + Definition C_AbsRingMixin := @AbsRingMixin (complex_ringType R_rcfType) + (@normc R_rcfType) normc0 normcN1 normcD (@normcM R_rcfType ) + (@eq0_normc R_rcfType). Definition C_absRingType := AbsRingType C C_AbsRingMixin. Canonical C_absRingType. Definition C_topologicalType := [topologicalType of C for C_absRingType]. - Canonical C_topologicalType. + Canonical C_topologicalType. Definition C_uniformType := [uniformType of C for C_absRingType]. Canonical C_uniformType. Definition Co_pointedType := [pointedType of C^o for C_absRingType]. - (*Canonical Co_pointedType.*) - Locate Ro_pointedType. Definition Co_filteredType := [filteredType C^o of C^o for C_absRingType]. Definition Co_topologicalType := [topologicalType of C^o for C_absRingType]. + + Canonical Zmod_topologicalType ( K : absRingType) + (V : normedModType K):= + [topologicalType of [zmodType of V]]. + Definition Co_uniformType := [uniformType of C^o for C_absRingType]. Definition Co_normedType := AbsRing_NormedModType C_absRingType. - (*Canonical Co_normedType.*) - (*Why is this Canonical, when the normed type on Ro is defined for R of the reals ? *) + Canonical C_normedType := [normedModType C^o of C for Co_normedType]. + (*C is convertible to C^o *) + + Canonical R_normedType := [normedModType R of R for [normedModType R of R^o]]. + + Canonical absRing_normedType (K : absRingType) := [normedModType K^o of K for (AbsRing_NormedModType K)]. - Lemma absCE : forall x : C, `|x|%real = normc x. + Lemma abs_normE : forall ( K : absRingType) (x : K), `|x|%real = `|[x]|. Proof. by []. Qed. + (*Delete absCE and adapt from abs_normE *) + Lemma absCE : forall x : C, `|x|%real = (normc x). + Proof. by []. Qed. - Lemma absring_real_complex : forall r: R, forall x : R, AbsRing_ball 0 r x -> (@AbsRing_ball C_absRingType 0%:C r x%:C). + Lemma normCR : forall x : R, `|[x%:C]| = `|x|%real. + Proof. Admitted. + + Lemma absring_real_complex : forall r: R, forall x : R, AbsRing_ball 0 r x -> + (AbsRing_ball 0%:C r x%:C). Proof. move => r x ballrx. rewrite /AbsRing_ball /ball_ absCE. @@ -193,7 +227,8 @@ Section C_absRing. Qed. - Lemma absring_real_Im : forall r: R, forall x : R, AbsRing_ball 0 r x -> (@AbsRing_ball C_absRingType 0%:C r x*i). + Lemma absring_real_Im : forall r: R, forall x : R, AbsRing_ball 0 r x -> + (AbsRing_ball 0%:C r x*i). Proof. move => r x ballrx. rewrite /AbsRing_ball /ball_ absCE. @@ -208,7 +243,10 @@ Section C_absRing. Qed. Lemma iE : 'i%C = 'i :> C. - Proof. by []. Qed. + Proof. by []. Qed. + + Lemma scaleC_mul : forall (w v : C^o), (v *: w = v * w). + Proof. by []. Qed. End C_absRing. @@ -220,27 +258,25 @@ Print differentiable_def. differentiable_def (K : absRingType) (V W : normedModType K) (f : V -> W) (x : filter_on V) (phF : phantom (set (set V)) x) : Prop := DifferentiableDef : continuous 'd f x /\ f = (cst (f (lim x)) + 'd f x) \o - center (lim x) +o_x center (lim x) -> differentiable_def f phF *) -(*Diff is defined from any normedmodule of any absringtype, so C is a normedmodul on itsself *) + center (lim x) +o_x center (lim x) -> differentiable_def f phF *) +(*Diff is defined from any normedmodule of any absringtype, + so C is a normedmodul on itsself *) (*Vague idea that this should work, as we see C^o as a vector space on C and not R*) -(*Important : differentiable in derive.v, means continuoulsy differentiable, not just that the limit exists. *) +(*Important : differentiable in derive.v, means continuoulsy differentiable, +not just that the limit exists. *) (*derivable concerns only the existence of the derivative *) -Definition holomorphic (f : Co_normedType -> Co_normedType) c := forall v, -cvg ((fun h => h^-1 *: ((f \o shift c) (h *: v) - f c)) @ locally' (0 : Co_normedType)). - -Definition complex_realfun (f : C^o -> C^o) : C_RnormedType -> C_RnormedType := f. + Definition holomorphic (f : C^o -> C^o) (c: C^o) := + cvg ((fun (h:C^o)=> h^-1 *: ((f \o shift c) (h) - f c)) @ (locally' 0)). -Definition complex_Rnormed_absring : C_RnormedType -> C^o := id. (* Coercion ? *) (*Avec C tout seul au lieu de C_absRIng ça devrait passer *) + Definition complex_realfun (f : C^o -> C^o) : C_RnormedType -> C_RnormedType := f. + Arguments complex_realfun _ _ /. + Definition complex_Rnormed_absring : C_RnormedType -> C^o := id. -(* Variable ( h : C_RnormedType -> C_RnormedType) (x : C_RnormedType). *) - -(* Check ('D_x h 0). (*This has a weird type *) *) - -Definition CauchyRiemanEq_R2 (f : C_RnormedType -> C_RnormedType) c := + Definition CauchyRiemanEq_R2 (f : C_RnormedType -> C_RnormedType) c := let u := (fun c => Re ( f c)): C_RnormedType -> R^o in let v:= (fun c => Im (f c)) : C_RnormedType -> R^o in (* ('D_(1%:C) u = 'D_('i) v) /\ ('D_('i) u = 'D_(1%:C) v). *) @@ -248,149 +284,137 @@ Definition CauchyRiemanEq_R2 (f : C_RnormedType -> C_RnormedType) c := (derive v c ('i))) /\ ((derive v c (1%:C)) = -(derive u c ('i)))). -Definition deriveC (V W : normedModType C)(f : V -> W) c v := - lim ((fun h => h^-1 *: ((f \o shift c) (h *: v) - f c)) @ locally' (0 : C^o)). + Definition deriveC (V W : normedModType C)(f : V -> W) c v := + lim ((fun (h: C^o) => h^-1 *: ((f \o shift c) (h *: v) - f c)) @ locally' 0). -Definition CauchyRiemanEq (f : C -> C) z:= - 'i * lim ((fun h : R => h^-1 *: ((f \o shift z) (h *: 1%:C) - f z)) @ locally' (0 : R^o)) = - lim ((fun h : R => h^-1 *: ((f \o shift z) (h *: 'i%C) - f z)) @ locally' (0 : R^o)). + Definition CauchyRiemanEq (f : C -> C) z := + 'i * lim ((fun h : R => h^-1 *: ((f \o shift z) (h *: 1%:C) - f z)) @ locally' 0) = + lim ((fun h : R => h^-1 *: ((f \o shift z) (h *: 'i%C) - f z)) @ locally' 0). -Lemma eqCr (R : rcfType) (r s : R) : (r%:C == s%:C) = (r == s). -Proof. exact: (inj_eq (@complexI _)). Qed. + Lemma eqCr (R : rcfType) (r s : R) : (r%:C == s%:C) = (r == s). + Proof. exact: (inj_eq (@complexI _)). Qed. -Lemma eqCI (R : rcfType) (r s : R) : (r*i == s*i) = (r == s). -Proof. Admitted. + Lemma eqCI (R : rcfType) (r s : R) : (r*i == s*i) = (r == s). + Proof. Admitted. -(*Lemma lim_trans (T : topologicalType) (F : set (set T)) (G : set (set T)) (l : T) : ( F `=>` G ) -> (G --> l) -> ( F --> l). +(*Lemma lim_trans (T : topologicalType) (F : set (set T)) +(G : set (set T)) (l : T) : ( F `=>` G ) -> (G --> l) -> ( F --> l). move => FG Gl A x. Search "lim" "trans". *) -Lemma cvg_translim (T : topologicalType) (F G: set (set T)) (l :T) : + Lemma cvg_translim (T : topologicalType) (F G: set (set T)) (l :T) : F `=>` G -> (G --> l) -> (F --> l). -Proof. + Proof. move => FG Gl. apply : cvg_trans. exact : FG. exact : Gl. -Qed. + Qed. -Lemma cvg_scaler (K : absRingType) (V : normedModType K) (T : topologicalType) + Lemma cvg_scaler (K : absRingType) (V : normedModType K) (T : topologicalType) (F : set (set T)) (H :Filter F) (f : T -> V) (k : K) : cvg (f @ F) -> cvg ((k \*: f) @ F ). -Proof. - by move => /cvg_ex [l H0] ; apply : cvgP ; apply :(@cvgZr _ _ _ F _ f k l). -Qed. + Proof. + by move => /cvg_ex [l H0] ; apply: cvgP; apply: cvgZr; apply: H0. + Qed. -About cvgZr. +(* Lemma cvg_proper_top (T : topologicalType) (F : set (set U)) (FF : Filter F) : *) +(* cvg F -> ProperFilter F. *) -Lemma limin_scaler (K : absRingType) (V : normedModType K) (T : topologicalType) - (F : set (set T)) (FF :Filter F) (f : T -> V) (k : K) : + Lemma limin_scaler (K : absRingType) (V : normedModType K) (T : topologicalType) + (F : set (set T)) (FF : ProperFilter F) (f : T -> V) (k : K) : cvg(f@F) -> k *: lim (f @ F) = lim ((k \*: f) @ F ). -Proof. - move => /cvg_ex [l H]. - (*rewrite (cvg_lim H). *) -(* The LHS of (cvg_lim H) *) -(* (lim (f @ F)) *) -(* matches but type classes inference fails *) -(* Check (cvg_lim (@cvgZr K V T F FF f k l H)). *) - Admitted. - + Proof. + move => cv. + symmetry. + by apply: cvg_lim; apply: cvgZr . + Qed. (*this could be done for scale also ... *) -(*I needed filter_of_filterE to make things easier - looked a long time of it as I was lookin for a [filter of lim]* instead of a [filter of filter]*) +(*I needed filter_of_filterE to make things easier - +looked a long time of it as I was looking for a [filter of lim]* + instead of a [filter of filter]*) (*There whould be a lemma analogous to [filter of lim] to ease the search *) -(* - -Lemma filter_of_filterE {T : Type} (F : set (set T)) : [filter of F] = F. -Proof. by []. Qed. - -Lemma locally_filterE {T : Type} (F : set (set T)) : locally F = F. -Proof. by []. Qed. - -Module Export LocallyFilter. -Definition locally_simpl := (@filter_of_filterE, @locally_filterE). -End LocallyFilter. - -Definition cvg_to {T : Type} (F G : set (set T)) := G `<=` F. -Notation "F `=>` G" := (cvg_to F G) : classical_set_scope. -Lemma cvg_refl T (F : set (set T)) : F `=>` F. -Proof. exact. Qed. - -Lemma cvg_trans T (G F H : set (set T)) : - (F `=>` G) -> (G `=>` H) -> (F `=>` H). -Proof. by move=> FG GH P /GH /FG. Qed. - -Notation "F --> G" := (cvg_to [filter of F] [filter of G]) : classical_set_scope. -Definition type_of_filter {T} (F : set (set T)) := T. - -Definition lim_in {U : Type} (T : filteredType U) := - fun F : set (set U) => get (fun l : T => F --> l). -Notation "[ 'lim' F 'in' T ]" := (@lim_in _ T [filter of F]) : classical_set_scope. -Notation lim F := [lim F in [filteredType _ of @type_of_filter _ [filter of F]]]. -Notation "[ 'cvg' F 'in' T ]" := (F --> [lim F in T]) : classical_set_scope. -Notation cvg F := [cvg F in [filteredType _ of @type_of_filter _ [filter of F]]]. -*) - - - -Lemma holo_derivable (f : C^o -> C^o) c : ((holomorphic f c)) - -> (forall v : C, derivable (complex_realfun f) c v). +Lemma holo_derivable (f : C^o -> C^o) c : holomorphic f c + -> (forall v:C , derivable (complex_realfun f) c v). Proof. - move => H; rewrite /derivable => v. - move : (H v) => /cvg_ex [l H0] {H}. (* eapply*) - apply : (cvgP (l := l)). - - have eqnear0 : {near (@locally' R_topologicalType 0), - (fun h : C_absRingType => h^-1 *: ((f \o shift c) (h *: (complex_Rnormed_absring v)) - f c)) - \o (real_complex R) =1 - (fun h0 : R_absRingType => h0^-1 *: ((complex_realfun f \o shift c) (h0 *: v ) - - complex_realfun f c)) }. - exists 1 ; first by [] ; move => h _ neq0h //=; rewrite real_complex_inv -scalecr. - by apply : (scalerI (neq0h)) ; rewrite !scalerA //= (divff neq0h) !scale1r //= -scalecr. - pose subsetfilters:= (cvg_eq_loc eqnear0). - apply : (@cvg_trans _ ( (fun h : C_absRingType => h^-1 *: ((f \o shift c) (h *: (complex_Rnormed_absring v)) - f c)) \o (real_complex R) @ (@locally' R_topologicalType 0))). - exact : (subsetfilters (@locally'_filter R_topologicalType 0)). -- unshelve apply : cvg_comp. - exact (locally' 0%:C). -- move => //= A [r [leq0r ballrA]] ; exists r ; first by []. - move => b ballrb neqb0. - have ballCrb : (AbsRing_ball 0%:C r b%:C). - by apply : absring_real_complex. - have bneq0C : (b%:C != 0%:C) by move : neqb0 ; apply : contra ; rewrite eqCr. - by apply : (ballrA b%:C ballCrb bneq0C). -by []. -Qed. - -Lemma holo_CauchyRieman (f : C^o -> C^o) c : (holomorphic f c) -> (CauchyRiemanEq f c). + move => /cvg_ex [l H]; rewrite /derivable => v. + rewrite /type_of_filter /= in l H. + set ff : C_RnormedType -> C_RnormedType := f. + set quotR := (X in (X @ locally' 0)). + pose mulv (h :R):= (h *:v). + pose quotC (h : C) : C^o := h^-1 *: ((f \o shift c) (h) - f c). + (* here f : C -> C does not work - +as if we needed C^o still for the normed structure*) + case : (EM (v = 0)). + - move => eqv0 ; apply (cvgP (l := (0:C))). + have eqnear0 : {near locally' (0:R), 0 =1 quotR}. + exists 1 => // h _ _ ; rewrite /quotR /shift eqv0. simpl. + by rewrite scaler0 add0r addrN scaler0. + (*addrN is too hard to find through Search *) + apply: cvg_translim. + - exact (cvg_eq_loc eqnear0). + - by apply : cst_continuous. + (*WARNING : cvg_cst from normedtype applies only to endofunctions + That should NOT be the case, as one could use it insteas of cst_continuous *) + - move/eqP => vneq0 ; apply : (cvgP (l := v *: l)). (*chainage avant et suff *) + have eqnear0 : {near (locally' (0 : R)), (v \*: quotC) \o mulv =1 quotR}. + exists 1 => // h _ neq0h //=; rewrite /quotC /quotR /mulv scale_inv. + rewrite scalerAl scalerCA -scalecAl mulrA -(mulrC v) mulfV. + rewrite mul1r; apply: (scalerI (neq0h)). + by rewrite !scalerA //= (divff neq0h). + by []. + have subsetfilters: quotR @ locally' 0 `=>` (v \*: quotC) \o mulv @locally' 0. + by exact: (cvg_eq_loc eqnear0). + apply: cvg_trans subsetfilters _. + unshelve apply : cvg_comp. + - exact (locally' (0:C)). + - move => //= A [r [leq0r ballrA]]. + exists (r / (`|[v]|)). + - apply : mulr_gt0 ; first by []. + by rewrite invr_gt0 normm_gt0. + - move => b; rewrite /AbsRing_ball /ball_ sub0r absRE normrN => ballrb neqb0. + have ballCrb : (AbsRing_ball 0 r (mulv b)). + rewrite /AbsRing_ball /ball_ sub0r absrN /mulv scalecr absrM abs_normE. + rewrite -ltr_pdivl_mulr. + - by rewrite normCR. + by rewrite abs_normE normm_gt0. + have bneq0C : (b%:C != 0%:C) by move: neqb0; apply: contra; rewrite eqCr. + by apply: (ballrA (mulv b) ballCrb); rewrite scaler_eq0; apply/norP; split. + suff : v \*: quotC @ locally' (0 : C) --> v *: l by []. + by apply: cvgZr ; rewrite /quotC. +Qed. + +Lemma holo_CauchyRieman (f : C^o -> C^o) c: (holomorphic f c) -> (CauchyRiemanEq f c). Proof. - move => H. (* move : (H 1%:C) => /cvg_ex [l H0] {H}. *) - (* move : l H0 ; rewrite filter_of_filterE => l H0. *) - pose quotC := (fun h : C_absRingType => h^-1 *: ((f \o shift c) (h * 1%:C) - f c)). - pose quotR := (fun h : R_absRingType => h^-1 *: ((f \o shift c) (h *: 1%:C ) - f c)). + move => H; rewrite /CauchyRiemanEq. + pose quotC := (fun h : C => h^-1 *: ((f \o shift c) (h) - f c)). + pose quotR := (fun h : R => h^-1 *: ((f \o shift c) (h *: 1%:C ) - f c)). pose quotiR := (fun (h : R) => h^-1 *: ((f \o shift c) (h *: 'i%C) - f c)). - have eqnear0x : {near (@locally' R_topologicalType 0), quotC \o ( fun h => h *: 1%:C) =1 quotR }. - exists 1 ; first by [] ; move => h _ _ //= ; simpc. - by rewrite /quotC /quotR real_complex_inv -scalecr ; simpc. + have eqnear0x : {near (locally' 0), quotC \o ( fun h => h *: 1%:C) =1 quotR}. + exists 1 ; first by [] ; move => h _ _ //=; simpc. + by rewrite /quotC /quotR real_complex_inv -scalecr; simpc. pose subsetfiltersx := (cvg_eq_loc eqnear0x). - rewrite /CauchyRiemanEq. - have -> : lim (quotR @ (@locally' R_topologicalType 0)) - = lim (quotC @ (@locally' C_topologicalType 0) ). - apply: (@cvg_map_lim _ _ _ (@locally' R_topologicalType 0) _ _ (lim (quotC @ (@locally' C_topologicalType 0) ))). - suff : quotR @ (@locally' R_topologicalType 0) `=>` (quotC @ (@locally' C_topologicalType 0)). - by move => H1 ; apply : (cvg_translim H1) ; exact : H. - apply : cvg_trans. - - exact : (subsetfiltersx (@locally'_filter R_topologicalType 0)). + have -> : lim (quotR @ (locally' 0)) + = lim (quotC @ (locally' 0)). + apply: cvg_map_lim. + suff: quotR @ (locally' 0) `=>` (quotC @ (locally' 0)). + move => H1; apply: (cvg_translim H1) ; exact H. (*can't apply a view*) + apply : cvg_trans. + - exact : (subsetfiltersx (locally'_filter 0)). move => {subsetfiltersx eqnear0x}. - unshelve apply : cvg_comp. - (*just showing that linear maps preserve balls - general lemma ? *) - - exact (@locally' C_topologicalType 0). + (*just showing that linear maps preserve balls + - general lemma ? *) + - exact (locally' 0). - move => A //= [r leq0r] absringrA. exists r ; first by []. move => h absrh hneq0 ; simpc. @@ -398,33 +422,49 @@ Proof. - by apply : absring_real_complex. - by rewrite eqCr . by []. - have eqnear0y : {near (@locally' R_topologicalType 0), 'i \*:quotC \o ( fun h => h *: 'i%C) =1 - quotiR }. - exists 1 ; first by [] ; move => h _ _ //= ; simpc . rewrite /quotC /quotiR (Im_mul h) invcM. + have eqnear0y : {near (locally' 0), 'i \*:quotC \o ( fun h => h *: 'i%C) =1 quotiR }. + exists 1 ; first by [] ; move => h _ _ //= ; simpc. + rewrite /quotC /quotiR (Im_mul h) invcM. rewrite scalerA real_complex_inv Im_inv !scalecr; simpc ; rewrite (Im_mul h). - by rewrite !real_complexE. - pose subsetfiltersy := (cvg_eq_loc eqnear0y). - have <- : lim (quotiR @ (@locally' R_topologicalType 0)) - = 'i * lim (quotC @ (@locally' C_topologicalType 0)). - have -> : 'i * lim (quotC @ (@locally' C_topologicalType 0)) - = lim ('i \*: quotC @ (@locally' C_topologicalType 0)). - rewrite scalei_muli ; rewrite (limin_scaler _ ('i) ). - - by []. - - exact : H. - apply : (@cvg_map_lim _ _ _ (@locally' R_topologicalType 0) _ _ (lim ('i \*:quotC @ (@locally' C_topologicalType 0) ))). - suff : quotiR @ (@locally' R_topologicalType 0) - `=>` ('i \*: quotC @ (@locally' C_topologicalType 0)). - move => H1 ; apply : (cvg_translim H1) . - by apply :(@cvg_scaler _ _ _ _ _ quotC ('i) ) ; exact : H. - apply : cvg_trans. - - apply : (subsetfiltersy (@locally'_filter R_topologicalType 0)). + by rewrite !real_complexE. + pose subsetfiltersy := (cvg_eq_loc eqnear0y). + have properlocally' : ProperFilter (locally'(0:C)). + (*This should be Canonical *) + split. + - rewrite /locally' /within => [[r leq0r] ballrwithin]; apply: (ballrwithin ((r/2)%:C) _). + rewrite /AbsRing_ball /ball_ absCE sub0r normcN //= . + rewrite expr0n //= addr0 sqrtr_sqr //= ger0_norm. + rewrite ltr_pdivr_mulr ; last by [] . + rewrite ltr_pmulr ; last by []. + by apply: ltr_spaddl. (* 1 < 2 *) + by apply : divr_ge0; apply ltrW. + have : (r / 2 != 0) by apply: mulf_neq0 ;apply: lt0r_neq0. + have -> : (0 = 0%:C) by move => K //=. + by apply: contra=> /eqP /complexI /eqP. + (* une vue permet d'abord d'utiliser une implication sur le terme + en tête sans avoir à l 'introduire*) + - by apply: locally'_filter. + have <- : lim (quotiR @ (locally' 0)) + = 'i * lim (quotC @ (locally' 0)). + have -> : 'i * lim (quotC @ (locally' 0)) + = lim ('i \*: quotC @ (locally' 0)). + rewrite scalei_muli limin_scaler; first by []. + by exact: H. + apply: cvg_map_lim. + suff: quotiR @ (locally' 0) + `=>` ('i \*: quotC @ (locally' 0)). + move => H1 ; apply: cvg_translim. + - exact: H1. + - by apply : cvg_scaler; exact : H. + apply: cvg_trans. + - apply : (subsetfiltersy (locally'_filter 0)). move => {subsetfiltersx eqnear0x}. - unshelve apply : cvg_comp. - - exact (@locally' C_topologicalType 0). + - exact (locally' 0). - move => A //= [r leq0r] absringrA. exists r ; first by []. - move => h absrh hneq0 ; simpc. - apply : (absringrA h*i). + move => h absrh hneq0; simpc. + apply: (absringrA). - by apply : absring_real_Im. - by rewrite eqCI. rewrite filter_of_filterE. @@ -433,21 +473,72 @@ Proof. Qed. - Lemma Diff_CR_holo (f : C^o -> C^o) c: - (forall v : C, derivable (complex_realfun f) c v) /\ (CauchyRiemanEq f c) -> - ((holomorphic f c)) . + +(* Local Notation "''D_' v f" := (derive f ^~ v). *) +(* Local Notation "''D_' v f c" := (derive f c v). *) + +Print derive. + Lemma Diff_CR_holo (f : C -> C) : (*This does not work pointwise *) + (forall c v : C, derivable ( f : C_RnormedType -> C_RnormedType) c v) + /\ (forall c, CauchyRiemanEq f c) ->(forall c, (holomorphic f c)). + (*sanity check : derivable (f : C ->C) does not type check *) Proof. - move => [der CR] v. - move : (der v); move => /cvg_ex {der} [l der]. - apply : (@cvgP _ _ _ l). - move => //= A loclA. - have lem : locally ((fun h : R => h^-1 *: (complex_realfun f (h *: v + c) - complex_realfun f c)) - @ (@locally' R_topologicalType 0)) A by exact : (der A loclA). - move : loclA ; move =>[r leq0r] absrA ; exists r ; first by []. - - move => [x y] ballrh neq0h //=. - move : lem ; move => //=. -Admitted. - + move => [der CR] c. + (* (* first attempt with littleo but requires to mix littleo on filter on different types ...*) *) + suff : exists l, forall h : C_absRingType, + f (c + h) = f c + h * l + 'o_[filter of locally (0 : C)] id h. + admit. + move: (der c 1%:C ); simpl => /cvg_ex [lr /cvg_lim //= Dlr]. + move: (der c 'i); simpl => /cvg_ex [li /cvg_lim //= Dli]. + simpl in (type of lr); simpl in (type of Dlr). + simpl in (type of li); simpl in (type of Dli). + move : (CR c) ; rewrite /CauchyRiemanEq //= (Dlr) (Dli) => CRc. + pose l:= ((lr + lr*'i)) ; exists l; move => [a b]. + move: (der (c + a%:C) 'i); simpl => /cvg_ex [//= la /cvg_lim //= Dla]. + move: (der (c + a%:C) 'i) => /derivable_locallyxP. + rewrite /derive //= Dla => oR. + have -> : (a +i* b) = (a%:C + b*: 'i%C) by simpc. + rewrite addrA oR. + (*have fun a => la = cst(lr) + o_0(a). *) + move: (der c 1%:C); simpl => /derivable_locallyxP ; rewrite /derive //= Dlr => oC. + (* rewrite [a%:C]/(a *: 1%:C). *) + have -> : a%:C = (a *: 1%:C) by simpc. + rewrite oC. Print real_complex. + have lem : (fun a =>( la - lr)) = 'o_[ filter of locally (0:R)] (@real_complex R) . + (*tried : la - lr = 'o_[ filter of locally (0:R)] (@real_complex R) a :> C^o *) + move => s0. Check eqoE. + suff : (fun _ : R => la - lr) = 'a_o_[filter of locally (0:R)] (real_complex R). + admit. + move => s1. + + + apply: eqoE. (*eqoE and eqoP are not working*) apply: eqoE. apply: eqoE. + (* struggling with o *) + Search "o" in landau. + + (* (*another attempt*) *) + (* rewrite /holomorphic cvg_ex. *) + (* move: (der c 1%:C ); simpl => /cvg_ex [lr //= Dlr]. *) + (* move: (der c 'i); simpl => /cvg_ex [li //= Dli]. *) + (* simpl in (type of lr); simpl in (type of Dlr). *) + (* simpl in (type of li); simpl in (type of Dli). *) + (* move : (CR c) ; rewrite /CauchyRiemanEq //= (cvg_lim Dlr) (cvg_lim Dli) => CRc. *) + (* pose l:= ((lr + lr*'i)) ; exists l; move => A //= [r leq0r] normrA. *) + (* pose r':= r/(sqrtr 2). *) + (* have lrl : l / (1 + 'i*1) = lr. admit. *) + (* exists r ; first by []. *) + (* move => [a b] ballab abneq0 //=. *) + (* suff : normc (l- (a +i* b)^-1 *: ((f (a +i* b + c) - f c) : C^o)) <= r. *) + (* admit. *) + (* have : locally lr A. exists r'. *) + (* - by rewrite mulr_gt0 //= invr_gt0 sqrtr_gt0. *) + (* - move => t; rewrite /ball_ -lrl.admit. *) + (* (*we should have a tactic rewriting in any way that fits *) *) + (* move => /Dlr //=. *) + (* move : (Dli A) => //=. + *) + Admitted. + Theorem CauchyRiemann (f : C^o -> C^o) c: ((holomorphic f c)) <-> (forall v : C, derivable (complex_realfun f) c v) /\ (CauchyRiemanEq f c). Proof. @@ -456,4 +547,4 @@ Admitted. -End Holomorphe. +End Holomorphe. \ No newline at end of file diff --git a/theories/newcomplex.v b/theories/newcomplex.v new file mode 100644 index 0000000000..bf0a18639e --- /dev/null +++ b/theories/newcomplex.v @@ -0,0 +1,1026 @@ +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) +Require Import Reals. (*can't get rid of this because it is used in normedtype *) +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype. +From mathcomp Require Import ssrnat eqtype choice fintype bigop ssralg . +From mathcomp Require Import bigop ssralg ssrint div ssrnum rat poly. +(* From mathcomp *) +(* Require Import matrix mxalgebra tuple mxpoly zmodp binomial realalg. *) +From mathcomp Require Import boolp reals Rstruct Rbar derive. +Require Import classical_sets posnum topology normedtype landau integral. + + +(*Pour distinguer fonctions mesurables et integrables, +utiliser des structures comme posrel. *) + + Import GRing.Theory Num.Theory Num.Def. +Local Open Scope ring_scope. +Local Open Scope classical_set_scope. + + + + +(**********************************************************************) +(*Definition of complex and holomorphy independantly from the *) + (* real-closed *) +(* of Cyril and thanks to the reals of mathcomp analysis *) +(**********************************************************************) + +Import GRing.Theory Num.Theory. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Obligation Tactic := idtac. + +Local Open Scope ring_scope. + +Reserved Notation "x +i* y" + (at level 40, left associativity, format "x +i* y"). +Reserved Notation "x -i* y" + (at level 40, left associativity, format "x -i* y"). +Reserved Notation "R [i]" + (at level 2, left associativity, format "R [i]"). + +Local Notation sgr := Num.sg. +Local Notation sqrtr := Num.sqrt. + +Record C : Type := Complex { Re : R; Im : R }. + +Delimit Scope complex_scope with C. +Local Open Scope complex_scope. + +Definition real_complex (x : R) := + Complex x 0. +(* Notation real_complex := (@real_complex_def _ ). *) +Notation "x %:C" := (real_complex x) + (at level 2, left associativity, format "x %:C") : complex_scope. +Notation "x +i* y" := (Complex x y) : complex_scope. +Notation "x -i* y" := (Complex x (- y)) : complex_scope. +Notation "x *i " := (Complex 0 x) (at level 8, format "x *i") : complex_scope. +Notation "''i'" := (Complex 0 1) : complex_scope. +(* Notation "C" := (complex) *) +(* (at level 2, left associativity, format "R [i]"). *) + +(* Module ComplexInternal. *) +Module ComplexEqChoice. +Section ComplexEqChoice. + +(* Variable R : Type. *) + +Definition sqR_of_complex (x : C) := let: a +i* b := x in [:: a; b]. +Definition complex_of_sqR (x : seq R) := + if x is [:: a; b] then Some (a +i* b) else None. + +Lemma complex_of_sqRK : pcancel sqR_of_complex complex_of_sqR. +Proof. by case. Qed. + +End ComplexEqChoice. +End ComplexEqChoice. + +Definition complex_eqMixin (* (R : eqType) *) := + PcanEqMixin (ComplexEqChoice.complex_of_sqRK ). +Definition complex_choiceMixin (* (R : choiceType) *) := + PcanChoiceMixin (ComplexEqChoice.complex_of_sqRK ). +(* Definition complex_countMixin (* (R : countType) *) := *) +(* PcanCountMixin (ComplexEqChoice.complex_of_sqRK ). *) + +Canonical complex_eqType (* (R : eqType) *) := + EqType C (complex_eqMixin). +Canonical complex_choiceType (* (R : choiceType) *) := + ChoiceType C (complex_choiceMixin). +(* Canonical complex_countType (* (R : countType) *) := *) +(* CountType C (complex_countMixin). *) + +Lemma eq_complex : forall (* (R : eqType) *) (x y : C), + (x == y) = (Re x == Re y) && (Im x == Im y). +Proof. +move=> [a b] [c d] /=. +apply/eqP/andP; first by move=> [-> ->]; split. +by case; move/eqP->; move/eqP->. +Qed. + +Lemma complexr0 : forall (* (R : ringType) *) (x : R), x +i* 0 = x%:C. Proof. by []. Qed. + +Module ComplexField. +Section ComplexField. + +(* Variable R : realType. *) +Local Notation C0 := ((0 : R)%:C). +Local Notation C1 := ((1 : R)%:C). + +Definition addc (x y : C) := let: a +i* b := x in let: c +i* d := y in + (a + c) +i* (b + d). +Definition oppc (x : C) := let: a +i* b := x in (- a) +i* (- b). + +Program Definition complex_zmodMixin := @ZmodMixin _ C0 oppc addc _ _ _ _. +Next Obligation. by move=> [a b] [c d] [e f] /=; rewrite !addrA. Qed. +Next Obligation. by move=> [a b] [c d] /=; congr (_ +i* _); rewrite addrC. Qed. +Next Obligation. by move=> [a b] /=; rewrite !add0r. Qed. +Next Obligation. by move=> [a b] /=; rewrite !addNr. Qed. +Canonical complex_zmodType := ZmodType C complex_zmodMixin. + +Definition scalec (a : R) (x : C) := + let: b +i* c := x in (a * b) +i* (a * c). + +Program Definition complex_lmodMixin := @LmodMixin _ _ scalec _ _ _ _. +Next Obligation. by move=> a b [c d] /=; rewrite !mulrA. Qed. +Next Obligation. by move=> [a b] /=; rewrite !mul1r. Qed. +Next Obligation. by move=> a [b c] [d e] /=; rewrite !mulrDr. Qed. +Next Obligation. by move=> [a b] c d /=; rewrite !mulrDl. Qed. +Definition C_RlmodType := LmodType R C complex_lmodMixin. +(*WARNING We don't want this to be canonical / contrary to real closed *) + +Definition mulc (x y : C) := let: a +i* b := x in let: c +i* d := y in + ((a * c) - (b * d)) +i* ((a * d) + (b * c)). + +Lemma mulcC : commutative mulc. +Proof. +move=> [a b] [c d] /=. +by rewrite [c * b + _]addrC ![_ * c]mulrC ![_ * d]mulrC. +Qed. + +Lemma mulcA : associative mulc. +Proof. +move=> [a b] [c d] [e f] /=. +rewrite !mulrDr !mulrDl !mulrN !mulNr !mulrA !opprD -!addrA. +by congr ((_ + _) +i* (_ + _)); rewrite !addrA addrAC; + congr (_ + _); rewrite addrC. +Qed. + +Definition invc (x : C) := let: a +i* b := x in let n2 := (a ^+ 2 + b ^+ 2) in + (a / n2) -i* (b / n2). + +Lemma mul1c : left_id C1 mulc. +Proof. by move=> [a b] /=; rewrite !mul1r !mul0r subr0 addr0. Qed. + +Lemma mulc_addl : left_distributive mulc addc. +Proof. +move=> [a b] [c d] [e f] /=; rewrite !mulrDl !opprD -!addrA. +by congr ((_ + _) +i* (_ + _)); rewrite addrCA. +Qed. + +Lemma nonzero1c : C1 != C0. Proof. by rewrite eq_complex /= oner_eq0. Qed. + +Definition complex_comRingMixin := + ComRingMixin mulcA mulcC mul1c mulc_addl nonzero1c. +Canonical complex_ringType :=RingType C complex_comRingMixin. +Canonical complex_comRingType := ComRingType C mulcC. + +Lemma mulVc : forall x, x != C0 -> mulc (invc x) x = C1. +Proof. +move=> [a b]; rewrite eq_complex => /= hab; rewrite !mulNr opprK. +rewrite ![_ / _ * _]mulrAC [b * a]mulrC subrr complexr0 -mulrDl mulfV //. +by rewrite paddr_eq0 -!expr2 ?expf_eq0 ?sqr_ge0. +Qed. + +Lemma invc0 : invc C0 = C0. Proof. by rewrite /= !mul0r oppr0. Qed. + +Definition complex_fieldUnitMixin := FieldUnitMixin mulVc invc0. +Canonical complex_unitRingType := UnitRingType C complex_fieldUnitMixin. +Canonical complex_comUnitRingType := Eval hnf in [comUnitRingType of C]. + +Lemma field_axiom : GRing.Field.mixin_of complex_unitRingType. +Proof. by []. Qed. + +Definition ComplexFieldIdomainMixin := (FieldIdomainMixin field_axiom). +Canonical complex_idomainType := IdomainType C (FieldIdomainMixin field_axiom). +Canonical complex_fieldType := FieldType C field_axiom. + +Ltac simpc := do ? + [ rewrite -[(_ +i* _) - (_ +i* _)]/(_ +i* _) + | rewrite -[(_ +i* _) + (_ +i* _)]/(_ +i* _) + | rewrite -[(_ +i* _) * (_ +i* _)]/(_ +i* _)]. + +Lemma real_complex_is_rmorphism : rmorphism (real_complex). +Proof. +split; [|split=> //] => a b /=; simpc; first by rewrite subrr. +by rewrite !mulr0 !mul0r addr0 subr0. +Qed. + +Canonical real_complex_rmorphism := + RMorphism real_complex_is_rmorphism. +Canonical real_complex_additive := + Additive real_complex_is_rmorphism. +About scalar. +Lemma Re_is_scalar : scalar (Re : C_RlmodType -> R). +Proof. by move=> a [b c] [d e]. Qed. + +Canonical Re_additive := Additive Re_is_scalar. +Canonical Re_linear := Linear Re_is_scalar. + +Lemma Im_is_scalar : scalar (Im : C_RlmodType -> R). +Proof. by move=> a [b c] [d e]. Qed. + +Canonical Im_additive := Additive Im_is_scalar. +Canonical Im_linear := Linear Im_is_scalar. + +Definition lec (x y : C) := + let: a +i* b := x in let: c +i* d := y in + (d == b) && (a <= c). + +Definition ltc (x y : C) := + let: a +i* b := x in let: c +i* d := y in + (d == b) && (a < c). + +Definition normc (x : C) : R := + let: a +i* b := x in sqrtr (a ^+ 2 + b ^+ 2). + +Notation normC x := (normc x)%:C. + +Lemma ltc0_add : forall x y, ltc 0 x -> ltc 0 y -> ltc 0 (x + y). +Proof. +move=> [a b] [c d] /= /andP [/eqP-> ha] /andP [/eqP-> hc]. +by rewrite addr0 eqxx addr_gt0. +Qed. + +Lemma eq0_normc x : normc x = 0 -> x = 0. +Proof. +case: x => a b /= /eqP; rewrite sqrtr_eq0 ler_eqVlt => /orP [|]; last first. + by rewrite ltrNge addr_ge0 ?sqr_ge0. +by rewrite paddr_eq0 ?sqr_ge0 ?expf_eq0 //= => /andP[/eqP -> /eqP ->]. +Qed. + +Lemma eq0_normC x : normC x = 0 -> x = 0. Proof. by case=> /eq0_normc. Qed. + +Lemma ge0_lec_total x y : lec 0 x -> lec 0 y -> lec x y || lec y x. +Proof. +move: x y => [a b] [c d] /= /andP[/eqP -> a_ge0] /andP[/eqP -> c_ge0]. +by rewrite eqxx ler_total. +Qed. + +Lemma normcM x y : normc (x * y) = normc x * normc y. +Proof. +move: x y => [a b] [c d] /=; rewrite -sqrtrM ?addr_ge0 ?sqr_ge0 //. +rewrite sqrrB sqrrD mulrDl !mulrDr -!exprMn. +rewrite mulrAC [b * d]mulrC !mulrA. +suff -> : forall (u v w z t : R), (u - v + w) + (z + v + t) = u + w + (z + t). + by rewrite addrAC !addrA. +by move=> u v w z t; rewrite [_ - _ + _]addrAC [z + v]addrC !addrA addrNK. +Qed. + +Lemma normCM x y : normC (x * y) = normC x * normC y. +Proof. by rewrite -rmorphM normcM. Qed. + +Lemma subc_ge0 x y : lec 0 (y - x) = lec x y. +Proof. by move: x y => [a b] [c d] /=; simpc; rewrite subr_ge0 subr_eq0. Qed. + +Lemma lec_def x y : lec x y = (normC (y - x) == y - x). +Proof. +rewrite -subc_ge0; move: (_ - _) => [a b]; rewrite eq_complex /= eq_sym. +have [<- /=|_] := altP eqP; last by rewrite andbF. +by rewrite [0 ^+ _]mul0r addr0 andbT sqrtr_sqr ger0_def. +Qed. + +Lemma ltc_def x y : ltc x y = (y != x) && lec x y. +Proof. +move: x y => [a b] [c d] /=; simpc; rewrite eq_complex /=. +by have [] := altP eqP; rewrite ?(andbF, andbT) //= ltr_def. +Qed. + +Lemma lec_normD x y : lec (normC (x + y)) (normC x + normC y). +Proof. +move: x y => [a b] [c d] /=; simpc; rewrite addr0 eqxx /=. +rewrite -(@ler_pexpn2r _ 2) -?topredE /= ?(ler_paddr, sqrtr_ge0) //. +rewrite [X in _ <= X] sqrrD ?sqr_sqrtr; + do ?by rewrite ?(ler_paddr, sqrtr_ge0, sqr_ge0, mulr_ge0) //. +rewrite -addrA addrCA (monoRL (addrNK _) (ler_add2r _)) !sqrrD. +set u := _ *+ 2; set v := _ *+ 2. +rewrite [a ^+ _ + _ + _]addrAC [b ^+ _ + _ + _]addrAC -addrA. +rewrite [u + _] addrC [X in _ - X]addrAC [b ^+ _ + _]addrC. +rewrite [u]lock [v]lock !addrA; set x := (a ^+ 2 + _ + _ + _). +rewrite -addrA addrC addKr -!lock addrC. +have [huv|] := ger0P (u + v); last first. + by move=> /ltrW /ler_trans -> //; rewrite pmulrn_lge0 // mulr_ge0 ?sqrtr_ge0. +rewrite -(@ler_pexpn2r _ 2) -?topredE //=; last first. + by rewrite ?(pmulrn_lge0, mulr_ge0, sqrtr_ge0) //. +rewrite -mulr_natl !exprMn !sqr_sqrtr ?(ler_paddr, sqr_ge0) //. +rewrite -mulrnDl -mulr_natl !exprMn ler_pmul2l ?exprn_gt0 ?ltr0n //. +rewrite sqrrD mulrDl !mulrDr -!exprMn addrAC -!addrA ler_add2l !addrA. +rewrite [_ + (b * d) ^+ 2]addrC -addrA ler_add2l. +have: 0 <= (a * d - b * c) ^+ 2 by rewrite sqr_ge0. +by rewrite sqrrB addrAC subr_ge0 [_ * c]mulrC mulrACA [d * _]mulrC. +Qed. + +Definition complex_numMixin := NumMixin lec_normD ltc0_add eq0_normC + ge0_lec_total normCM lec_def ltc_def. +Canonical complex_numDomainType := NumDomainType C complex_numMixin. + +End ComplexField. +End ComplexField. + +Locate numFieldType. +Import ComplexField. + +Canonical ComplexField.complex_zmodType. +Canonical ComplexField.C_RlmodType. (*Warning : is this OK ?*) +Canonical ComplexField.complex_ringType. +Canonical ComplexField.complex_comRingType. +Canonical ComplexField.complex_unitRingType. +Canonical ComplexField.complex_comUnitRingType. +Canonical ComplexField.complex_idomainType. +Canonical ComplexField.complex_fieldType. +Canonical ComplexField.complex_numDomainType. +Canonical complex_numFieldType := [numFieldType of C]. +Canonical ComplexField.real_complex_rmorphism. +Canonical ComplexField.real_complex_additive. +Canonical ComplexField.Re_additive. +Canonical ComplexField.Im_additive. + +Definition conjc (x : C) := let: a +i* b := x in a -i* b. +Notation "x ^*" := (conjc x) (at level 2, format "x ^*") : complex_scope. +Local Open Scope complex_scope. +Delimit Scope complex_scope with C. + +Ltac simpc := do ? + [ rewrite -[- (_ +i* _)%C]/(_ +i* _)%C + | rewrite -[(_ +i* _)%C - (_ +i* _)%C]/(_ +i* _)%C + | rewrite -[(_ +i* _)%C + (_ +i* _)%C]/(_ +i* _)%C + | rewrite -[(_ +i* _)%C * (_ +i* _)%C]/(_ +i* _)%C + | rewrite -[(_ +i* _)%C ^*]/(_ +i* _)%C + | rewrite -[_ *: (_ +i* _)%C]/(_ +i* _)%C + | rewrite -[(_ +i* _)%C <= (_ +i* _)%C]/((_ == _) && (_ <= _)) + | rewrite -[(_ +i* _)%C < (_ +i* _)%C]/((_ == _) && (_ < _)) + | rewrite -[`|(_ +i* _)%C|]/(sqrtr (_ + _))%:C%C + | rewrite (mulrNN, mulrN, mulNr, opprB, opprD, mulr0, mul0r, + subr0, sub0r, addr0, add0r, mulr1, mul1r, subrr, opprK, oppr0, + eqxx) ]. + + +Section ComplexTheory. + +(* Variable R : realType. *) + +Lemma ReiNIm : forall x : C, Re (x * 'i%C) = - Im x. +Proof. by case=> a b; simpc. Qed. + +Lemma ImiRe : forall x : C, Im (x * 'i%C) = Re x. +Proof. by case=> a b; simpc. Qed. + +Lemma complexE x : x = (Re x)%:C + 'i%C * (Im x)%:C :> C. +Proof. by case: x => *; simpc. Qed. + +Lemma real_complexE x : x%:C = x +i* 0 :> C. Proof. done. Qed. + +Lemma sqr_i : 'i%C ^+ 2 = -1 :> C. +Proof. by rewrite exprS; simpc; rewrite -real_complexE rmorphN. Qed. + +Lemma complexI : injective (real_complex). Proof. by move=> x y []. Qed. + +Lemma ler0c (x : R) : (0 <= x%:C) = (0 <= x). Proof. by simpc. Qed. + +Lemma lecE : forall x y : C, (x <= y) = (Im y == Im x) && (Re x <= Re y). +Proof. by move=> [a b] [c d]. Qed. + +Lemma ltcE : forall x y : C, (x < y) = (Im y == Im x) && (Re x < Re y). +Proof. by move=> [a b] [c d]. Qed. + +Lemma lecR : forall x y : R, (x%:C <= y%:C) = (x <= y). +Proof. by move=> x y; simpc. Qed. + +Lemma ltcR : forall x y : R, (x%:C < y%:C) = (x < y). +Proof. by move=> x y; simpc. Qed. + +Lemma conjc_is_rmorphism : rmorphism (conjc). +Proof. +split=> [[a b] [c d] | ] /=; first by simpc; rewrite [d - _]addrC. +by split=> [[a b] [c d] | ] /=; simpc. +Qed. + +Lemma conjc_is_scalable : scalable (conjc : C -> C_RlmodType). +Proof. by move=> a [b c]; simpc. Qed. + +Canonical conjc_rmorphism := RMorphism conjc_is_rmorphism. +Canonical conjc_additive := Additive conjc_is_rmorphism. +Canonical conjc_linear := AddLinear conjc_is_scalable. + +Lemma conjcK : involutive (conjc). +Proof. by move=> [a b] /=; rewrite opprK. Qed. + +Lemma mulcJ_ge0 (x : C) : 0 <= x * x^*%C. +Proof. +by move: x=> [a b]; simpc; rewrite mulrC addNr eqxx addr_ge0 ?sqr_ge0. +Qed. + +Lemma conjc_real (x : R) : x%:C^* = x%:C. +Proof. by rewrite /= oppr0. Qed. + +Lemma ReJ_add (x : C) : (Re x)%:C = (x + x^*%C) / 2%:R. +Proof. +case: x => a b; simpc; rewrite [0 ^+ 2]mul0r addr0 /=. +rewrite -!mulr2n -mulr_natr -mulrA [_ * (_ / _)]mulrA. +by rewrite divff ?mulr1 // -natrM pnatr_eq0. +Qed. + +Lemma ImJ_sub (x : C) : (Im x)%:C = (x^*%C - x) / 2%:R * 'i%C. +Proof. +case: x => a b; simpc; rewrite [0 ^+ 2]mul0r addr0 /=. +rewrite -!mulr2n -mulr_natr -mulrA [_ * (_ / _)]mulrA. +by rewrite divff ?mulr1 ?opprK // -natrM pnatr_eq0. +Qed. + +Lemma ger0_Im (x : C) : 0 <= x -> Im x = 0. +Proof. by move: x=> [a b] /=; simpc => /andP [/eqP]. Qed. + +(* Todo : extend theory of : *) +(* - signed exponents *) + +Lemma conj_ge0 : forall x : C, (0 <= x ^*) = (0 <= x). +Proof. by move=> [a b] /=; simpc; rewrite oppr_eq0. Qed. + +Lemma conjc_nat : forall n, (n%:R : C)^* = n%:R. +Proof. exact: rmorph_nat. Qed. + +Lemma conjc0 : (0 : C) ^* = 0. +Proof. exact: (conjc_nat 0). Qed. + +Lemma conjc1 : (1 : C) ^* = 1. +Proof. exact: (conjc_nat 1). Qed. + +Lemma conjc_eq0 : forall x : C, (x ^* == 0) = (x == 0). +Proof. by move=> [a b]; rewrite !eq_complex /= eqr_oppLR oppr0. Qed. + +Lemma conjc_inv: forall x : C, (x^-1)^* = (x^*%C )^-1. +Proof. exact: fmorphV. Qed. + +Lemma complex_root_conj (p : {poly C}) (x : C) : + root (map_poly conjc p) x = root p x^*. +Proof. by rewrite /root -{1}[x]conjcK horner_map /= conjc_eq0. Qed. + +Lemma normc_def (z : C) : `|z| = (sqrtr ((Re z)^+2 + (Im z)^+2))%:C. +Proof. by case: z. Qed. + +Lemma add_Re2_Im2 (z : C) : ((Re z)^+2 + (Im z)^+2)%:C = `|z|^+2. +Proof. by rewrite normc_def -rmorphX sqr_sqrtr ?addr_ge0 ?sqr_ge0. Qed. + +Lemma addcJ (z : C) : z + z^*%C = 2%:R * (Re z)%:C. +Proof. by rewrite ReJ_add mulrC mulfVK ?pnatr_eq0. Qed. + +Lemma subcJ (z : C) : z - z^*%C = 2%:R * (Im z)%:C * 'i%C. +Proof. +rewrite ImJ_sub mulrCA mulrA mulfVK ?pnatr_eq0 //. +by rewrite -mulrA ['i%C * _]sqr_i mulrN1 opprB. +Qed. + +Lemma complex_real (a b : R) : a +i* b \is Num.real = (b == 0). +Proof. +rewrite realE; simpc; rewrite [0 == _]eq_sym. +by have [] := ltrgtP 0 a; rewrite ?(andbF, andbT, orbF, orbb). +Qed. + +Lemma complex_realP (x : C) : reflect (exists y, x = y%:C) (x \is Num.real). +Proof. +case: x=> [a b] /=; rewrite complex_real. +by apply: (iffP eqP) => [->|[c []//]]; exists a. +Qed. + +Lemma RRe_real (x : C) : x \is Num.real -> (Re x)%:C = x. +Proof. by move=> /complex_realP [y ->]. Qed. + +Lemma RIm_real (x : C) : x \is Num.real -> (Im x)%:C = 0. +Proof. by move=> /complex_realP [y ->]. Qed. + +End ComplexTheory. + +(* all the above is copied from real-closed/complex.v *) + + Local Open Scope complex_scope. + Import ComplexField . + + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. + (* Obligation Tactic := idtac. *) + + (*This is now R from Reals *) + (*Adapting lemma eq_complex from complex.v, + which was done in boolean style*) + Lemma eqE_complex : forall (x y : C), (x = y) = ((Re x = Re y) /\ (Im x = Im y)). + Proof. + move => [a b] [c d]; apply : propositional_extensionality ; split. + by move => -> ; split. + by case => //= -> ->. + Qed. + + Lemma Re0 : Re 0 = 0 :> R. + Proof. by []. Qed. + + Lemma Im0 : Im 0 = 0 :> R. + Proof. by []. Qed. + + Lemma ReIm_eq0 (x : C) : (x=0) = ((Re x = 0)/\(Im x = 0)). + Proof. + by rewrite -[in Re x= _]Re0 -Im0 -eqE_complex. + Qed. + + Lemma normc0 : normc 0 = 0 :> R . + Proof. + by rewrite /normc //= expr0n //= add0r sqrtr0. + Qed. + + Lemma normcN ( x : C) : normc (-x) = (normc x). + Admitted. + + Lemma normc_r (x : R) : normc (x%:C) = normr (x). + Proof. by rewrite /normc/= expr0n //= addr0 sqrtr_sqr. Qed. + + + Lemma normc_i (x : R) : normc (x*i) = normr (x). + Proof. by rewrite /normc/= expr0n //= add0r sqrtr_sqr. Qed. + + Lemma normcN1 : normc (-1%:C) = 1 :> R. + Proof. + by rewrite /normc/= oppr0 expr0n addr0 -signr_odd expr0 sqrtr1. + Qed. + + Lemma realtocomplex_additive : forall x y : R, (x + y)%:C = x%:C + y%:C. + Proof. + (*real_complex_additive*) + move => x y ; rewrite -!complexr0 eqE_complex //=. + by split ; last by rewrite addr0. + Qed. + + Lemma real_complex_inv : forall x : R, x%:C^-1 = (x^-1)%:C. + Proof. + Search _ (rmorphism _). + Admitted. + + Lemma Im_inv : ('i%C)^-1 = (-1*i) :> C. + Proof. Admitted. + + Lemma invcM : forall x y : C, (x*y)^-1 = x^-1 * y^-1. + (*Maybe another lemma is doing that, or invrM *) + Proof. Admitted. + +Lemma scale_inv : forall (h : R) (v : C), (h*:v)^-1 = h^-1 *: v^-1. + (*Maybe another lemma is doing that, or invrM *) + Proof. Admitted. + + + Lemma Im_mul : forall x : R, (x*i) = (x%:C * 'i%C). + Proof. by move => x ; simpc. Qed. + + Lemma normcD : forall ( x y : C), normc (x+y) <= (normc x + normc y). + Proof. + by move => x y ; rewrite -lecR realtocomplex_additive ; apply :lec_normD . + Qed. + + Lemma normcZ : forall (l : R) (x : C), normc (l *: x) = `|l| * (normc x). + Proof. + move => l [a b] ; rewrite /normc //= !exprMn. + rewrite -mulrDr sqrtrM ; last by rewrite sqr_ge0. + by rewrite sqrtr_sqr. + Qed. + + Lemma scalecr : forall w : C^o, forall r : R, (r *: w = r%:C *: w). + Proof. by move => [a b ] r; rewrite eqE_complex //=; split; simpc. Qed. + + + +Section C_Rnormed. + + (* Uniform.mixin_of takes a locally but does not expect a TopologicalType, which is inserted in the Uniform.class_of *) + (* Whereas NormedModule.mixin_of asks for a Uniform.mixin_of loc *) + + Program Definition uniformmixin_of_normaxioms (V : lmodType R) (norm : V -> R) + (ax1 : forall x y : V, norm (x + y) <= norm x + norm y) + ( ax2 : forall (l : R) (x : V), norm (l *: x) = `|l| * (norm x)) + ( ax4 : forall x : V, norm x = 0 -> x = 0 ) : Uniform.mixin_of (locally_ (ball_ norm)) + := @Uniform.Mixin V (locally_ (ball_ norm)) (ball_ norm) _ _ _ _. + Next Obligation. + move => V norm _ H _ ; rewrite /ball_ => x e. + have -> : x - x = 0 . by rewrite addrN. + suff -> : norm 0 = 0 by []. + have -> : 0 = 0 *: x by rewrite scale0r. + by rewrite H normr0 mul0r. + Qed. + Next Obligation. + move => V norm _ H _ ; rewrite /ball_ => x e e0. + have -> : x - e = (-1) *: (e-x) by rewrite -opprB scaleN1r. + by rewrite (H (-1) (e-x)) normrN1 mul1r. + Qed. + Next Obligation. + move => V norm H _ _ ; rewrite /ball_ => x y z e1 e2 normxy normyz. + by rewrite (subr_trans y) (ler_lt_trans (H _ _)) ?ltr_add. + Qed. + Next Obligation. by []. Qed. + + (*Warning : line 412 of Rstruct, why is the canonical realType structure on R + called real_relaType and not R_realType. *) + (*C as a R-lmodule *) + + Definition C_RlmodMixin := (complex_lmodMixin). + (*LmodType is hard to use, not findable through Search and not checkable + as abbreviation is not applied enough*) + Definition C_RlmodType := @LmodType R C C_RlmodMixin. + Definition C_pointedType := PointedType C 0. + Canonical C_pointedType. + Definition C_filteredType := FilteredType C C (locally_ (ball_ (normc))). + Canonical C_filteredType. + (*Are we sure that the above is canonical *) + + (*Warning : going from R to a R:realType one must remplace + everything related to normc to normc with explicit realtype *) + Program Definition C_RuniformMixin := + @uniformmixin_of_normaxioms C_RlmodType (normc) normcD normcZ (eq0_normc). + Definition C_RtopologicalMixin := topologyOfBallMixin C_RuniformMixin. + Definition C_RtopologicalType := TopologicalType C_filteredType C_RtopologicalMixin. + Definition C_RuniformType := @UniformType C_RtopologicalType C_RuniformMixin. + + + Program Definition C_RnormedMixin + := @NormedModMixin R_absRingType C_RlmodType _ C_RuniformMixin (normc) + normcD normcZ _ (eq0_normc). + Next Obligation. by []. Qed. + + + Definition C_RnormedType : normedModType R := @NormedModType R C_RuniformType C_RnormedMixin. + + + Lemma scalecAl : forall (h : R) ( x y : C_RnormedType), + h *: ( x * y) = h *: x * y. + Proof. move => h [a b] [c d]. simpc. Admitted. + + + Definition C_RLalg := LalgType R C_RlmodType scalecAl. + +End C_Rnormed. + + +Section C_absRing. + + + + (*Canonical C_ringType := complex_ringType . *) + Definition C_AbsRingMixin := @AbsRingMixin (complex_ringType) + (normc) normc0 normcN1 normcD (normcM) (eq0_normc). + Definition C_absRingType := AbsRingType C C_AbsRingMixin. + Canonical C_absRingType. + Definition C_topologicalType := [topologicalType of C for C_absRingType]. + Canonical C_topologicalType. + Definition C_uniformType := [uniformType of C for C_absRingType]. + Canonical C_uniformType. + Definition Co_pointedType := [pointedType of C^o for C_absRingType]. + Definition Co_filteredType := [filteredType C^o of C^o for C_absRingType]. + Definition Co_topologicalType := [topologicalType of C^o for C_absRingType]. + + Canonical Zmod_topologicalType ( K : absRingType) + (V : normedModType K):= + [topologicalType of [zmodType of V]]. + + Definition Co_uniformType := [uniformType of C^o for C_absRingType]. + Canonical Co_uniformType. + Definition Co_normedType := AbsRing_NormedModType C_absRingType. + Canonical Co_normedType. + Canonical C_normedType := [normedModType C of C for Co_normedType]. + (*C is convertible to C^o *) + + + Canonical R_normedType := [normedModType R of R for [normedModType R of R^o]]. + + Canonical absRing_normedType (K : absRingType) := + [normedModType K^o of K for (AbsRing_NormedModType K)]. + + Lemma abs_normE : forall ( K : absRingType) (x : K), `|x|%real = `|[x]|. + Proof. by []. Qed. + + (*Delete absCE and adapt from abs_normE *) + Lemma absCE : forall x : C, `|x|%real = (normc x). + Proof. by []. Qed. + + Lemma normCR : forall x : R, `|[x%:C]| = `|x|%real. + Proof. Admitted. + + Lemma absring_real_complex : forall r: R, forall x : R, AbsRing_ball 0 r x -> + (AbsRing_ball 0%:C r x%:C). + Proof. + move => r x ballrx. + rewrite /AbsRing_ball /ball_ absCE. + rewrite addrC addr0 -scaleN1r normcZ normrN1 mul1r normc_r. + move : ballrx ; rewrite /AbsRing_ball /ball_ absRE. + by rewrite addrC addr0 normrN. + Qed. + + + Lemma absring_real_Im : forall r: R, forall x : R, AbsRing_ball 0 r x -> + (AbsRing_ball 0%:C r x*i). + Proof. + move => r x ballrx. + rewrite /AbsRing_ball /ball_ absCE. + rewrite addrC addr0 -scaleN1r normcZ normrN1 mul1r normc_i. + move : ballrx ; rewrite /AbsRing_ball /ball_ absRE. + by rewrite addrC addr0 normrN. + Qed. + Locate imaginaryC. (* WHAT ?????? *) + Print imaginaryC. + Unset Printing Notations. + Check 'i. + Lemma scalei_muli : forall (z : C), z * 'i = 'i *: z. + Proof. Why is it not working ? Let us do everyhting over a realtype + by []. Coule be a problem of requiring Reals after reals. + Qed. + + Lemma iE : 'i%C = 'i :> C. + Proof. by []. Qed. + + Lemma scaleC_mul : forall (w v : C^o), (v *: w = v * w). + Proof. by []. Qed. + +End C_absRing. + + + +Section Holomorphe. + +Print differentiable_def. +(* used in derive.v, what does center means*) +(*CoInductive +differentiable_def (K : absRingType) (V W : normedModType K) (f : V -> W) +(x : filter_on V) (phF : phantom (set (set V)) x) : Prop := + DifferentiableDef : continuous 'd f x /\ f = (cst (f (lim x)) + 'd f x) \o + center (lim x) +o_x center (lim x) -> differentiable_def f phF *) +(*Diff is defined from any normedmodule of any absringtype, + so C is a normedmodul on itsself *) +(*Vague idea that this should work, as we see C^o as a vector space on C and not R*) + + +(*Important : differentiable in derive.v, means continuoulsy differentiable, +not just that the limit exists. *) +(*derivable concerns only the existence of the derivative *) + + Definition holomorphic (f : C^o -> C^o) (c: C^o) := + cvg ((fun (h:C^o)=> h^-1 *: ((f \o shift c) (h) - f c)) @ (locally' 0)). + + Definition complex_realfun (f : C^o -> C^o) : C_RnormedType -> C_RnormedType := f. + Arguments complex_realfun _ _ /. + + Definition complex_Rnormed_absring : C_RnormedType -> C^o := id. + + Definition CauchyRiemanEq_R2 (f : C_RnormedType -> C_RnormedType) c := + let u := (fun c => Re ( f c)): C_RnormedType -> R^o in + let v:= (fun c => Im (f c)) : C_RnormedType -> R^o in + (* ('D_(1%:C) u = 'D_('i) v) /\ ('D_('i) u = 'D_(1%:C) v). *) + (((derive u c (1%:C)) = + (derive v c ('i : C_RnormedType))) /\ ((derive v c (1%:C)) = -(derive u c ('i : C_RnormedType)))). + + + Definition deriveC (V W : normedModType C)(f : V -> W) c v := + lim ((fun (h: C^o) => h^-1 *: ((f \o shift c) (h *: v) - f c)) @ locally' 0). + + + Definition CauchyRiemanEq (f : C -> C) z := + 'i * lim ((fun h : R => h^-1 *: ((f \o shift z) (h *: 1%:C) - f z)) @ locally' 0) = + lim ((fun h : R => h^-1 *: ((f \o shift z) (h *: 'i%C) - f z)) @ locally' 0). + + + Lemma eqCr (R : rcfType) (r s : R) : (r%:C == s%:C) = (r == s). + Proof. exact: (inj_eq (@complexI _)). Qed. + + Lemma eqCI (R : rcfType) (r s : R) : (r*i == s*i) = (r == s). + Proof. Admitted. + + +(*Lemma lim_trans (T : topologicalType) (F : set (set T)) +(G : set (set T)) (l : T) : ( F `=>` G ) -> (G --> l) -> ( F --> l). + move => FG Gl A x. + Search "lim" "trans". + *) + + Lemma cvg_translim (T : topologicalType) (F G: set (set T)) (l :T) : + F `=>` G -> (G --> l) -> (F --> l). + Proof. + move => FG Gl. apply : cvg_trans. + exact : FG. + exact : Gl. + Qed. + + + Lemma cvg_scaler (K : absRingType) (V : normedModType K) (T : topologicalType) + (F : set (set T)) (H :Filter F) (f : T -> V) (k : K) : + cvg (f @ F) -> cvg ((k \*: f) @ F ). + Proof. + by move => /cvg_ex [l H0] ; apply: cvgP; apply: cvgZr; apply: H0. + Qed. + +(* Lemma cvg_proper_top (T : topologicalType) (F : set (set U)) (FF : Filter F) : *) +(* cvg F -> ProperFilter F. *) + + + Lemma limin_scaler (K : absRingType) (V : normedModType K) (T : topologicalType) + (F : set (set T)) (FF : ProperFilter F) (f : T -> V) (k : K) : + cvg(f@F) -> k *: lim (f @ F) = lim ((k \*: f) @ F ). + Proof. + move => cv. + symmetry. + by apply: cvg_lim; apply: cvgZr . + Qed. + +(*this could be done for scale also ... *) + +(*I needed filter_of_filterE to make things easier - +looked a long time of it as I was looking for a [filter of lim]* + instead of a [filter of filter]*) + +(*There whould be a lemma analogous to [filter of lim] to ease the search *) + +Lemma holo_derivable (f : C^o -> C^o) c : holomorphic f c + -> (forall v:C , derivable (complex_realfun f) c v). +Proof. + move => /cvg_ex [l H]; rewrite /derivable => v. + rewrite /type_of_filter /= in l H. + set ff : C_RnormedType -> C_RnormedType := f. + set quotR := (X in (X @ locally' 0)). + pose mulv (h :R):= (h *:v). + pose quotC (h : C) : C^o := h^-1 *: ((f \o shift c) (h) - f c). + (* here f : C -> C does not work - +as if we needed C^o still for the normed structure*) + case : (EM (v = 0)). + - move => eqv0 ; apply (cvgP (l := (0:C))). + have eqnear0 : {near locally' (0:R), 0 =1 quotR}. + exists 1 => // h _ _ ; rewrite /quotR /shift eqv0. simpl. + by rewrite scaler0 add0r addrN scaler0. + (*addrN is too hard to find through Search *) + apply: cvg_translim. + - exact (cvg_eq_loc eqnear0). + - by apply : cst_continuous. + (*WARNING : cvg_cst from normedtype applies only to endofunctions + That should NOT be the case, as one could use it insteas of cst_continuous *) + - move/eqP => vneq0 ; apply : (cvgP (l := v *: l)). (*chainage avant et suff *) + have eqnear0 : {near (locally' (0 : R)), (v \*: quotC) \o mulv =1 quotR}. + exists 1 => // h _ neq0h //=; rewrite /quotC /quotR /mulv scale_inv. + rewrite scalerAl scalerCA -scalecAl mulrA -(mulrC v) mulfV. + rewrite mul1r; apply: (scalerI (neq0h)). + by rewrite !scalerA //= (divff neq0h). + by []. + have subsetfilters: quotR @ locally' 0 `=>` (v \*: quotC) \o mulv @locally' 0. + by exact: (cvg_eq_loc eqnear0). + apply: cvg_trans subsetfilters _. + unshelve apply : cvg_comp. + - exact (locally' (0:C)). + - move => //= A [r [leq0r ballrA]]. + exists (r / (`|[v]|)). + - apply : mulr_gt0 ; first by []. + by rewrite invr_gt0 normm_gt0. + - move => b; rewrite /AbsRing_ball /ball_ sub0r absRE normrN => ballrb neqb0. + have ballCrb : (AbsRing_ball 0 r (mulv b)). + rewrite /AbsRing_ball /ball_ sub0r absrN /mulv scalecr absrM abs_normE. + rewrite -ltr_pdivl_mulr. + - by rewrite normCR. + by rewrite abs_normE normm_gt0. + have bneq0C : (b%:C != 0%:C) by move: neqb0; apply: contra; rewrite eqCr. + by apply: (ballrA (mulv b) ballCrb); rewrite scaler_eq0; apply/norP; split. + suff : v \*: quotC @ locally' (0 : C) --> v *: l by []. + by apply: cvgZr ; rewrite /quotC. +Qed. + +Lemma holo_CauchyRieman (f : C^o -> C^o) c: (holomorphic f c) -> (CauchyRiemanEq f c). +Proof. + move => H; rewrite /CauchyRiemanEq. + pose quotC := (fun h : C => h^-1 *: ((f \o shift c) (h) - f c)). + pose quotR := (fun h : R => h^-1 *: ((f \o shift c) (h *: 1%:C ) - f c)). + pose quotiR := (fun (h : R) => h^-1 *: ((f \o shift c) (h *: 'i%C) - f c)). + have eqnear0x : {near (locally' 0), quotC \o ( fun h => h *: 1%:C) =1 quotR}. + exists 1 ; first by [] ; move => h _ _ //=; simpc. + by rewrite /quotC /quotR real_complex_inv -scalecr; simpc. + pose subsetfiltersx := (cvg_eq_loc eqnear0x). + have -> : lim (quotR @ (locally' 0)) + = lim (quotC @ (locally' 0)). + apply: cvg_map_lim. + suff: quotR @ (locally' 0) `=>` (quotC @ (locally' 0)). + move => H1; apply: (cvg_translim H1) ; exact H. (*can't apply a view*) + apply : cvg_trans. + - exact : (subsetfiltersx (locally'_filter 0)). + move => {subsetfiltersx eqnear0x}. + - unshelve apply : cvg_comp. + (*just showing that linear maps preserve balls + - general lemma ? *) + - exact (locally' 0). + - move => A //= [r leq0r] absringrA. + exists r ; first by []. + move => h absrh hneq0 ; simpc. + apply : (absringrA h%:C). + - by apply : absring_real_complex. + - by rewrite eqCr . + by []. + have eqnear0y : {near (locally' 0), 'i \*:quotC \o ( fun h => h *: 'i%C) =1 quotiR }. + exists 1 ; first by [] ; move => h _ _ //= ; simpc. + rewrite /quotC /quotiR (Im_mul h) invcM. + rewrite scalerA real_complex_inv Im_inv !scalecr; simpc ; rewrite (Im_mul h). + by rewrite !real_complexE. + pose subsetfiltersy := (cvg_eq_loc eqnear0y). + have properlocally' : ProperFilter (locally'(0:C)). + (*This should be Canonical *) + split. + - rewrite /locally' /within => [[r leq0r] ballrwithin]; apply: (ballrwithin ((r/2)%:C) _). + rewrite /AbsRing_ball /ball_ absCE sub0r normcN //= . + rewrite expr0n //= addr0 sqrtr_sqr //= ger0_norm. + rewrite ltr_pdivr_mulr ; last by [] . + rewrite ltr_pmulr ; last by []. + by apply: ltr_spaddl. (* 1 < 2 *) + by apply : divr_ge0; apply ltrW. + have : (r / 2 != 0) by apply: mulf_neq0 ;apply: lt0r_neq0. + have -> : (0 = 0%:C) by move => K //=. + by apply: contra=> /eqP /complexI /eqP. + (* une vue permet d'abord d'utiliser une implication sur le terme + en tête sans avoir à l 'introduire*) + - by apply: locally'_filter. + have <- : lim (quotiR @ (locally' 0)) + = 'i * lim (quotC @ (locally' 0)). + have -> : 'i * lim (quotC @ (locally' 0)) + = lim ('i \*: quotC @ (locally' 0)). + rewrite scalei_muli limin_scaler; first by []. + by exact: H. + apply: cvg_map_lim. + suff: quotiR @ (locally' 0) + `=>` ('i \*: quotC @ (locally' 0)). + move => H1 ; apply: cvg_translim. + - exact: H1. + - by apply : cvg_scaler; exact : H. + apply: cvg_trans. + - apply : (subsetfiltersy (locally'_filter 0)). + move => {subsetfiltersx eqnear0x}. + - unshelve apply : cvg_comp. + - exact (locally' 0). + - move => A //= [r leq0r] absringrA. + exists r ; first by []. + move => h absrh hneq0; simpc. + apply: (absringrA). + - by apply : absring_real_Im. + - by rewrite eqCI. + rewrite filter_of_filterE. + by []. + by []. +Qed. + + + +(* Local Notation "''D_' v f" := (derive f ^~ v). *) +(* Local Notation "''D_' v f c" := (derive f c v). *) + +Print derive. + Lemma Diff_CR_holo (f : C -> C) : (*This does not work pointwise *) + (forall c v : C, derivable ( f : C_RnormedType -> C_RnormedType) c v) + /\ (forall c, CauchyRiemanEq f c) ->(forall c, (holomorphic f c)). + (*sanity check : derivable (f : C ->C) does not type check *) + Proof. + move => [der CR] c. + (* (* first attempt with littleo but requires to mix littleo on filter on different types ...*) *) + suff : exists l, forall h : C_absRingType, + f (c + h) = f c + h * l + 'o_[filter of locally (0 : C)] id h. + admit. + move: (der c 1%:C ); simpl => /cvg_ex [lr /cvg_lim //= Dlr]. + move: (der c 'i); simpl => /cvg_ex [li /cvg_lim //= Dli]. + simpl in (type of lr); simpl in (type of Dlr). + simpl in (type of li); simpl in (type of Dli). + move : (CR c) ; rewrite /CauchyRiemanEq //= (Dlr) (Dli) => CRc. + pose l:= ((lr + lr*'i)) ; exists l; move => [a b]. + move: (der (c + a%:C) 'i); simpl => /cvg_ex [//= la /cvg_lim //= Dla]. + move: (der (c + a%:C) 'i) => /derivable_locallyxP. + rewrite /derive //= Dla => oR. + have -> : (a +i* b) = (a%:C + b*: 'i%C) by simpc. + rewrite addrA oR. + (*have fun a => la = cst(lr) + o_0(a). *) + move: (der c 1%:C); simpl => /derivable_locallyxP ; rewrite /derive //= Dlr => oC. + (* rewrite [a%:C]/(a *: 1%:C). *) + have -> : a%:C = (a *: 1%:C) by simpc. + rewrite oC. Print real_complex. + have lem : (fun a =>( la - lr)) = 'o_[ filter of locally (0:R)] (@real_complex R) . + (*tried : la - lr = 'o_[ filter of locally (0:R)] (@real_complex R) a :> C^o *) + move => s0. Check eqoE. + suff : (fun _ : R => la - lr) = 'a_o_[filter of locally (0:R)] (real_complex R). + admit. + move => s1. + (*eqoE and eqoP are not working*) + (* struggling with o *) + (* (*another attempt*) *) + (* rewrite /holomorphic cvg_ex. *) + (* move: (der c 1%:C ); simpl => /cvg_ex [lr //= Dlr]. *) + (* move: (der c 'i); simpl => /cvg_ex [li //= Dli]. *) + (* simpl in (type of lr); simpl in (type of Dlr). *) + (* simpl in (type of li); simpl in (type of Dli). *) + (* move : (CR c) ; rewrite /CauchyRiemanEq //= (cvg_lim Dlr) (cvg_lim Dli) => CRc. *) + (* pose l:= ((lr + lr*'i)) ; exists l; move => A //= [r leq0r] normrA. *) + (* pose r':= r/(sqrtr 2). *) + (* have lrl : l / (1 + 'i*1) = lr. admit. *) + (* exists r ; first by []. *) + (* move => [a b] ballab abneq0 //=. *) + (* suff : normc (l- (a +i* b)^-1 *: ((f (a +i* b + c) - f c) : C^o)) <= r. *) + (* admit. *) + (* have : locally lr A. exists r'. *) + (* - by rewrite mulr_gt0 //= invr_gt0 sqrtr_gt0. *) + (* - move => t; rewrite /ball_ -lrl.admit. *) + (* (*we should have a tactic rewriting in any way that fits *) *) + (* move => /Dlr //=. *) + (* move : (Dli A) => //=. + *) + Admitted. + +Theorem CauchyRiemann (f : C^o -> C^o) c: ((holomorphic f c)) + <-> (forall v : C, derivable (complex_realfun f) c v) /\ (CauchyRiemanEq f c). +Proof. +Admitted. + + + + +End Holomorphe. \ No newline at end of file From 1f0898f4766d26bbef18f95a09f2f898d0bfd6ee Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 30 Apr 2020 00:56:07 +0900 Subject: [PATCH 04/11] update cauchyetoile.v wrt PR#270 --- theories/cauchyetoile.v | 126 ++++++++++++++++++++++++++-------------- 1 file changed, 81 insertions(+), 45 deletions(-) diff --git a/theories/cauchyetoile.v b/theories/cauchyetoile.v index 02d848d7da..96421a9ac7 100644 --- a/theories/cauchyetoile.v +++ b/theories/cauchyetoile.v @@ -1,30 +1,31 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) -Require Import Reals. From mathcomp Require Import ssreflect ssrfun ssrbool. -From mathcomp Require Import ssrnat eqtype choice fintype bigop ssralg ssrnum. -From mathcomp Require Import complex. -From mathcomp Require Import boolp reals Rstruct Rbar derive. -Require Import classical_sets posnum topology normedtype landau integral. +From mathcomp Require Import ssrnat eqtype choice fintype bigop order ssralg ssrnum. +From mathcomp Require Import complex. +From mathcomp Require Import boolp reals ereal derive. +Require Import classical_sets posnum topology normedtype landau integral. -(*Pour distinguer fonctions mesurables et integrables, +(*Pour distinguer fonctions mesurables et integrables, utiliser des structures comme posrel. *) -Import GRing.Theory Num.Theory ComplexField Num.Def. +Import Order.TTheory GRing.Theory Num.Theory ComplexField Num.Def. Local Open Scope ring_scope. Local Open Scope classical_set_scope. Local Open Scope complex_scope. - Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. (* Obligation Tactic := idtac. *) +Section cauchyetoile. +Variable R : rcfType. + Local Notation sgr := Num.sg. Local Notation sqrtr := Num.sqrt. Local Notation C := R[i]. - Notation Re:= (complex.Re). - Notation Im:= (complex.Im). + Notation Re:= (@complex.Re R). + Notation Im:= (@complex.Im R). (*Adapting lemma eq_complex from complex.v, @@ -109,8 +110,14 @@ Lemma scale_inv : forall (h : R) (v : C), (h*:v)^-1 = h^-1 *: v^-1. Lemma scalecr : forall w : C^o, forall r : R, (r *: w = r%:C *: w). Proof. by move => [a b ] r; rewrite eqE_complex //=; split; simpc. Qed. - - +Lemma normc_ge0 (x : C) : 0 <= normc x. +Proof. case: x => ? ?; exact: sqrtr_ge0. Qed. + +Lemma mulrnc (a b : R) k : a +i* b *+ k = (a *+ k) +i* (b *+ k). +Proof. +by elim: k => // k ih; apply/eqP; rewrite !mulrS eq_complex !ih !eqxx. +Qed. + Section C_Rnormed. (* Uniform.mixin_of takes a locally but does not expect a TopologicalType, which is inserted in the Uniform.class_of *) @@ -122,8 +129,8 @@ Section C_Rnormed. Program Definition uniformmixin_of_normaxioms (V : lmodType R) (norm : V -> R) (ax1 : forall x y : V, norm (x + y) <= norm x + norm y) ( ax2 : forall (l : R) (x : V), norm (l *: x) = `|l| * (norm x)) - ( ax4 : forall x : V, norm x = 0 -> x = 0 ) : Uniform.mixin_of (locally_ (ball_ norm)) - := @Uniform.Mixin V (locally_ (ball_ norm)) (ball_ norm) _ _ _ _. + ( ax4 : forall x : V, norm x = 0 -> x = 0 ) : Uniform.mixin_of _ (locally_ (ball_ norm)) + := @Uniform.Mixin _ V (locally_ (ball_ norm)) (ball_ norm) _ _ _ _. Next Obligation. move => V norm _ H _ ; rewrite /ball_ => x e. have -> : x - x = 0 . by rewrite addrN. @@ -138,35 +145,63 @@ Section C_Rnormed. Qed. Next Obligation. move => V norm H _ _ ; rewrite /ball_ => x y z e1 e2 normxy normyz. - by rewrite (subr_trans y) (ler_lt_trans (H _ _)) ?ltr_add. + by rewrite (subr_trans y) (order.Order.POrderTheory.le_lt_trans (H _ _)) ?ltr_add. Qed. Next Obligation. by []. Qed. (*C as a R-lmodule *) - Definition C_RlmodMixin := (complex_lmodMixin R_rcfType). (*R instead of R_rcfType is not working *) - (*LmodType is hard to use, not findable through Search and not checkable as abbreviation is not applied enough*) + Definition C_RlmodMixin := (complex_lmodMixin R). (*R instead of R_rcfType is not working *) +(*LmodType is hard to use, not findable through Search and not checkable as abbreviation is not applied enough*) Definition C_RlmodType := @LmodType R C C_RlmodMixin. Definition C_pointedType := PointedType C 0. Canonical C_pointedType. - Definition C_filteredType := FilteredType C C (locally_ (ball_ (@normc R_rcfType))). + Definition C_filteredType := FilteredType C C (locally_ (ball_ (@normc R))). Canonical C_filteredType. (*Are we sure that the above is canonical *) Program Definition C_RuniformMixin := - @uniformmixin_of_normaxioms C_RlmodType (@normc R_rcfType) normcD normcZ (@eq0_normc R_rcfType). + @uniformmixin_of_normaxioms (complex_lmodType R) (@normc R) normcD normcZ (@eq0_normc R). Definition C_RtopologicalMixin := topologyOfBallMixin C_RuniformMixin. - Definition C_RtopologicalType := TopologicalType C_filteredType C_RtopologicalMixin. - Definition C_RuniformType := @UniformType C_RtopologicalType C_RuniformMixin. +(* Definition C_RtopologicalType := TopologicalType C_filteredType C_RtopologicalMixin.*) +Canonical C_RtopologicalType := TopologicalType C C_RtopologicalMixin. +(* Definition C_RuniformType := @UniformType C_RtopologicalType C_RuniformMixin.*) +Canonical C_RuniformType := UniformType C C_RuniformMixin. + +Lemma normc_natmul (x : C) k : normc (x *+ k) = (normc x) *+ k. +Proof. +elim: k => [|k ih]; first by rewrite !mulr0n normc0. +rewrite !mulrS; apply/eqP; rewrite eq_le; apply/andP; split. + rewrite -ih; exact/normcD. +have [/eqP->|x0] := boolP (normc x == 0). + by rewrite mul0rn add0r normc_ge0. +case: x x0 ih; rewrite /normc => a b x0. +Admitted. +Program Definition C_RnormedMixin := + @Num.NormedMixin _ _ _ _ normcD (@eq0_normc _) normc_natmul normcN. +Canonical C_RnormedType := NormedZmodType R C^o C_RnormedMixin. +Lemma normc_ball : + @ball _ [uniformType R of C^o] = ball_ (fun x => `| x |). +Proof. by []. Qed. + +Definition normc_UniformNormedZmodMixin := + UniformNormedZmodule.Mixin normc_ball. +Canonical normc_uniformNormedZmodType := + UniformNormedZmoduleType R C^o normc_UniformNormedZmodMixin. (* TODO: warning *) + +Definition C_RnormedModMixin := @NormedModMixin R normc_uniformNormedZmodType _ normcZ. +Canonical C_RnormedModType := + NormedModType R normc_uniformNormedZmodType C_RnormedModMixin. + +(* Program Definition C_RnormedMixin - := @NormedModMixin R_absRingType C_RlmodType _ C_RuniformMixin (@normc R_rcfType) normcD normcZ _ (@eq0_normc R_rcfType) . + := @NormedModMixin R_absRingType C_RlmodType _ C_RuniformMixin (@normc R) normcD normcZ _ (@eq0_normc R) . Next Obligation. by []. Qed. - Definition C_RnormedType : normedModType R := @NormedModType R C_RuniformType C_RnormedMixin. - +*) Lemma scalecAl : forall (h : R) ( x y : C_RnormedType), h *: ( x * y) = h *: x * y. @@ -180,6 +215,7 @@ End C_Rnormed. Section C_absRing. +(* Definition C_AbsRingMixin := @AbsRingMixin (complex_ringType R_rcfType) (@normc R_rcfType) normc0 normcN1 normcD (@normcM R_rcfType ) (@eq0_normc R_rcfType). @@ -206,17 +242,19 @@ Section C_absRing. Canonical absRing_normedType (K : absRingType) := [normedModType K^o of K for (AbsRing_NormedModType K)]. - Lemma abs_normE : forall ( K : absRingType) (x : K), `|x|%real = `|[x]|. - Proof. by []. Qed. +*) + +(* Lemma abs_normE : forall ( K : absRingType) (x : K), `|x|%real = `|[x]|. + Proof. by []. Qed.*) (*Delete absCE and adapt from abs_normE *) - Lemma absCE : forall x : C, `|x|%real = (normc x). - Proof. by []. Qed. +(* Lemma absCE : forall x : C, `|x|%real = (normc x). + Proof. by []. Qed.*) - Lemma normCR : forall x : R, `|[x%:C]| = `|x|%real. - Proof. Admitted. +(* Lemma normCR : forall x : R, `|[x%:C]| = `|x|%real. + Proof. Admitted.*) - Lemma absring_real_complex : forall r: R, forall x : R, AbsRing_ball 0 r x -> +(* Lemma absring_real_complex : forall r: R, forall x : R, AbsRing_ball 0 r x -> (AbsRing_ball 0%:C r x%:C). Proof. move => r x ballrx. @@ -235,7 +273,7 @@ Section C_absRing. rewrite addrC addr0 -scaleN1r normcZ normrN1 mul1r normc_i. move : ballrx ; rewrite /AbsRing_ball /ball_ absRE. by rewrite addrC addr0 normrN. - Qed. + Qed.*) Lemma scalei_muli : forall z : C^o, ('i * z) = ('i *: z). Proof. @@ -277,8 +315,8 @@ not just that the limit exists. *) Definition complex_Rnormed_absring : C_RnormedType -> C^o := id. Definition CauchyRiemanEq_R2 (f : C_RnormedType -> C_RnormedType) c := - let u := (fun c => Re ( f c)): C_RnormedType -> R^o in - let v:= (fun c => Im (f c)) : C_RnormedType -> R^o in + let u := (fun c => Re ( f c)): C_RnormedModType -> R^o in + let v:= (fun c => Im (f c)) : C_RnormedModType -> R^o in (* ('D_(1%:C) u = 'D_('i) v) /\ ('D_('i) u = 'D_(1%:C) v). *) (((derive u c (1%:C)) = (derive v c ('i))) /\ ((derive v c (1%:C)) = -(derive u c ('i)))). @@ -287,16 +325,15 @@ not just that the limit exists. *) Definition deriveC (V W : normedModType C)(f : V -> W) c v := lim ((fun (h: C^o) => h^-1 *: ((f \o shift c) (h *: v) - f c)) @ locally' 0). - Definition CauchyRiemanEq (f : C -> C) z := - 'i * lim ((fun h : R => h^-1 *: ((f \o shift z) (h *: 1%:C) - f z)) @ locally' 0) = - lim ((fun h : R => h^-1 *: ((f \o shift z) (h *: 'i%C) - f z)) @ locally' 0). + 'i * lim ((fun h : R => h^-1 *: ((f \o shift z) (h *: 1%:C) - f z)) @ (@locally' [topologicalType of R^o] 0)) = + lim ((fun h : R => h^-1 *: ((f \o shift z) (h *: 'i%C) - f z)) @ (@locally' [topologicalType of R^o] 0)). - Lemma eqCr (R : rcfType) (r s : R) : (r%:C == s%:C) = (r == s). + Lemma eqCr (r s : R) : (r%:C == s%:C) = (r == s). Proof. exact: (inj_eq (@complexI _)). Qed. - Lemma eqCI (R : rcfType) (r s : R) : (r*i == s*i) = (r == s). + Lemma eqCI (r s : R) : (r*i == s*i) = (r == s). Proof. Admitted. @@ -315,7 +352,7 @@ not just that the limit exists. *) Qed. - Lemma cvg_scaler (K : absRingType) (V : normedModType K) (T : topologicalType) + Lemma cvg_scaler (K : numFieldType) (V : normedModType K) (T : topologicalType) (F : set (set T)) (H :Filter F) (f : T -> V) (k : K) : cvg (f @ F) -> cvg ((k \*: f) @ F ). Proof. @@ -326,7 +363,7 @@ not just that the limit exists. *) (* cvg F -> ProperFilter F. *) - Lemma limin_scaler (K : absRingType) (V : normedModType K) (T : topologicalType) + Lemma limin_scaler (K : numFieldType) (V : normedModType K) (T : topologicalType) (F : set (set T)) (FF : ProperFilter F) (f : T -> V) (k : K) : cvg(f@F) -> k *: lim (f @ F) = lim ((k \*: f) @ F ). Proof. @@ -342,20 +379,19 @@ looked a long time of it as I was looking for a [filter of lim]* instead of a [filter of filter]*) (*There whould be a lemma analogous to [filter of lim] to ease the search *) - Lemma holo_derivable (f : C^o -> C^o) c : holomorphic f c -> (forall v:C , derivable (complex_realfun f) c v). Proof. move => /cvg_ex [l H]; rewrite /derivable => v. rewrite /type_of_filter /= in l H. set ff : C_RnormedType -> C_RnormedType := f. - set quotR := (X in (X @ locally' 0)). + set quotR := (X in (X @ _)). pose mulv (h :R):= (h *:v). pose quotC (h : C) : C^o := h^-1 *: ((f \o shift c) (h) - f c). (* here f : C -> C does not work - as if we needed C^o still for the normed structure*) case : (EM (v = 0)). - - move => eqv0 ; apply (cvgP (l := (0:C))). + - move => eqv0 ; apply (@cvgP _ _ _ (0:C)). have eqnear0 : {near locally' (0:R), 0 =1 quotR}. exists 1 => // h _ _ ; rewrite /quotR /shift eqv0. simpl. by rewrite scaler0 add0r addrN scaler0. @@ -547,4 +583,4 @@ Admitted. -End Holomorphe. \ No newline at end of file +End Holomorphe. From 3010cdca2768c97ea16afba0925cd1a3617d9064 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 30 Apr 2020 00:35:41 +0900 Subject: [PATCH 05/11] update cauchyetoile.v wrt PR#270 --- theories/cauchyetoile.v | 930 +++++++++++++++++++--------------------- 1 file changed, 444 insertions(+), 486 deletions(-) diff --git a/theories/cauchyetoile.v b/theories/cauchyetoile.v index 96421a9ac7..257bef9ed8 100644 --- a/theories/cauchyetoile.v +++ b/theories/cauchyetoile.v @@ -5,215 +5,256 @@ From mathcomp Require Import complex. From mathcomp Require Import boolp reals ereal derive. Require Import classical_sets posnum topology normedtype landau integral. -(*Pour distinguer fonctions mesurables et integrables, -utiliser des structures comme posrel. *) +(* Pour distinguer fonctions mesurables et integrables, utiliser des structures comme posrel. *) Import Order.TTheory GRing.Theory Num.Theory ComplexField Num.Def. Local Open Scope ring_scope. Local Open Scope classical_set_scope. Local Open Scope complex_scope. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. -(* Obligation Tactic := idtac. *) +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. -Section cauchyetoile. +Section complex_extras. Variable R : rcfType. +Local Notation sqrtr := Num.sqrt. +Local Notation C := R[i]. +Local Notation Re := (@complex.Re R). +Local Notation Im := (@complex.Im R). - Local Notation sgr := Num.sg. - Local Notation sqrtr := Num.sqrt. - Local Notation C := R[i]. - - Notation Re:= (@complex.Re R). - Notation Im:= (@complex.Im R). - - - (*Adapting lemma eq_complex from complex.v, - which was done in boolean style*) - Lemma eqE_complex : forall (x y : C), (x = y) = ((Re x = Re y) /\ (Im x = Im y)). - Proof. - move => [a b] [c d]; apply : propositional_extensionality ; split. - by move => -> ; split. - by case => //= -> ->. - Qed. - - Lemma Re0 : Re 0 = 0 :> R. - Proof. by []. Qed. - - Lemma Im0 : Im 0 = 0 :> R. - Proof. by []. Qed. - - Lemma ReIm_eq0 (x : C) : (x=0) = ((Re x = 0)/\(Im x = 0)). - Proof. - by rewrite -[in Re x= _]Re0 -Im0 -eqE_complex. - Qed. - - Lemma normc0 : normc 0 = 0 :> R . - Proof. - by rewrite /normc //= expr0n //= add0r sqrtr0. - Qed. - - Lemma normcN ( x : C) : normc (-x) = (normc x). - Admitted. - - Lemma normc_r (x : R) : normc (x%:C) = normr (x). - Proof. by rewrite /normc/= expr0n //= addr0 sqrtr_sqr. Qed. - - - Lemma normc_i (x : R) : normc (x*i) = normr (x). - Proof. by rewrite /normc/= expr0n //= add0r sqrtr_sqr. Qed. - - Lemma normcN1 : normc (-1%:C) = 1 :> R. - Proof. - by rewrite /normc/= oppr0 expr0n addr0 -signr_odd expr0 sqrtr1. - Qed. - - Lemma realtocomplex_additive : forall x y : R, (x + y)%:C = x%:C + y%:C. - Proof. - (*real_complex_additive*) - move => x y ; rewrite -!complexr0 eqE_complex //=. - by split ; last by rewrite addr0. - Qed. - - Lemma real_complex_inv : forall x : R, x%:C^-1 = (x^-1)%:C. - Proof. - Search _ (rmorphism _). - Admitted. - - Lemma Im_inv : ('i%C)^-1 = (-1*i) :> C. - Proof. Admitted. - - Lemma invcM : forall x y : C, (x*y)^-1 = x^-1 * y^-1. - (*Maybe another lemma is doing that, or invrM *) - Proof. Admitted. - -Lemma scale_inv : forall (h : R) (v : C), (h*:v)^-1 = h^-1 *: v^-1. - (*Maybe another lemma is doing that, or invrM *) - Proof. Admitted. - - - Lemma Im_mul : forall x : R, (x*i) = (x%:C * 'i%C). - Proof. by move => x ; simpc. Qed. - - Lemma normcD : forall ( x y : C), normc (x+y) <= (normc x + normc y). - Proof. - by move => x y ; rewrite -lecR realtocomplex_additive ; apply :lec_normD . - Qed. - - Lemma normcZ : forall (l : R) (x : C), normc (l *: x) = `|l| * (normc x). - Proof. - move => l [a b] ; rewrite /normc //= !exprMn. - rewrite -mulrDr sqrtrM ; last by rewrite sqr_ge0. - by rewrite sqrtr_sqr. - Qed. - - Lemma scalecr : forall w : C^o, forall r : R, (r *: w = r%:C *: w). - Proof. by move => [a b ] r; rewrite eqE_complex //=; split; simpc. Qed. +(*Adapting lemma eq_complex from complex.v, which was done in boolean style*) +Lemma eqE_complex : forall (x y : C), (x = y) = ((Re x = Re y) /\ (Im x = Im y)). +Proof. +move => [a b] [c d]; apply : propositional_extensionality ; split. +by move => -> ; split. +by case => //= -> ->. +Qed. + +Lemma Re0 : Re 0 = 0 :> R. +Proof. by []. Qed. + +Lemma Im0 : Im 0 = 0 :> R. +Proof. by []. Qed. + +Lemma ReIm_eq0 (x : C) : (x = 0) = ((Re x = 0) /\ (Im x = 0)). +Proof. by rewrite -[in Re x= _]Re0 -Im0 -eqE_complex. Qed. + +Lemma scalei_muli : forall z : C^o, 'i * z = 'i *: z. +Proof. by []. Qed. + +Lemma iE : 'i%C = 'i :> C. +Proof. by []. Qed. + +Lemma scaleC_mul : forall (w v : C^o), (v *: w = v * w). +Proof. by []. Qed. + +Lemma normc0 : normc 0 = 0 :> R . +Proof. by rewrite /normc //= expr0n //= add0r sqrtr0. Qed. + +Lemma normcN (x : C) : normc (- x) = normc x. +Proof. by case: x => a b /=; rewrite 2!sqrrN. Qed. + +Lemma normc_r (x : R) : normc (x%:C) = normr x. +Proof. by rewrite /normc/= expr0n //= addr0 sqrtr_sqr. Qed. + +Lemma normc_i (x : R) : normc (x*i) = normr x. +Proof. by rewrite /normc/= expr0n //= add0r sqrtr_sqr. Qed. + +Lemma normcN1 : normc (-1%:C) = 1 :> R. +Proof. by rewrite /normc/= oppr0 expr0n addr0 -signr_odd expr0 sqrtr1. Qed. + +Lemma realtocomplex_additive (x y : R) : (x + y)%:C = x%:C + y%:C. +Proof. +(*real_complex_additive*) +rewrite -!complexr0 eqE_complex //=; by split; last by rewrite addr0. +Qed. + +Lemma real_complex_inv (x : R) : x%:C^-1 = (x^-1)%:C. +Proof. +(* Search _ (rmorphism _). *) +have [/eqP->|x0] := boolP (x == 0); first by rewrite !invr0. +apply/eqP; rewrite eq_complex /= mul0r oppr0 eqxx andbT expr0n addr0. +by rewrite expr2 invrM ?unitfE // mulrA divrr ?unitfE // div1r. +Qed. + +Lemma Im_inv : ('i%C)^-1 = (-1 *i) :> C. +Proof. by rewrite complexiE invCi. Qed. + +Lemma invcM (x y : C) : (x * y)^-1 = x^-1 * y^-1. +Proof. +have [/eqP->|x0] := boolP (x == 0); first by rewrite !(invr0,mul0r). +have [/eqP->|y0] := boolP (y == 0); first by rewrite !(invr0,mulr0). +by rewrite invrM // mulrC. +Qed. + +Lemma Im_mul (x : R) : x *i = x%:C * 'i%C. +Proof. by simpc. Qed. + +Lemma normcD (x y : C) : normc (x + y) <= normc x + normc y. +Proof. by rewrite -lecR realtocomplex_additive; apply: lec_normD. Qed. + +Lemma normcZ (l : R) : forall (x : C), normc (l *: x) = `|l| * (normc x). +Proof. +by case=> ? ?; rewrite /normc //= !exprMn -mulrDr sqrtrM ?sqr_ge0 // sqrtr_sqr. +Qed. + +Lemma scalecr : forall w : C^o, forall r : R, (r *: w = r%:C *: w). +Proof. by move=> [a b] r; rewrite eqE_complex //=; split; simpc. Qed. Lemma normc_ge0 (x : C) : 0 <= normc x. Proof. case: x => ? ?; exact: sqrtr_ge0. Qed. +Lemma normc_gt0 (v : C) : (0 < normc v) = (v != 0). +Proof. +rewrite lt_neqAle normc_ge0 andbT; apply/idP/idP; apply/contra. +by move/eqP ->; rewrite normc0. +by rewrite eq_sym => /eqP/eq0_normc ->. +Qed. + Lemma mulrnc (a b : R) k : a +i* b *+ k = (a *+ k) +i* (b *+ k). Proof. by elim: k => // k ih; apply/eqP; rewrite !mulrS eq_complex !ih !eqxx. Qed. -Section C_Rnormed. - - (* Uniform.mixin_of takes a locally but does not expect a TopologicalType, which is inserted in the Uniform.class_of *) - (* Whereas NormedModule.mixin_of asks for a Uniform.mixin_of loc *) +Lemma normc_natmul (k : nat) : normc k%:R = k%:R :> R. +Proof. +by rewrite mulrnc /= mul0rn expr0n addr0 sqrtr_sqr ger0_norm // ler0n. +Qed. -(*Context (K : absRingType). Nor working with any K, how to close the real scope ? Do it before ? *) - - - Program Definition uniformmixin_of_normaxioms (V : lmodType R) (norm : V -> R) - (ax1 : forall x y : V, norm (x + y) <= norm x + norm y) - ( ax2 : forall (l : R) (x : V), norm (l *: x) = `|l| * (norm x)) - ( ax4 : forall x : V, norm x = 0 -> x = 0 ) : Uniform.mixin_of _ (locally_ (ball_ norm)) - := @Uniform.Mixin _ V (locally_ (ball_ norm)) (ball_ norm) _ _ _ _. - Next Obligation. - move => V norm _ H _ ; rewrite /ball_ => x e. - have -> : x - x = 0 . by rewrite addrN. - suff -> : norm 0 = 0 by []. - have -> : 0 = 0 *: x by rewrite scale0r. - by rewrite H normr0 mul0r. - Qed. - Next Obligation. - move => V norm _ H _ ; rewrite /ball_ => x e e0. - have -> : x - e = (-1) *: (e-x) by rewrite -opprB scaleN1r. - by rewrite (H (-1) (e-x)) normrN1 mul1r. - Qed. - Next Obligation. - move => V norm H _ _ ; rewrite /ball_ => x y z e1 e2 normxy normyz. - by rewrite (subr_trans y) (order.Order.POrderTheory.le_lt_trans (H _ _)) ?ltr_add. - Qed. - Next Obligation. by []. Qed. - - (*C as a R-lmodule *) - Definition C_RlmodMixin := (complex_lmodMixin R). (*R instead of R_rcfType is not working *) -(*LmodType is hard to use, not findable through Search and not checkable as abbreviation is not applied enough*) - Definition C_RlmodType := @LmodType R C C_RlmodMixin. - Definition C_pointedType := PointedType C 0. - Canonical C_pointedType. - Definition C_filteredType := FilteredType C C (locally_ (ball_ (@normc R))). - Canonical C_filteredType. - (*Are we sure that the above is canonical *) - - - Program Definition C_RuniformMixin := - @uniformmixin_of_normaxioms (complex_lmodType R) (@normc R) normcD normcZ (@eq0_normc R). - Definition C_RtopologicalMixin := topologyOfBallMixin C_RuniformMixin. -(* Definition C_RtopologicalType := TopologicalType C_filteredType C_RtopologicalMixin.*) -Canonical C_RtopologicalType := TopologicalType C C_RtopologicalMixin. -(* Definition C_RuniformType := @UniformType C_RtopologicalType C_RuniformMixin.*) -Canonical C_RuniformType := UniformType C C_RuniformMixin. - -Lemma normc_natmul (x : C) k : normc (x *+ k) = (normc x) *+ k. +Lemma normc_mulrn (x : C) k : normc (x *+ k) = (normc x) *+ k. Proof. -elim: k => [|k ih]; first by rewrite !mulr0n normc0. -rewrite !mulrS; apply/eqP; rewrite eq_le; apply/andP; split. - rewrite -ih; exact/normcD. -have [/eqP->|x0] := boolP (normc x == 0). - by rewrite mul0rn add0r normc_ge0. -case: x x0 ih; rewrite /normc => a b x0. -Admitted. +by rewrite -mulr_natr normcM -[in RHS]mulr_natr normc_natmul. +Qed. -Program Definition C_RnormedMixin := - @Num.NormedMixin _ _ _ _ normcD (@eq0_normc _) normc_natmul normcN. -Canonical C_RnormedType := NormedZmodType R C^o C_RnormedMixin. +Lemma gt0_normc (r : C) : 0 < r -> r = (normc r)%:C. +Proof. +move=> r0; have rr : r \is Num.real by rewrite realE (ltW r0). +rewrite /normc (complexE r) /=; simpc. +rewrite (ger0_Im (ltW r0)) expr0n addr0 sqrtr_sqr gtr0_norm ?complexr0 //. +by move: r0; rewrite {1}(complexE r) /=; simpc => /andP[/eqP]. +Qed. -Lemma normc_ball : - @ball _ [uniformType R of C^o] = ball_ (fun x => `| x |). -Proof. by []. Qed. +Lemma real_norm (b : R) : `|b%:C| = `|b|%:C. +Proof. by rewrite normc_def /= expr0n addr0 sqrtr_sqr. Qed. -Definition normc_UniformNormedZmodMixin := - UniformNormedZmodule.Mixin normc_ball. -Canonical normc_uniformNormedZmodType := - UniformNormedZmoduleType R C^o normc_UniformNormedZmodMixin. (* TODO: warning *) +Lemma eqCr (r s : R) : (r%:C == s%:C) = (r == s). +Proof. exact: (inj_eq (@complexI _)). Qed. -Definition C_RnormedModMixin := @NormedModMixin R normc_uniformNormedZmodType _ normcZ. -Canonical C_RnormedModType := - NormedModType R normc_uniformNormedZmodType C_RnormedModMixin. +Lemma eqCI (r s : R) : (r *i == s *i) = (r == s). +Proof. by apply/idP/idP => [/eqP[] ->//|/eqP ->]. Qed. -(* - Program Definition C_RnormedMixin - := @NormedModMixin R_absRingType C_RlmodType _ C_RuniformMixin (@normc R) normcD normcZ _ (@eq0_normc R) . - Next Obligation. by []. Qed. +Lemma scale_inv (h : R) (v : C) : h != 0 -> v != 0 -> (h *: v)^-1 = h^-1 *: v^-1. +Proof. +by move=> h0 v0; rewrite scalecr invrM // ?unitfE ?eqCr // mulrC scalecr real_complex_inv. +Qed. - Definition C_RnormedType : normedModType R := @NormedModType R C_RuniformType C_RnormedMixin. -*) +End complex_extras. - Lemma scalecAl : forall (h : R) ( x y : C_RnormedType), - h *: ( x * y) = h *: x * y. - Proof. move => h [a b] [c d]. simpc. Admitted. +Section C_Rnormed. +Variable R : rcfType. + + (* Uniform.mixin_of takes a locally but does not expect a TopologicalType, +which is inserted in the Uniform.class_of *) + (* Whereas NormedModule.mixin_of asks for a Uniform.mixin_of loc *) +(*Context (K : absRingType). Nor working with any K, how to close the real scope ? Do it before ? *) + +Program Definition uniformmixin_of_normaxioms (V : lmodType R) (norm : V -> R) + (ax1 : forall x y : V, norm (x + y) <= norm x + norm y) + (ax2 : forall (l : R) (x : V), norm (l *: x) = `|l| * (norm x)) + (ax4 : forall x : V, norm x = 0 -> x = 0 ) : Uniform.mixin_of _ (locally_ (ball_ norm)) := + @Uniform.Mixin _ V (locally_ (ball_ norm)) (ball_ norm) _ _ _ _. +Next Obligation. +move => V norm _ H _; rewrite /ball_ => x e. +rewrite subrr. +suff -> : norm 0 = 0 by []. +have -> : 0 = 0 *: x by rewrite scale0r. +by rewrite H normr0 mul0r. +Qed. +Next Obligation. +move => V norm _ H _ ; rewrite /ball_ => x e e0. +have -> : x - e = (-1) *: (e - x) by rewrite -opprB scaleN1r. +by rewrite (H (-1) (e - x)) normrN1 mul1r. +Qed. +Next Obligation. +move => V norm H _ _ ; rewrite /ball_ => x y z e1 e2 normxy normyz. +by rewrite (subr_trans y) (le_lt_trans (H _ _)) ?ltr_add. +Qed. +Next Obligation. by []. Qed. + +(*C as a R-lmodule *) +(*Definition C_RlmodMixin := (complex_lmodMixin R). +(*LmodType is hard to use, not findable through Search + and not checkable as abbreviation is not applied enough*) +Definition C_RlmodType := @LmodType R C C_RlmodMixin.*) +(*Are we sure that the above is canonical *) + +Local Notation C := R[i]. + +Definition C_pointedType := PointedType C 0. +Canonical C_pointedType. +Definition C_filteredType := FilteredType C C (locally_ (ball_ (@normc R))). +Canonical C_filteredType. + +(*Definition C_RtopologicalType := TopologicalType C_filteredType C_RtopologicalMixin.*) +(*Definition C_RtopologicalType := TopologicalType C C_RtopologicalMixin.*) +(*Definition C_RuniformType := @UniformType C_RtopologicalType C_RuniformMixin.*) +(*Definition C_RuniformType := UniformType C_RtopologicalType C_RuniformMixin.*) +(*Definition C_RnormedZmodType := NormedZmodType R C^o C_RnormedMixin.*) + +Definition Rcomplex := R[i]. +Canonical Rcomplex_eqType := [eqType of Rcomplex]. +Canonical Rcomplex_choiceType := [choiceType of Rcomplex]. +Canonical Rcomplex_zmodType := [zmodType of Rcomplex]. +Canonical Rcomplex_lmodType := [lmodType R of Rcomplex]. +Canonical Rcomplex_pointedType := [pointedType of Rcomplex]. +Canonical Rcomplex_filteredType := [filteredType Rcomplex of Rcomplex]. +Definition Rcomplex_uniformMixin := + @uniformmixin_of_normaxioms [lmodType R of Rcomplex] (@normc R) (@normcD _) (@normcZ _) (@eq0_normc _). +Definition Rcomplex_topologicalMixin := topologyOfBallMixin Rcomplex_uniformMixin. +Canonical Rcomplex_topologicalType := + TopologicalType Rcomplex Rcomplex_topologicalMixin. +Canonical Rcomplex_uniformType := UniformType Rcomplex Rcomplex_uniformMixin. +Definition Rcomplex_normedMixin := + @Num.NormedMixin _ _ _ _ (@normcD R) (@eq0_normc _) (@normc_mulrn _) (@normcN _). +Canonical Rcomplex_normedZmodType := NormedZmodType R Rcomplex Rcomplex_normedMixin. + +Lemma Rcomplex_ball_ball_ : + @ball _ [uniformType R of Rcomplex] = ball_ (fun x => `| x |). +Proof. by []. Qed. + +Definition Rcomplex_uniformNormedZmodMixin := + UniformNormedZmodule.Mixin Rcomplex_ball_ball_. +Canonical Rcomplex_uniformNormedZmodType := + UniformNormedZmodType R Rcomplex Rcomplex_uniformNormedZmodMixin. + +Definition Rcomplex_normedModMixin := + @NormedModMixin R [uniformNormedZmodType R of Rcomplex] _ (@normcZ _). +Canonical Rcomplex_normedModType := + NormedModType R Rcomplex Rcomplex_normedModMixin. + +Lemma scalecAl (h : R) (x y : Rcomplex_normedModType) : h *: (x * y) = h *: x * y. +Proof. +by move: h x y => h [a b] [c d]; simpc; rewrite -!mulrA -mulrBr -mulrDr. +Qed. - Definition C_RLalg := LalgType R C_RlmodType scalecAl. +Definition C_RLalg := LalgType R Rcomplex scalecAl. End C_Rnormed. - -Section C_absRing. +Section Holomorphe. +Variable R : rcfType. + +Local Notation sqrtr := Num.sqrt. +Local Notation C := R[i]. +Local Notation RComplex := (Rcomplex R). +Local Notation Re := (@complex.Re R). +Local Notation Im := (@complex.Im R). + +(*Important: C is a lmodType R while C^o is a lmodType C*) + +(*Section C_absRing.*) +(* This is now replaced by complex_numFieldType and numFieldType_normedModType.*) (* Definition C_AbsRingMixin := @AbsRingMixin (complex_ringType R_rcfType) @@ -222,365 +263,282 @@ Section C_absRing. Definition C_absRingType := AbsRingType C C_AbsRingMixin. Canonical C_absRingType. Definition C_topologicalType := [topologicalType of C for C_absRingType]. - Canonical C_topologicalType. + Canonical C_topologicalType. Definition C_uniformType := [uniformType of C for C_absRingType]. Canonical C_uniformType. Definition Co_pointedType := [pointedType of C^o for C_absRingType]. Definition Co_filteredType := [filteredType C^o of C^o for C_absRingType]. Definition Co_topologicalType := [topologicalType of C^o for C_absRingType]. - + Canonical Zmod_topologicalType ( K : absRingType) (V : normedModType K):= [topologicalType of [zmodType of V]]. - + Definition Co_uniformType := [uniformType of C^o for C_absRingType]. Definition Co_normedType := AbsRing_NormedModType C_absRingType. Canonical C_normedType := [normedModType C^o of C for Co_normedType]. (*C is convertible to C^o *) - + Canonical R_normedType := [normedModType R of R for [normedModType R of R^o]]. - - Canonical absRing_normedType (K : absRingType) := [normedModType K^o of K for (AbsRing_NormedModType K)]. + + Canonical absRing_normedType (K : absRingType) := [normedModType K^o +of K for (AbsRing_NormedModType K)]. *) -(* Lemma abs_normE : forall ( K : absRingType) (x : K), `|x|%real = `|[x]|. - Proof. by []. Qed.*) - - (*Delete absCE and adapt from abs_normE *) -(* Lemma absCE : forall x : C, `|x|%real = (normc x). - Proof. by []. Qed.*) - -(* Lemma normCR : forall x : R, `|[x%:C]| = `|x|%real. - Proof. Admitted.*) - -(* Lemma absring_real_complex : forall r: R, forall x : R, AbsRing_ball 0 r x -> - (AbsRing_ball 0%:C r x%:C). - Proof. - move => r x ballrx. - rewrite /AbsRing_ball /ball_ absCE. - rewrite addrC addr0 -scaleN1r normcZ normrN1 mul1r normc_r. - move : ballrx ; rewrite /AbsRing_ball /ball_ absRE. - by rewrite addrC addr0 normrN. - Qed. - - - Lemma absring_real_Im : forall r: R, forall x : R, AbsRing_ball 0 r x -> - (AbsRing_ball 0%:C r x*i). - Proof. - move => r x ballrx. - rewrite /AbsRing_ball /ball_ absCE. - rewrite addrC addr0 -scaleN1r normcZ normrN1 mul1r normc_i. - move : ballrx ; rewrite /AbsRing_ball /ball_ absRE. - by rewrite addrC addr0 normrN. - Qed.*) - - Lemma scalei_muli : forall z : C^o, ('i * z) = ('i *: z). - Proof. - by []. - Qed. - - Lemma iE : 'i%C = 'i :> C. - Proof. by []. Qed. - - Lemma scaleC_mul : forall (w v : C^o), (v *: w = v * w). - Proof. by []. Qed. - -End C_absRing. -Section Holomorphe. +(* NB: not used *) +Lemma cvg_translim (T : topologicalType) (F G: set (set T)) (l :T) : + F `=>` G -> (G --> l) -> (F --> l). +Proof. move => FG Gl. apply : cvg_trans; [exact : FG | exact : Gl]. Qed. + +Lemma cvg_scaler (K : numFieldType) (V : normedModType K) (T : topologicalType) + (F : set (set T)) (H :Filter F) (f : T -> V) (k : K) : + cvg (f @ F) -> cvg ((k \*: f) @ F ). +Proof. by move => /cvg_ex [l H0] ; apply: cvgP; apply: cvgZr; apply: H0. Qed. + +Lemma limin_scaler (K : numFieldType) (V : normedModType K) (T : topologicalType) + (F : set (set T)) (FF : ProperFilter F) (f : T -> V) (k : K) : + cvg(f @ F) -> k *: lim (f @ F) = lim ((k \*: f) @ F ). +Proof. by move => cv; apply/esym/cvg_lim; apply: cvgZr. Qed. -Print differentiable_def. (* used in derive.v, what does center means*) (*CoInductive -differentiable_def (K : absRingType) (V W : normedModType K) (f : V -> W) +differentiable_def (K : absRingType) (V W : normedModType K) (f : V -> W) (x : filter_on V) (phF : phantom (set (set V)) x) : Prop := DifferentiableDef : continuous 'd f x /\ f = (cst (f (lim x)) + 'd f x) \o center (lim x) +o_x center (lim x) -> differentiable_def f phF *) (*Diff is defined from any normedmodule of any absringtype, - so C is a normedmodul on itsself *) + so C is a normedmodul on itself *) (*Vague idea that this should work, as we see C^o as a vector space on C and not R*) - -(*Important : differentiable in derive.v, means continuoulsy differentiable, +(*Important : differentiable in derive.v, means continuoulsy differentiable, not just that the limit exists. *) (*derivable concerns only the existence of the derivative *) - Definition holomorphic (f : C^o -> C^o) (c: C^o) := - cvg ((fun (h:C^o)=> h^-1 *: ((f \o shift c) (h) - f c)) @ (locally' 0)). - - Definition complex_realfun (f : C^o -> C^o) : C_RnormedType -> C_RnormedType := f. - Arguments complex_realfun _ _ /. - - Definition complex_Rnormed_absring : C_RnormedType -> C^o := id. - - Definition CauchyRiemanEq_R2 (f : C_RnormedType -> C_RnormedType) c := - let u := (fun c => Re ( f c)): C_RnormedModType -> R^o in - let v:= (fun c => Im (f c)) : C_RnormedModType -> R^o in - (* ('D_(1%:C) u = 'D_('i) v) /\ ('D_('i) u = 'D_(1%:C) v). *) - (((derive u c (1%:C)) = - (derive v c ('i))) /\ ((derive v c (1%:C)) = -(derive u c ('i)))). - - - Definition deriveC (V W : normedModType C)(f : V -> W) c v := - lim ((fun (h: C^o) => h^-1 *: ((f \o shift c) (h *: v) - f c)) @ locally' 0). - - Definition CauchyRiemanEq (f : C -> C) z := - 'i * lim ((fun h : R => h^-1 *: ((f \o shift z) (h *: 1%:C) - f z)) @ (@locally' [topologicalType of R^o] 0)) = - lim ((fun h : R => h^-1 *: ((f \o shift z) (h *: 'i%C) - f z)) @ (@locally' [topologicalType of R^o] 0)). - - - Lemma eqCr (r s : R) : (r%:C == s%:C) = (r == s). - Proof. exact: (inj_eq (@complexI _)). Qed. - - Lemma eqCI (r s : R) : (r*i == s*i) = (r == s). - Proof. Admitted. - - -(*Lemma lim_trans (T : topologicalType) (F : set (set T)) -(G : set (set T)) (l : T) : ( F `=>` G ) -> (G --> l) -> ( F --> l). - move => FG Gl A x. - Search "lim" "trans". - *) - - Lemma cvg_translim (T : topologicalType) (F G: set (set T)) (l :T) : - F `=>` G -> (G --> l) -> (F --> l). - Proof. - move => FG Gl. apply : cvg_trans. - exact : FG. - exact : Gl. - Qed. - +Definition holomorphic (f : C^o -> C^o) (c : C^o) := + cvg ((fun (h : C^o) => h^-1 *: ((f \o shift c) h - f c)) @ (locally' (0:C^o))). - Lemma cvg_scaler (K : numFieldType) (V : normedModType K) (T : topologicalType) - (F : set (set T)) (H :Filter F) (f : T -> V) (k : K) : - cvg (f @ F) -> cvg ((k \*: f) @ F ). - Proof. - by move => /cvg_ex [l H0] ; apply: cvgP; apply: cvgZr; apply: H0. - Qed. +Definition complex_realfun (f : C^o -> C^o) : RComplex -> RComplex := f. +Arguments complex_realfun _ _ /. -(* Lemma cvg_proper_top (T : topologicalType) (F : set (set U)) (FF : Filter F) : *) -(* cvg F -> ProperFilter F. *) +Definition CauchyRiemanEq_R2 (f : RComplex -> RComplex) c := + let u := (fun c => Re (f c)) : RComplex -> R^o in + let v:= (fun c => Im (f c)) : RComplex -> R^o in + 'D_1%:C u c = 'D_'i v c /\ 'D_1%:C v c = - 'D_'i u c. +(* NB: not used *) ++Definition Cderivable (V W : normedModType C) (f : V -> W) := derivable f. - Lemma limin_scaler (K : numFieldType) (V : normedModType K) (T : topologicalType) - (F : set (set T)) (FF : ProperFilter F) (f : T -> V) (k : K) : - cvg(f@F) -> k *: lim (f @ F) = lim ((k \*: f) @ F ). - Proof. - move => cv. - symmetry. - by apply: cvg_lim; apply: cvgZr . - Qed. - +Definition CauchyRiemanEq (f : C -> C) z := + 'i * lim ((fun h : R => h^-1 *: ((f \o shift z) (h *: 1%:C) - f z)) @ (locally' (0:R^o))) = + lim ((fun h : R => h^-1 *: ((f \o shift z) (h *: 'i%C) - f z)) @ (locally' (0:R^o))). (*this could be done for scale also ... *) -(*I needed filter_of_filterE to make things easier - +(*I needed filter_of_filterE to make things easier - looked a long time of it as I was looking for a [filter of lim]* instead of a [filter of filter]*) -(*There whould be a lemma analogous to [filter of lim] to ease the search *) -Lemma holo_derivable (f : C^o -> C^o) c : holomorphic f c - -> (forall v:C , derivable (complex_realfun f) c v). +(*There should be a lemma analogous to [filter of lim] to ease the search *) + +Definition Rderivable (V W : normedModType R) (f : V -> W) := derivable f. + +(*The topological structure on R is given by R^o *) +Lemma holo_derivable (f : (C)^o -> (C)^o) c : + holomorphic f c -> (forall v : C, Rderivable (complex_realfun f) c v). Proof. - move => /cvg_ex [l H]; rewrite /derivable => v. - rewrite /type_of_filter /= in l H. - set ff : C_RnormedType -> C_RnormedType := f. - set quotR := (X in (X @ _)). - pose mulv (h :R):= (h *:v). - pose quotC (h : C) : C^o := h^-1 *: ((f \o shift c) (h) - f c). - (* here f : C -> C does not work - -as if we needed C^o still for the normed structure*) - case : (EM (v = 0)). - - move => eqv0 ; apply (@cvgP _ _ _ (0:C)). - have eqnear0 : {near locally' (0:R), 0 =1 quotR}. - exists 1 => // h _ _ ; rewrite /quotR /shift eqv0. simpl. - by rewrite scaler0 add0r addrN scaler0. - (*addrN is too hard to find through Search *) - apply: cvg_translim. - - exact (cvg_eq_loc eqnear0). - - by apply : cst_continuous. - (*WARNING : cvg_cst from normedtype applies only to endofunctions +move=> /cvg_ex [l H]; rewrite /Rderivable /derivable => v /=. +rewrite /type_of_filter /= in l H. +set ff : RComplex -> RComplex := f. +set quotR := (X in (X @ _)). +pose mulv (h : R) := (h *: v). +pose quotC (h : C) : C^o := h^-1 *: ((f \o shift c) h - f c). +case: (EM (v = 0)) => [eqv0|/eqP vneq0]. +- apply (cvgP (l := (0:RComplex))). + have eqnear0 : {near locally' (0:R^o), 0 =1 quotR}. + by exists 1=> // h _ _ ; rewrite /quotR /shift eqv0 /= scaler0 add0r addrN scaler0. + apply: cvg_trans. + + exact (cvg_eq_loc eqnear0). + + exact: cst_continuous. + (*cvg_cst from normedtype applies only to endofunctions That should NOT be the case, as one could use it insteas of cst_continuous *) - - move/eqP => vneq0 ; apply : (cvgP (l := v *: l)). (*chainage avant et suff *) - have eqnear0 : {near (locally' (0 : R)), (v \*: quotC) \o mulv =1 quotR}. - exists 1 => // h _ neq0h //=; rewrite /quotC /quotR /mulv scale_inv. - rewrite scalerAl scalerCA -scalecAl mulrA -(mulrC v) mulfV. - rewrite mul1r; apply: (scalerI (neq0h)). - by rewrite !scalerA //= (divff neq0h). - by []. - have subsetfilters: quotR @ locally' 0 `=>` (v \*: quotC) \o mulv @locally' 0. - by exact: (cvg_eq_loc eqnear0). - apply: cvg_trans subsetfilters _. - unshelve apply : cvg_comp. - - exact (locally' (0:C)). - - move => //= A [r [leq0r ballrA]]. - exists (r / (`|[v]|)). - - apply : mulr_gt0 ; first by []. - by rewrite invr_gt0 normm_gt0. - - move => b; rewrite /AbsRing_ball /ball_ sub0r absRE normrN => ballrb neqb0. - have ballCrb : (AbsRing_ball 0 r (mulv b)). - rewrite /AbsRing_ball /ball_ sub0r absrN /mulv scalecr absrM abs_normE. - rewrite -ltr_pdivl_mulr. - - by rewrite normCR. - by rewrite abs_normE normm_gt0. +- apply (cvgP (l := v *: l : RComplex)). + (*normedtype seem difficulut to infer *) + (*Est-ce que on peut faire cohabiter plusieurs normes ? *) + have eqnear0 : {near (locally' (0 : R^o)), (v \*: quotC) \o mulv =1 quotR}. + exists 1 => // h _ neq0h //=; rewrite /quotC /quotR /mulv scale_inv //. + rewrite scalerAl scalerCA -scalecAl mulrA -(mulrC v) mulfV // mul1r. + by apply: (scalerI neq0h); rewrite !scalerA //= (divff neq0h). + have subsetfilters : quotR @ locally' (0:R^o) `=>` (v \*: quotC) \o mulv @ locally' (0:R^o). + exact: (cvg_eq_loc eqnear0). + apply: cvg_trans subsetfilters _. + suff : v \*: quotC \o mulv @ locally' (0:R^o) `=>` locally (v *: l). + move/cvg_trans; apply. + (* locally (v *: l) `=>` [filter of v *: ]l *) + move=> a -[x x0 Hx]. + exists x%:C; first by rewrite ltcR. + by move=> /= y yx; apply Hx; rewrite /ball_ -ltcR. + apply: (@cvg_comp _ _ _ _ _ _ (locally' (0:C^o))). + + move => //= A [r leq0r ballrA]. + exists (normc r / normc v). + * rewrite mulr_gt0 //. + by rewrite normc_gt0 gt_eqF. + by rewrite invr_gt0 normc_gt0. + * move=> b; rewrite /ball_ sub0r normrN => ballrb neqb0. + have ballCrb : (@ball_ _ _ (fun x => `|x|) 0 r (mulv b)). + rewrite /ball_ sub0r normrN /mulv scalecr normrM. + rewrite ltr_pdivl_mulr in ballrb; last by rewrite normc_gt0. + rewrite -ltcR in ballrb. + rewrite -(ger0_norm (ltW leq0r)) (le_lt_trans _ ballrb) // rmorphM /=. + by rewrite le_eqVlt; apply/orP; left; apply/eqP; rewrite real_norm. have bneq0C : (b%:C != 0%:C) by move: neqb0; apply: contra; rewrite eqCr. - by apply: (ballrA (mulv b) ballCrb); rewrite scaler_eq0; apply/norP; split. - suff : v \*: quotC @ locally' (0 : C) --> v *: l by []. - by apply: cvgZr ; rewrite /quotC. -Qed. + by apply: (ballrA (mulv b) ballCrb); rewrite /mulv (@scaler_eq0 _ (C_RLalg R)); exact/norP. + + suff : v \*: quotC @ locally' (0 : (Rcomplex R)^o) --> v *: l by []. + by apply: cvgZr; rewrite /quotC. +Qed. -Lemma holo_CauchyRieman (f : C^o -> C^o) c: (holomorphic f c) -> (CauchyRiemanEq f c). +Lemma holo_CauchyRieman (f : C^o -> C^o) c : holomorphic f c -> CauchyRiemanEq f c. Proof. - move => H; rewrite /CauchyRiemanEq. - pose quotC := (fun h : C => h^-1 *: ((f \o shift c) (h) - f c)). - pose quotR := (fun h : R => h^-1 *: ((f \o shift c) (h *: 1%:C ) - f c)). - pose quotiR := (fun (h : R) => h^-1 *: ((f \o shift c) (h *: 'i%C) - f c)). - have eqnear0x : {near (locally' 0), quotC \o ( fun h => h *: 1%:C) =1 quotR}. - exists 1 ; first by [] ; move => h _ _ //=; simpc. - by rewrite /quotC /quotR real_complex_inv -scalecr; simpc. - pose subsetfiltersx := (cvg_eq_loc eqnear0x). - have -> : lim (quotR @ (locally' 0)) - = lim (quotC @ (locally' 0)). - apply: cvg_map_lim. - suff: quotR @ (locally' 0) `=>` (quotC @ (locally' 0)). - move => H1; apply: (cvg_translim H1) ; exact H. (*can't apply a view*) - apply : cvg_trans. - - exact : (subsetfiltersx (locally'_filter 0)). - move => {subsetfiltersx eqnear0x}. - - unshelve apply : cvg_comp. - (*just showing that linear maps preserve balls - - general lemma ? *) - - exact (locally' 0). - - move => A //= [r leq0r] absringrA. - exists r ; first by []. - move => h absrh hneq0 ; simpc. - apply : (absringrA h%:C). - - by apply : absring_real_complex. - - by rewrite eqCr . - by []. - have eqnear0y : {near (locally' 0), 'i \*:quotC \o ( fun h => h *: 'i%C) =1 quotiR }. - exists 1 ; first by [] ; move => h _ _ //= ; simpc. - rewrite /quotC /quotiR (Im_mul h) invcM. - rewrite scalerA real_complex_inv Im_inv !scalecr; simpc ; rewrite (Im_mul h). - by rewrite !real_complexE. - pose subsetfiltersy := (cvg_eq_loc eqnear0y). - have properlocally' : ProperFilter (locally'(0:C)). - (*This should be Canonical *) - split. - - rewrite /locally' /within => [[r leq0r] ballrwithin]; apply: (ballrwithin ((r/2)%:C) _). - rewrite /AbsRing_ball /ball_ absCE sub0r normcN //= . - rewrite expr0n //= addr0 sqrtr_sqr //= ger0_norm. - rewrite ltr_pdivr_mulr ; last by [] . - rewrite ltr_pmulr ; last by []. - by apply: ltr_spaddl. (* 1 < 2 *) - by apply : divr_ge0; apply ltrW. - have : (r / 2 != 0) by apply: mulf_neq0 ;apply: lt0r_neq0. - have -> : (0 = 0%:C) by move => K //=. - by apply: contra=> /eqP /complexI /eqP. - (* une vue permet d'abord d'utiliser une implication sur le terme - en tête sans avoir à l 'introduire*) - - by apply: locally'_filter. - have <- : lim (quotiR @ (locally' 0)) - = 'i * lim (quotC @ (locally' 0)). - have -> : 'i * lim (quotC @ (locally' 0)) - = lim ('i \*: quotC @ (locally' 0)). - rewrite scalei_muli limin_scaler; first by []. - by exact: H. - apply: cvg_map_lim. - suff: quotiR @ (locally' 0) - `=>` ('i \*: quotC @ (locally' 0)). - move => H1 ; apply: cvg_translim. - - exact: H1. - - by apply : cvg_scaler; exact : H. - apply: cvg_trans. - - apply : (subsetfiltersy (locally'_filter 0)). - move => {subsetfiltersx eqnear0x}. - - unshelve apply : cvg_comp. - - exact (locally' 0). - - move => A //= [r leq0r] absringrA. - exists r ; first by []. - move => h absrh hneq0; simpc. - apply: (absringrA). - - by apply : absring_real_Im. - - by rewrite eqCI. - rewrite filter_of_filterE. - by []. - by []. +move=> H; rewrite /CauchyRiemanEq. +pose quotC := fun h : C => h^-1 *: ((f \o shift c) h - f c). +pose quotR := fun h : R => h^-1 *: ((f \o shift c) (h *: 1%:C ) - f c) : RComplex. +pose quotiR := fun h : R => h^-1 *: ((f \o shift c) (h *: 'i%C) - f c) : (numFieldType_normedModType (complex_numFieldType R)). (*IMP*) (* pbm with cvg_map_lim*) +have eqnear0x : {near (locally' (0:R^o)), quotC \o (fun h => h *: 1%:C) =1 quotR}. + exists 1; first by []. + by move => h _ _ //=; simpc; rewrite /quotC /quotR real_complex_inv -scalecr; simpc. +pose subsetfiltersx := cvg_eq_loc eqnear0x. +have -> : lim (quotR @ (locally' (0:R^o))) = lim (quotC @ (locally' (0:C^o))). + apply: (@cvg_map_lim _ _). (*IMP*) + exact: Proper_locally'_numFieldType. + suff: quotR @ (locally' (0:R^o)) `=>` quotC @ (locally' (0:C^o)). + move/cvg_trans; apply. + have : cvg (quotC @ locally' (0:C^o)) by []. + move/cvg_trans; apply. + move=> /= s [x x0 xs]; exists x%:C; first by rewrite ltcR. + by move=> y xy; apply xs; move: xy; rewrite /ball_ -ltcR. + apply: cvg_trans. + - exact : (subsetfiltersx (locally'_filter (0:R^o))). + - move=> {subsetfiltersx eqnear0x}. + apply: (@cvg_comp _ _ _ _ _ _ (locally' (0:(Rcomplex R)^o))). + + move => s //= [r r0 rs]. + exists (normc r); first by rewrite normc_gt0 gt_eqF. + move=> h rh h0; simpc; apply: (rs h%:C); last by rewrite eqCr. + by move: rh; rewrite /ball_ !sub0r !normrN -ltcR real_norm {2}(gt0_normc r0). + + by []. +have eqnear0y : {near (locally' (0:R^o)), 'i \*:quotC \o ( fun h => h *: 'i%C) =1 quotiR}. + exists 1 ; first by [] ; move => h _ _ //= ; simpc. + rewrite /quotC /quotiR (Im_mul h) invcM. + rewrite scalerA real_complex_inv Im_inv !scalecr; simpc; rewrite (Im_mul h). + by rewrite !real_complexE. +pose subsetfiltersy := (cvg_eq_loc eqnear0y). +have properlocally' : ProperFilter (locally'(0:C^o)). + exact: Proper_locally'_numFieldType. +have <- : lim (quotiR @ (locally' (0:R^o))) = + 'i * lim (quotC @ (locally' (0:C^o))) . + have -> : 'i * lim (quotC @ (locally' (0:C^o))) = lim ('i \*: quotC @ (locally' (0:C^o))). + by rewrite scalei_muli limin_scaler. (* exact: H. *) + apply: cvg_map_lim. + exact: Proper_locally'_numFieldType. + suff : quotiR @ (locally' (0:R^o)) `=>` ('i \*: quotC @ (locally' (0:C^o))). + move=> H1 ; apply: cvg_trans. + exact: H1. + apply : cvg_scaler; exact : H. + apply: cvg_trans. + - by apply : (subsetfiltersy (locally'_filter 0)). + - move => {subsetfiltersx eqnear0x}. + unshelve apply : cvg_comp. + + exact (locally' (0:C^o)). + + move => A //= [r leq0r] absringrA. + exists (normc r); first by rewrite normc_gt0 gt_eqF. + move=> y ry y0. + apply absringrA. + move: ry; rewrite /ball_ !sub0r !normrN -ltcR {2}(gt0_normc leq0r) //. + rewrite scalecr normrM (_ : `|'i| = 1) ?mulr1 // ?real_norm //. + by rewrite normc_def /= expr0n expr1n add0r sqrtr1. + rewrite scalecr scaler_eq0 negb_or; apply/andP; split. + by rewrite eqCr. + by apply/eqP; case => /eqP; rewrite oner_eq0. + + by rewrite filter_of_filterE. +rewrite -/quotiR /lim_in /=; congr (get _). +rewrite funeqE => i; rewrite propeqE; split => /cvg_trans; apply. + move=> s [x x0 ix]; exists x%:C; first by rewrite ltcR. + by move=> y y0; apply ix; move: y0; rewrite /ball_ -ltcR. +move=> s [x x0 ix]; exists (normc x); first by rewrite normc_gt0 gt_eqF. +move=> y y0; apply ix; by move: y0; rewrite /ball_ -ltcR {2}(gt0_normc x0). Qed. - - (* Local Notation "''D_' v f" := (derive f ^~ v). *) (* Local Notation "''D_' v f c" := (derive f c v). *) -Print derive. - Lemma Diff_CR_holo (f : C -> C) : (*This does not work pointwise *) - (forall c v : C, derivable ( f : C_RnormedType -> C_RnormedType) c v) - /\ (forall c, CauchyRiemanEq f c) ->(forall c, (holomorphic f c)). +Lemma Diff_CR_holo (f : C -> C) : + (forall c v : C, derivable (f : Rcomplex_normedModType R -> Rcomplex_normedModType R) c v) /\ + (forall c, CauchyRiemanEq f c) -> + (forall c, (holomorphic f c)). (*sanity check : derivable (f : C ->C) does not type check *) - Proof. - move => [der CR] c. - (* (* first attempt with littleo but requires to mix littleo on filter on different types ...*) *) - suff : exists l, forall h : C_absRingType, - f (c + h) = f c + h * l + 'o_[filter of locally (0 : C)] id h. - admit. - move: (der c 1%:C ); simpl => /cvg_ex [lr /cvg_lim //= Dlr]. - move: (der c 'i); simpl => /cvg_ex [li /cvg_lim //= Dli]. - simpl in (type of lr); simpl in (type of Dlr). - simpl in (type of li); simpl in (type of Dli). - move : (CR c) ; rewrite /CauchyRiemanEq //= (Dlr) (Dli) => CRc. - pose l:= ((lr + lr*'i)) ; exists l; move => [a b]. - move: (der (c + a%:C) 'i); simpl => /cvg_ex [//= la /cvg_lim //= Dla]. - move: (der (c + a%:C) 'i) => /derivable_locallyxP. - rewrite /derive //= Dla => oR. - have -> : (a +i* b) = (a%:C + b*: 'i%C) by simpc. - rewrite addrA oR. - (*have fun a => la = cst(lr) + o_0(a). *) - move: (der c 1%:C); simpl => /derivable_locallyxP ; rewrite /derive //= Dlr => oC. - (* rewrite [a%:C]/(a *: 1%:C). *) - have -> : a%:C = (a *: 1%:C) by simpc. - rewrite oC. Print real_complex. - have lem : (fun a =>( la - lr)) = 'o_[ filter of locally (0:R)] (@real_complex R) . - (*tried : la - lr = 'o_[ filter of locally (0:R)] (@real_complex R) a :> C^o *) - move => s0. Check eqoE. - suff : (fun _ : R => la - lr) = 'a_o_[filter of locally (0:R)] (real_complex R). - admit. - move => s1. - - - apply: eqoE. (*eqoE and eqoP are not working*) apply: eqoE. apply: eqoE. - (* struggling with o *) - Search "o" in landau. - - (* (*another attempt*) *) - (* rewrite /holomorphic cvg_ex. *) - (* move: (der c 1%:C ); simpl => /cvg_ex [lr //= Dlr]. *) - (* move: (der c 'i); simpl => /cvg_ex [li //= Dli]. *) - (* simpl in (type of lr); simpl in (type of Dlr). *) - (* simpl in (type of li); simpl in (type of Dli). *) - (* move : (CR c) ; rewrite /CauchyRiemanEq //= (cvg_lim Dlr) (cvg_lim Dli) => CRc. *) - (* pose l:= ((lr + lr*'i)) ; exists l; move => A //= [r leq0r] normrA. *) - (* pose r':= r/(sqrtr 2). *) - (* have lrl : l / (1 + 'i*1) = lr. admit. *) - (* exists r ; first by []. *) - (* move => [a b] ballab abneq0 //=. *) - (* suff : normc (l- (a +i* b)^-1 *: ((f (a +i* b + c) - f c) : C^o)) <= r. *) - (* admit. *) - (* have : locally lr A. exists r'. *) - (* - by rewrite mulr_gt0 //= invr_gt0 sqrtr_gt0. *) - (* - move => t; rewrite /ball_ -lrl.admit. *) - (* (*we should have a tactic rewriting in any way that fits *) *) - (* move => /Dlr //=. *) - (* move : (Dli A) => //=. - *) - Admitted. - -Theorem CauchyRiemann (f : C^o -> C^o) c: ((holomorphic f c)) - <-> (forall v : C, derivable (complex_realfun f) c v) /\ (CauchyRiemanEq f c). Proof. +move => [der CR] c. +(* Before 270: first attempt with littleo but requires to mix + littleo on filter on different types. Check now*) +suff : exists l, forall h : C, + f (c + h) = f c + h * l + (('o_ (0 : [filteredType C^o of C^o]) id) : _ +-> numFieldType_normedModType (complex_numFieldType R) (*IMP*)) h. + admit. +(*This should be a lemma *) +move: (der c 1%:C ); simpl => /cvg_ex [lr /cvg_lim //= Dlr]. +move: (der c 'i); simpl => /cvg_ex [li /cvg_lim //= Dli]. +simpl in (type of lr); simpl in (type of Dlr). +simpl in (type of li); simpl in (type of Dli). +move : (CR c) ; rewrite /CauchyRiemanEq //= (Dlr) (Dli) => CRc. +pose l:= ((lr + lr*'i)) ; exists l; move => [a b]. +move: (der (c + a%:C) 'i); simpl => /cvg_ex [//= la /cvg_lim //= Dla]. +move: (der (c + a%:C) 'i) => /derivable_locallyxP. +have Htmp : ProperFilter ((fun h : R => h^-1 *: (f (h *: 'i%C + (c + a%:C)) - f (c + a%:C))) @ locally' (0:R^o)). + by apply fmap_proper_filter; apply Proper_locally'_numFieldType. +move: (Dla Htmp) => {}Dla. +rewrite /derive //= Dla => oR. +have -> : (a +i* b) = (a%:C + b*: 'i%C) by simpc. +rewrite addrA oR. +(*have fun a => la = cst(lr) + o_0(a). *) +move: (der c 1%:C); simpl => /derivable_locallyxP ; rewrite /derive //= Dlr => oC. +(* rewrite [a%:C]/(a *: 1%:C). *) +have -> : a%:C = (a *: 1%:C) by simpc. +rewrite oC. Print real_complex. +rewrite /type_of_filter /= in la Dla oR *. +have lem : ('o_ (0 : [filteredType R^o of R^o]) (@real_complex _ : _ -> numFieldType_normedModType (complex_numFieldType R) (*IMP*))) = + (fun a => (la - lr : C^o)). +move => s0. Check eqoE. +Fail suff : (fun _ : R => la - lr) = 'a_o_[filter of locally (0:R)] (real_complex R). +(* admit. +move => s1. + +apply: eqoE. (*eqoE and eqoP are not working*) apply: eqoE. apply: eqoE.*) + +(* (*another attempt*) *) +(* rewrite /holomorphic cvg_ex. *) +(* move: (der c 1%:C ); simpl => /cvg_ex [lr //= Dlr]. *) +(* move: (der c 'i); simpl => /cvg_ex [li //= Dli]. *) +(* simpl in (type of lr); simpl in (type of Dlr). *) +(* simpl in (type of li); simpl in (type of Dli). *) +(* move : (CR c) ; rewrite /CauchyRiemanEq //= (cvg_lim Dlr) (cvg_lim Dli) => CRc. *) +(* pose l:= ((lr + lr*'i)) ; exists l; move => A //= [r leq0r] normrA. *) +(* pose r':= r/(sqrtr 2). *) +(* have lrl : l / (1 + 'i*1) = lr. admit. *) +(* exists r ; first by []. *) +(* move => [a b] ballab abneq0 //=. *) +(* suff : normc (l- (a +i* b)^-1 *: ((f (a +i* b + c) - f c) : C^o)) <= r. *) +(* admit. *) +(* have : locally lr A. exists r'. *) +(* - by rewrite mulr_gt0 //= invr_gt0 sqrtr_gt0. *) +(* - move => t; rewrite /ball_ -lrl.admit. *) +(* (*we should have a tactic rewriting in any way that fits *) *) +(* move => /Dlr //=. *) +(* move : (Dli A) => //=. + *) Admitted. - - +Theorem CauchyRiemann (f : C^o -> C^o) c : (holomorphic f c) <-> + (forall v : C, derivable (complex_realfun f) c v) /\ (CauchyRiemanEq f c). +Proof. +Admitted. End Holomorphe. From e70d20114f9e418dd2edf90b3fa0e2442422b91e Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 30 Apr 2020 00:23:39 +0900 Subject: [PATCH 06/11] renaming: Uniform -> PseudoMetric --- theories/cauchyetoile.v | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/theories/cauchyetoile.v b/theories/cauchyetoile.v index 257bef9ed8..157fd53ecf 100644 --- a/theories/cauchyetoile.v +++ b/theories/cauchyetoile.v @@ -159,11 +159,11 @@ which is inserted in the Uniform.class_of *) (*Context (K : absRingType). Nor working with any K, how to close the real scope ? Do it before ? *) -Program Definition uniformmixin_of_normaxioms (V : lmodType R) (norm : V -> R) +Program Definition pseudometricmixin_of_normaxioms (V : lmodType R) (norm : V -> R) (ax1 : forall x y : V, norm (x + y) <= norm x + norm y) (ax2 : forall (l : R) (x : V), norm (l *: x) = `|l| * (norm x)) - (ax4 : forall x : V, norm x = 0 -> x = 0 ) : Uniform.mixin_of _ (locally_ (ball_ norm)) := - @Uniform.Mixin _ V (locally_ (ball_ norm)) (ball_ norm) _ _ _ _. + (ax4 : forall x : V, norm x = 0 -> x = 0 ) : PseudoMetric.mixin_of _ (locally_ (ball_ norm)) := + @PseudoMetric.Mixin _ V (locally_ (ball_ norm)) (ball_ norm) _ _ _ _. Next Obligation. move => V norm _ H _; rewrite /ball_ => x e. rewrite subrr. @@ -209,27 +209,27 @@ Canonical Rcomplex_zmodType := [zmodType of Rcomplex]. Canonical Rcomplex_lmodType := [lmodType R of Rcomplex]. Canonical Rcomplex_pointedType := [pointedType of Rcomplex]. Canonical Rcomplex_filteredType := [filteredType Rcomplex of Rcomplex]. -Definition Rcomplex_uniformMixin := - @uniformmixin_of_normaxioms [lmodType R of Rcomplex] (@normc R) (@normcD _) (@normcZ _) (@eq0_normc _). -Definition Rcomplex_topologicalMixin := topologyOfBallMixin Rcomplex_uniformMixin. +Definition Rcomplex_pseudoMetricMixin := + @pseudometricmixin_of_normaxioms [lmodType R of Rcomplex] (@normc R) (@normcD _) (@normcZ _) (@eq0_normc _). +Definition Rcomplex_topologicalMixin := topologyOfBallMixin Rcomplex_pseudoMetricMixin. Canonical Rcomplex_topologicalType := TopologicalType Rcomplex Rcomplex_topologicalMixin. -Canonical Rcomplex_uniformType := UniformType Rcomplex Rcomplex_uniformMixin. +Canonical Rcomplex_pseudoMetricType := PseudoMetricType Rcomplex Rcomplex_pseudoMetricMixin. Definition Rcomplex_normedMixin := @Num.NormedMixin _ _ _ _ (@normcD R) (@eq0_normc _) (@normc_mulrn _) (@normcN _). Canonical Rcomplex_normedZmodType := NormedZmodType R Rcomplex Rcomplex_normedMixin. Lemma Rcomplex_ball_ball_ : - @ball _ [uniformType R of Rcomplex] = ball_ (fun x => `| x |). + @ball _ [pseudoMetricType R of Rcomplex] = ball_ (fun x => `| x |). Proof. by []. Qed. -Definition Rcomplex_uniformNormedZmodMixin := - UniformNormedZmodule.Mixin Rcomplex_ball_ball_. -Canonical Rcomplex_uniformNormedZmodType := - UniformNormedZmodType R Rcomplex Rcomplex_uniformNormedZmodMixin. +Definition Rcomplex_pseudoMetricNormedZmodMixin := + PseudoMetricNormedZmodule.Mixin Rcomplex_ball_ball_. +Canonical Rcomplex_pseudoMetricNormedZmodType := + PseudoMetricNormedZmodType R Rcomplex Rcomplex_pseudoMetricNormedZmodMixin. Definition Rcomplex_normedModMixin := - @NormedModMixin R [uniformNormedZmodType R of Rcomplex] _ (@normcZ _). + @NormedModMixin R [pseudoMetricNormedZmodType R of Rcomplex] _ (@normcZ _). Canonical Rcomplex_normedModType := NormedModType R Rcomplex Rcomplex_normedModMixin. From f47b4974bc35370af8bbb8eb09b3b4b7519614e2 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Mon, 3 Feb 2020 19:29:53 +0100 Subject: [PATCH 07/11] wip Co-Authored-By: Georges Gonthier --- theories/cauchyetoile.v | 57 ++++++++++++++++++++++++++++++++++++++--- 1 file changed, 53 insertions(+), 4 deletions(-) diff --git a/theories/cauchyetoile.v b/theories/cauchyetoile.v index 157fd53ecf..9c9ab48d3e 100644 --- a/theories/cauchyetoile.v +++ b/theories/cauchyetoile.v @@ -242,6 +242,39 @@ Definition C_RLalg := LalgType R Rcomplex scalecAl. End C_Rnormed. +Canonical regular_pointedType (R: pointedType) := + [pointedType of R^o]. + +Canonical regular_normedZmodType (R: numDomainType) (V: normedZmodType R) := + [normedZmodType R of V^o]. + +Canonical regular_numDomainType (R: numDomainType) := + [numDomainType of R^o]. + +Canonical regular_numFieldType (R: numFieldType) := + [numFieldType of R^o]. + +Canonical regular_rcfType (R: rcfType) := + [rcfType of R^o]. + +Canonical regular_filteredType U (R: filteredType U) := + [filteredType U of R^o]. + +Canonical regular_topologicalType (R : topologicalType) := + [topologicalType of R^o]. + +Canonical regular_uniformType U (R : uniformType U):= + [uniformType U of R^o]. +(*Update the header of topologicaltype.v *) + +Canonical regular_completeType U (R : completeType U) := + @Complete.clone U R^o _ _ id. + +(*Update the syntax for completeType *) + +(*To be added at least to normedmodule.v*) + + Section Holomorphe. Variable R : rcfType. @@ -397,12 +430,13 @@ case: (EM (v = 0)) => [eqv0|/eqP vneq0]. by apply: cvgZr; rewrite /quotC. Qed. + Lemma holo_CauchyRieman (f : C^o -> C^o) c : holomorphic f c -> CauchyRiemanEq f c. Proof. move=> H; rewrite /CauchyRiemanEq. -pose quotC := fun h : C => h^-1 *: ((f \o shift c) h - f c). -pose quotR := fun h : R => h^-1 *: ((f \o shift c) (h *: 1%:C ) - f c) : RComplex. -pose quotiR := fun h : R => h^-1 *: ((f \o shift c) (h *: 'i%C) - f c) : (numFieldType_normedModType (complex_numFieldType R)). (*IMP*) (* pbm with cvg_map_lim*) +pose quotC := fun h : C => h^-1 *: ((f \o shift c) h - f c) : C^o. +pose quotR := fun h : R => h^-1 *: ((f \o shift c) (h *: 1%:C ) - f c) : (Rcomplex R). +pose quotiR := fun h : R => h^-1 *: ((f \o shift c) (h *: 'i%C) - f c): C^o. (* : (numFieldType_normedModType (complex_numFieldType R)). *) have eqnear0x : {near (locally' (0:R^o)), quotC \o (fun h => h *: 1%:C) =1 quotR}. exists 1; first by []. by move => h _ _ //=; simpc; rewrite /quotC /quotR real_complex_inv -scalecr; simpc. @@ -437,7 +471,20 @@ have <- : lim (quotiR @ (locally' (0:R^o))) = 'i * lim (quotC @ (locally' (0:C^o))) . have -> : 'i * lim (quotC @ (locally' (0:C^o))) = lim ('i \*: quotC @ (locally' (0:C^o))). by rewrite scalei_muli limin_scaler. (* exact: H. *) - apply: cvg_map_lim. + Set Printing All. Set Printing Depth 20. + (*simpl. + rewrite {1}/type_of_filter.*) (*too violent*) + have := cvg_map_lim _ . + rewrite {1}/Choice.sort. + rewrite {1}/Filtered.fpointedType. + rewrite {1}/Pointed.choiceType. + rewrite {1}/Pointed.sort. + rewrite {1}/Filtered.sort {1}/Filtered.clone. + apply. + (* apply: (@cvg_map_lim _ _ ). *) + (* C and C^o are too alike and Coq avoids + computing the nec. projections. + Instead it computes the can structures *) exact: Proper_locally'_numFieldType. suff : quotiR @ (locally' (0:R^o)) `=>` ('i \*: quotC @ (locally' (0:C^o))). move=> H1 ; apply: cvg_trans. @@ -467,6 +514,8 @@ move=> s [x x0 ix]; exists (normc x); first by rewrite normc_gt0 gt_eqF. move=> y y0; apply ix; by move: y0; rewrite /ball_ -ltcR {2}(gt0_normc x0). Qed. + + (* Local Notation "''D_' v f" := (derive f ^~ v). *) (* Local Notation "''D_' v f c" := (derive f c v). *) From 7f431b8e7f82d5a2ea6fa458c4fe4f92f1ba0478 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 30 Apr 2020 00:21:02 +0900 Subject: [PATCH 08/11] update cauchyetoile.v --- theories/cauchyetoile.v | 29 +++++++++++++---------------- 1 file changed, 13 insertions(+), 16 deletions(-) diff --git a/theories/cauchyetoile.v b/theories/cauchyetoile.v index 9c9ab48d3e..4d4d7d9b55 100644 --- a/theories/cauchyetoile.v +++ b/theories/cauchyetoile.v @@ -263,9 +263,8 @@ Canonical regular_filteredType U (R: filteredType U) := Canonical regular_topologicalType (R : topologicalType) := [topologicalType of R^o]. -Canonical regular_uniformType U (R : uniformType U):= - [uniformType U of R^o]. -(*Update the header of topologicaltype.v *) +Canonical regular_pseudoMetricType U (R : pseudoMetricType U):= + [pseudoMetricType U of R^o]. Canonical regular_completeType U (R : completeType U) := @Complete.clone U R^o _ _ id. @@ -319,7 +318,6 @@ of K for (AbsRing_NormedModType K)]. *) - (* NB: not used *) Lemma cvg_translim (T : topologicalType) (F G: set (set T)) (l :T) : F `=>` G -> (G --> l) -> (F --> l). @@ -333,7 +331,7 @@ Proof. by move => /cvg_ex [l H0] ; apply: cvgP; apply: cvgZr; apply: H0. Qed. Lemma limin_scaler (K : numFieldType) (V : normedModType K) (T : topologicalType) (F : set (set T)) (FF : ProperFilter F) (f : T -> V) (k : K) : cvg(f @ F) -> k *: lim (f @ F) = lim ((k \*: f) @ F ). -Proof. by move => cv; apply/esym/cvg_lim; apply: cvgZr. Qed. +Proof. by move => cv; apply/esym/cvg_lim => //; apply: cvgZr. Qed. (* used in derive.v, what does center means*) (*CoInductive @@ -361,7 +359,7 @@ Definition CauchyRiemanEq_R2 (f : RComplex -> RComplex) c := 'D_1%:C u c = 'D_'i v c /\ 'D_1%:C v c = - 'D_'i u c. (* NB: not used *) -+Definition Cderivable (V W : normedModType C) (f : V -> W) := derivable f. +Definition Cderivable (V W : normedModType C) (f : V -> W) := derivable f. Definition CauchyRiemanEq (f : C -> C) z := 'i * lim ((fun h : R => h^-1 *: ((f \o shift z) (h *: 1%:C) - f z)) @ (locally' (0:R^o))) = @@ -377,7 +375,7 @@ looked a long time of it as I was looking for a [filter of lim]* Definition Rderivable (V W : normedModType R) (f : V -> W) := derivable f. (*The topological structure on R is given by R^o *) -Lemma holo_derivable (f : (C)^o -> (C)^o) c : +Lemma holo_derivable (f : C^o -> C^o) c : holomorphic f c -> (forall v : C, Rderivable (complex_realfun f) c v). Proof. move=> /cvg_ex [l H]; rewrite /Rderivable /derivable => v /=. @@ -389,14 +387,15 @@ pose quotC (h : C) : C^o := h^-1 *: ((f \o shift c) h - f c). case: (EM (v = 0)) => [eqv0|/eqP vneq0]. - apply (cvgP (l := (0:RComplex))). have eqnear0 : {near locally' (0:R^o), 0 =1 quotR}. - by exists 1=> // h _ _ ; rewrite /quotR /shift eqv0 /= scaler0 add0r addrN scaler0. + exists 1 => // h _ _. + by rewrite /quotR /shift eqv0 /= scaler0 add0r addrN scaler0. apply: cvg_trans. + exact (cvg_eq_loc eqnear0). + exact: cst_continuous. (*cvg_cst from normedtype applies only to endofunctions That should NOT be the case, as one could use it insteas of cst_continuous *) - apply (cvgP (l := v *: l : RComplex)). - (*normedtype seem difficulut to infer *) + (*normedtype seem difficult to infer *) (*Est-ce que on peut faire cohabiter plusieurs normes ? *) have eqnear0 : {near (locally' (0 : R^o)), (v \*: quotC) \o mulv =1 quotR}. exists 1 => // h _ neq0h //=; rewrite /quotC /quotR /mulv scale_inv //. @@ -442,7 +441,7 @@ have eqnear0x : {near (locally' (0:R^o)), quotC \o (fun h => h *: 1%:C) =1 quotR by move => h _ _ //=; simpc; rewrite /quotC /quotR real_complex_inv -scalecr; simpc. pose subsetfiltersx := cvg_eq_loc eqnear0x. have -> : lim (quotR @ (locally' (0:R^o))) = lim (quotC @ (locally' (0:C^o))). - apply: (@cvg_map_lim _ _). (*IMP*) + apply: (@cvg_map_lim _ _) => //. (*IMP*) exact: Proper_locally'_numFieldType. suff: quotR @ (locally' (0:R^o)) `=>` quotC @ (locally' (0:C^o)). move/cvg_trans; apply. @@ -471,7 +470,7 @@ have <- : lim (quotiR @ (locally' (0:R^o))) = 'i * lim (quotC @ (locally' (0:C^o))) . have -> : 'i * lim (quotC @ (locally' (0:C^o))) = lim ('i \*: quotC @ (locally' (0:C^o))). by rewrite scalei_muli limin_scaler. (* exact: H. *) - Set Printing All. Set Printing Depth 20. + (*Set Printing All. Set Printing Depth 20.*) (*simpl. rewrite {1}/type_of_filter.*) (*too violent*) have := cvg_map_lim _ . @@ -480,7 +479,7 @@ have <- : lim (quotiR @ (locally' (0:R^o))) = rewrite {1}/Pointed.choiceType. rewrite {1}/Pointed.sort. rewrite {1}/Filtered.sort {1}/Filtered.clone. - apply. + apply => //. (* apply: (@cvg_map_lim _ _ ). *) (* C and C^o are too alike and Coq avoids computing the nec. projections. @@ -514,8 +513,6 @@ move=> s [x x0 ix]; exists (normc x); first by rewrite normc_gt0 gt_eqF. move=> y y0; apply ix; by move: y0; rewrite /ball_ -ltcR {2}(gt0_normc x0). Qed. - - (* Local Notation "''D_' v f" := (derive f ^~ v). *) (* Local Notation "''D_' v f c" := (derive f c v). *) @@ -537,13 +534,13 @@ move: (der c 1%:C ); simpl => /cvg_ex [lr /cvg_lim //= Dlr]. move: (der c 'i); simpl => /cvg_ex [li /cvg_lim //= Dli]. simpl in (type of lr); simpl in (type of Dlr). simpl in (type of li); simpl in (type of Dli). -move : (CR c) ; rewrite /CauchyRiemanEq //= (Dlr) (Dli) => CRc. +move : (CR c) ; rewrite /CauchyRiemanEq //= Dlr // Dli // => CRc. pose l:= ((lr + lr*'i)) ; exists l; move => [a b]. move: (der (c + a%:C) 'i); simpl => /cvg_ex [//= la /cvg_lim //= Dla]. move: (der (c + a%:C) 'i) => /derivable_locallyxP. have Htmp : ProperFilter ((fun h : R => h^-1 *: (f (h *: 'i%C + (c + a%:C)) - f (c + a%:C))) @ locally' (0:R^o)). by apply fmap_proper_filter; apply Proper_locally'_numFieldType. -move: (Dla Htmp) => {}Dla. +move: (Dla (@normedModType_hausdorff _ _) Htmp) => {}Dla. rewrite /derive //= Dla => oR. have -> : (a +i* b) = (a%:C + b*: 'i%C) by simpc. rewrite addrA oR. From cfaf5e7650da51e3531368279ebe4cc6e6b04d47 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 30 Apr 2020 02:02:31 +0900 Subject: [PATCH 09/11] fix to compile --- _CoqProject | 1 + theories/cauchyetoile.v | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/_CoqProject b/_CoqProject index 488adb57dd..2b7629d27a 100644 --- a/_CoqProject +++ b/_CoqProject @@ -16,6 +16,7 @@ theories/normedtype.v theories/forms.v theories/derive.v theories/summability.v +theories/cauchyetoile.v theories/altreals/xfinmap.v theories/altreals/discrete.v theories/altreals/realseq.v diff --git a/theories/cauchyetoile.v b/theories/cauchyetoile.v index 4d4d7d9b55..c7d77a8dd1 100644 --- a/theories/cauchyetoile.v +++ b/theories/cauchyetoile.v @@ -3,7 +3,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool. From mathcomp Require Import ssrnat eqtype choice fintype bigop order ssralg ssrnum. From mathcomp Require Import complex. From mathcomp Require Import boolp reals ereal derive. -Require Import classical_sets posnum topology normedtype landau integral. +Require Import classical_sets posnum topology normedtype landau. (* Pour distinguer fonctions mesurables et integrables, utiliser des structures comme posrel. *) Import Order.TTheory GRing.Theory Num.Theory ComplexField Num.Def. From 7be3df2bfa2ba791df782ee31965460b566c9b30 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 14 May 2020 20:59:55 +0900 Subject: [PATCH 10/11] update wrt master --- theories/cauchyetoile.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/theories/cauchyetoile.v b/theories/cauchyetoile.v index c7d77a8dd1..474df5b275 100644 --- a/theories/cauchyetoile.v +++ b/theories/cauchyetoile.v @@ -385,16 +385,16 @@ set quotR := (X in (X @ _)). pose mulv (h : R) := (h *: v). pose quotC (h : C) : C^o := h^-1 *: ((f \o shift c) h - f c). case: (EM (v = 0)) => [eqv0|/eqP vneq0]. -- apply (cvgP (l := (0:RComplex))). +- apply (@cvgP _ _ _ (0:RComplex)). have eqnear0 : {near locally' (0:R^o), 0 =1 quotR}. exists 1 => // h _ _. by rewrite /quotR /shift eqv0 /= scaler0 add0r addrN scaler0. apply: cvg_trans. - + exact (cvg_eq_loc eqnear0). - + exact: cst_continuous. + + exact (near_eq_cvg eqnear0). + + exact: cvg_cst. (*cvg_cst from normedtype applies only to endofunctions That should NOT be the case, as one could use it insteas of cst_continuous *) -- apply (cvgP (l := v *: l : RComplex)). +- apply (@cvgP _ _ _ (v *: l : RComplex)). (*normedtype seem difficult to infer *) (*Est-ce que on peut faire cohabiter plusieurs normes ? *) have eqnear0 : {near (locally' (0 : R^o)), (v \*: quotC) \o mulv =1 quotR}. @@ -402,7 +402,7 @@ case: (EM (v = 0)) => [eqv0|/eqP vneq0]. rewrite scalerAl scalerCA -scalecAl mulrA -(mulrC v) mulfV // mul1r. by apply: (scalerI neq0h); rewrite !scalerA //= (divff neq0h). have subsetfilters : quotR @ locally' (0:R^o) `=>` (v \*: quotC) \o mulv @ locally' (0:R^o). - exact: (cvg_eq_loc eqnear0). + exact: (near_eq_cvg eqnear0). apply: cvg_trans subsetfilters _. suff : v \*: quotC \o mulv @ locally' (0:R^o) `=>` locally (v *: l). move/cvg_trans; apply. @@ -439,7 +439,7 @@ pose quotiR := fun h : R => h^-1 *: ((f \o shift c) (h *: 'i%C) - f c): C^o. (* have eqnear0x : {near (locally' (0:R^o)), quotC \o (fun h => h *: 1%:C) =1 quotR}. exists 1; first by []. by move => h _ _ //=; simpc; rewrite /quotC /quotR real_complex_inv -scalecr; simpc. -pose subsetfiltersx := cvg_eq_loc eqnear0x. +pose subsetfiltersx := near_eq_cvg eqnear0x. have -> : lim (quotR @ (locally' (0:R^o))) = lim (quotC @ (locally' (0:C^o))). apply: (@cvg_map_lim _ _) => //. (*IMP*) exact: Proper_locally'_numFieldType. @@ -463,7 +463,7 @@ have eqnear0y : {near (locally' (0:R^o)), 'i \*:quotC \o ( fun h => h *: 'i%C) = rewrite /quotC /quotiR (Im_mul h) invcM. rewrite scalerA real_complex_inv Im_inv !scalecr; simpc; rewrite (Im_mul h). by rewrite !real_complexE. -pose subsetfiltersy := (cvg_eq_loc eqnear0y). +pose subsetfiltersy := (near_eq_cvg eqnear0y). have properlocally' : ProperFilter (locally'(0:C^o)). exact: Proper_locally'_numFieldType. have <- : lim (quotiR @ (locally' (0:R^o))) = @@ -540,7 +540,7 @@ move: (der (c + a%:C) 'i); simpl => /cvg_ex [//= la /cvg_lim //= Dla]. move: (der (c + a%:C) 'i) => /derivable_locallyxP. have Htmp : ProperFilter ((fun h : R => h^-1 *: (f (h *: 'i%C + (c + a%:C)) - f (c + a%:C))) @ locally' (0:R^o)). by apply fmap_proper_filter; apply Proper_locally'_numFieldType. -move: (Dla (@normedModType_hausdorff _ _) Htmp) => {}Dla. +move: (Dla (@norm_hausdorff _ _) Htmp) => {}Dla. rewrite /derive //= Dla => oR. have -> : (a +i* b) = (a%:C + b*: 'i%C) by simpc. rewrite addrA oR. From e09c8a2684f21a3a85d0936a809aa887087243f9 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 14 May 2020 15:15:29 +0200 Subject: [PATCH 11/11] name change --- theories/cauchyetoile.v | 590 ---------------------------------------- 1 file changed, 590 deletions(-) delete mode 100644 theories/cauchyetoile.v diff --git a/theories/cauchyetoile.v b/theories/cauchyetoile.v deleted file mode 100644 index 474df5b275..0000000000 --- a/theories/cauchyetoile.v +++ /dev/null @@ -1,590 +0,0 @@ -(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) -From mathcomp Require Import ssreflect ssrfun ssrbool. -From mathcomp Require Import ssrnat eqtype choice fintype bigop order ssralg ssrnum. -From mathcomp Require Import complex. -From mathcomp Require Import boolp reals ereal derive. -Require Import classical_sets posnum topology normedtype landau. - -(* Pour distinguer fonctions mesurables et integrables, utiliser des structures comme posrel. *) -Import Order.TTheory GRing.Theory Num.Theory ComplexField Num.Def. -Local Open Scope ring_scope. -Local Open Scope classical_set_scope. -Local Open Scope complex_scope. - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. - -Section complex_extras. -Variable R : rcfType. -Local Notation sqrtr := Num.sqrt. -Local Notation C := R[i]. -Local Notation Re := (@complex.Re R). -Local Notation Im := (@complex.Im R). - -(*Adapting lemma eq_complex from complex.v, which was done in boolean style*) -Lemma eqE_complex : forall (x y : C), (x = y) = ((Re x = Re y) /\ (Im x = Im y)). -Proof. -move => [a b] [c d]; apply : propositional_extensionality ; split. -by move => -> ; split. -by case => //= -> ->. -Qed. - -Lemma Re0 : Re 0 = 0 :> R. -Proof. by []. Qed. - -Lemma Im0 : Im 0 = 0 :> R. -Proof. by []. Qed. - -Lemma ReIm_eq0 (x : C) : (x = 0) = ((Re x = 0) /\ (Im x = 0)). -Proof. by rewrite -[in Re x= _]Re0 -Im0 -eqE_complex. Qed. - -Lemma scalei_muli : forall z : C^o, 'i * z = 'i *: z. -Proof. by []. Qed. - -Lemma iE : 'i%C = 'i :> C. -Proof. by []. Qed. - -Lemma scaleC_mul : forall (w v : C^o), (v *: w = v * w). -Proof. by []. Qed. - -Lemma normc0 : normc 0 = 0 :> R . -Proof. by rewrite /normc //= expr0n //= add0r sqrtr0. Qed. - -Lemma normcN (x : C) : normc (- x) = normc x. -Proof. by case: x => a b /=; rewrite 2!sqrrN. Qed. - -Lemma normc_r (x : R) : normc (x%:C) = normr x. -Proof. by rewrite /normc/= expr0n //= addr0 sqrtr_sqr. Qed. - -Lemma normc_i (x : R) : normc (x*i) = normr x. -Proof. by rewrite /normc/= expr0n //= add0r sqrtr_sqr. Qed. - -Lemma normcN1 : normc (-1%:C) = 1 :> R. -Proof. by rewrite /normc/= oppr0 expr0n addr0 -signr_odd expr0 sqrtr1. Qed. - -Lemma realtocomplex_additive (x y : R) : (x + y)%:C = x%:C + y%:C. -Proof. -(*real_complex_additive*) -rewrite -!complexr0 eqE_complex //=; by split; last by rewrite addr0. -Qed. - -Lemma real_complex_inv (x : R) : x%:C^-1 = (x^-1)%:C. -Proof. -(* Search _ (rmorphism _). *) -have [/eqP->|x0] := boolP (x == 0); first by rewrite !invr0. -apply/eqP; rewrite eq_complex /= mul0r oppr0 eqxx andbT expr0n addr0. -by rewrite expr2 invrM ?unitfE // mulrA divrr ?unitfE // div1r. -Qed. - -Lemma Im_inv : ('i%C)^-1 = (-1 *i) :> C. -Proof. by rewrite complexiE invCi. Qed. - -Lemma invcM (x y : C) : (x * y)^-1 = x^-1 * y^-1. -Proof. -have [/eqP->|x0] := boolP (x == 0); first by rewrite !(invr0,mul0r). -have [/eqP->|y0] := boolP (y == 0); first by rewrite !(invr0,mulr0). -by rewrite invrM // mulrC. -Qed. - -Lemma Im_mul (x : R) : x *i = x%:C * 'i%C. -Proof. by simpc. Qed. - -Lemma normcD (x y : C) : normc (x + y) <= normc x + normc y. -Proof. by rewrite -lecR realtocomplex_additive; apply: lec_normD. Qed. - -Lemma normcZ (l : R) : forall (x : C), normc (l *: x) = `|l| * (normc x). -Proof. -by case=> ? ?; rewrite /normc //= !exprMn -mulrDr sqrtrM ?sqr_ge0 // sqrtr_sqr. -Qed. - -Lemma scalecr : forall w : C^o, forall r : R, (r *: w = r%:C *: w). -Proof. by move=> [a b] r; rewrite eqE_complex //=; split; simpc. Qed. - -Lemma normc_ge0 (x : C) : 0 <= normc x. -Proof. case: x => ? ?; exact: sqrtr_ge0. Qed. - -Lemma normc_gt0 (v : C) : (0 < normc v) = (v != 0). -Proof. -rewrite lt_neqAle normc_ge0 andbT; apply/idP/idP; apply/contra. -by move/eqP ->; rewrite normc0. -by rewrite eq_sym => /eqP/eq0_normc ->. -Qed. - -Lemma mulrnc (a b : R) k : a +i* b *+ k = (a *+ k) +i* (b *+ k). -Proof. -by elim: k => // k ih; apply/eqP; rewrite !mulrS eq_complex !ih !eqxx. -Qed. - -Lemma normc_natmul (k : nat) : normc k%:R = k%:R :> R. -Proof. -by rewrite mulrnc /= mul0rn expr0n addr0 sqrtr_sqr ger0_norm // ler0n. -Qed. - -Lemma normc_mulrn (x : C) k : normc (x *+ k) = (normc x) *+ k. -Proof. -by rewrite -mulr_natr normcM -[in RHS]mulr_natr normc_natmul. -Qed. - -Lemma gt0_normc (r : C) : 0 < r -> r = (normc r)%:C. -Proof. -move=> r0; have rr : r \is Num.real by rewrite realE (ltW r0). -rewrite /normc (complexE r) /=; simpc. -rewrite (ger0_Im (ltW r0)) expr0n addr0 sqrtr_sqr gtr0_norm ?complexr0 //. -by move: r0; rewrite {1}(complexE r) /=; simpc => /andP[/eqP]. -Qed. - -Lemma real_norm (b : R) : `|b%:C| = `|b|%:C. -Proof. by rewrite normc_def /= expr0n addr0 sqrtr_sqr. Qed. - -Lemma eqCr (r s : R) : (r%:C == s%:C) = (r == s). -Proof. exact: (inj_eq (@complexI _)). Qed. - -Lemma eqCI (r s : R) : (r *i == s *i) = (r == s). -Proof. by apply/idP/idP => [/eqP[] ->//|/eqP ->]. Qed. - -Lemma scale_inv (h : R) (v : C) : h != 0 -> v != 0 -> (h *: v)^-1 = h^-1 *: v^-1. -Proof. -by move=> h0 v0; rewrite scalecr invrM // ?unitfE ?eqCr // mulrC scalecr real_complex_inv. -Qed. - -End complex_extras. - -Section C_Rnormed. -Variable R : rcfType. - - (* Uniform.mixin_of takes a locally but does not expect a TopologicalType, -which is inserted in the Uniform.class_of *) - (* Whereas NormedModule.mixin_of asks for a Uniform.mixin_of loc *) - -(*Context (K : absRingType). Nor working with any K, how to close the real scope ? Do it before ? *) - -Program Definition pseudometricmixin_of_normaxioms (V : lmodType R) (norm : V -> R) - (ax1 : forall x y : V, norm (x + y) <= norm x + norm y) - (ax2 : forall (l : R) (x : V), norm (l *: x) = `|l| * (norm x)) - (ax4 : forall x : V, norm x = 0 -> x = 0 ) : PseudoMetric.mixin_of _ (locally_ (ball_ norm)) := - @PseudoMetric.Mixin _ V (locally_ (ball_ norm)) (ball_ norm) _ _ _ _. -Next Obligation. -move => V norm _ H _; rewrite /ball_ => x e. -rewrite subrr. -suff -> : norm 0 = 0 by []. -have -> : 0 = 0 *: x by rewrite scale0r. -by rewrite H normr0 mul0r. -Qed. -Next Obligation. -move => V norm _ H _ ; rewrite /ball_ => x e e0. -have -> : x - e = (-1) *: (e - x) by rewrite -opprB scaleN1r. -by rewrite (H (-1) (e - x)) normrN1 mul1r. -Qed. -Next Obligation. -move => V norm H _ _ ; rewrite /ball_ => x y z e1 e2 normxy normyz. -by rewrite (subr_trans y) (le_lt_trans (H _ _)) ?ltr_add. -Qed. -Next Obligation. by []. Qed. - -(*C as a R-lmodule *) -(*Definition C_RlmodMixin := (complex_lmodMixin R). -(*LmodType is hard to use, not findable through Search - and not checkable as abbreviation is not applied enough*) -Definition C_RlmodType := @LmodType R C C_RlmodMixin.*) -(*Are we sure that the above is canonical *) - -Local Notation C := R[i]. - -Definition C_pointedType := PointedType C 0. -Canonical C_pointedType. -Definition C_filteredType := FilteredType C C (locally_ (ball_ (@normc R))). -Canonical C_filteredType. - -(*Definition C_RtopologicalType := TopologicalType C_filteredType C_RtopologicalMixin.*) -(*Definition C_RtopologicalType := TopologicalType C C_RtopologicalMixin.*) -(*Definition C_RuniformType := @UniformType C_RtopologicalType C_RuniformMixin.*) -(*Definition C_RuniformType := UniformType C_RtopologicalType C_RuniformMixin.*) -(*Definition C_RnormedZmodType := NormedZmodType R C^o C_RnormedMixin.*) - -Definition Rcomplex := R[i]. -Canonical Rcomplex_eqType := [eqType of Rcomplex]. -Canonical Rcomplex_choiceType := [choiceType of Rcomplex]. -Canonical Rcomplex_zmodType := [zmodType of Rcomplex]. -Canonical Rcomplex_lmodType := [lmodType R of Rcomplex]. -Canonical Rcomplex_pointedType := [pointedType of Rcomplex]. -Canonical Rcomplex_filteredType := [filteredType Rcomplex of Rcomplex]. -Definition Rcomplex_pseudoMetricMixin := - @pseudometricmixin_of_normaxioms [lmodType R of Rcomplex] (@normc R) (@normcD _) (@normcZ _) (@eq0_normc _). -Definition Rcomplex_topologicalMixin := topologyOfBallMixin Rcomplex_pseudoMetricMixin. -Canonical Rcomplex_topologicalType := - TopologicalType Rcomplex Rcomplex_topologicalMixin. -Canonical Rcomplex_pseudoMetricType := PseudoMetricType Rcomplex Rcomplex_pseudoMetricMixin. -Definition Rcomplex_normedMixin := - @Num.NormedMixin _ _ _ _ (@normcD R) (@eq0_normc _) (@normc_mulrn _) (@normcN _). -Canonical Rcomplex_normedZmodType := NormedZmodType R Rcomplex Rcomplex_normedMixin. - -Lemma Rcomplex_ball_ball_ : - @ball _ [pseudoMetricType R of Rcomplex] = ball_ (fun x => `| x |). -Proof. by []. Qed. - -Definition Rcomplex_pseudoMetricNormedZmodMixin := - PseudoMetricNormedZmodule.Mixin Rcomplex_ball_ball_. -Canonical Rcomplex_pseudoMetricNormedZmodType := - PseudoMetricNormedZmodType R Rcomplex Rcomplex_pseudoMetricNormedZmodMixin. - -Definition Rcomplex_normedModMixin := - @NormedModMixin R [pseudoMetricNormedZmodType R of Rcomplex] _ (@normcZ _). -Canonical Rcomplex_normedModType := - NormedModType R Rcomplex Rcomplex_normedModMixin. - -Lemma scalecAl (h : R) (x y : Rcomplex_normedModType) : h *: (x * y) = h *: x * y. -Proof. -by move: h x y => h [a b] [c d]; simpc; rewrite -!mulrA -mulrBr -mulrDr. -Qed. - -Definition C_RLalg := LalgType R Rcomplex scalecAl. - -End C_Rnormed. - -Canonical regular_pointedType (R: pointedType) := - [pointedType of R^o]. - -Canonical regular_normedZmodType (R: numDomainType) (V: normedZmodType R) := - [normedZmodType R of V^o]. - -Canonical regular_numDomainType (R: numDomainType) := - [numDomainType of R^o]. - -Canonical regular_numFieldType (R: numFieldType) := - [numFieldType of R^o]. - -Canonical regular_rcfType (R: rcfType) := - [rcfType of R^o]. - -Canonical regular_filteredType U (R: filteredType U) := - [filteredType U of R^o]. - -Canonical regular_topologicalType (R : topologicalType) := - [topologicalType of R^o]. - -Canonical regular_pseudoMetricType U (R : pseudoMetricType U):= - [pseudoMetricType U of R^o]. - -Canonical regular_completeType U (R : completeType U) := - @Complete.clone U R^o _ _ id. - -(*Update the syntax for completeType *) - -(*To be added at least to normedmodule.v*) - - -Section Holomorphe. -Variable R : rcfType. - -Local Notation sqrtr := Num.sqrt. -Local Notation C := R[i]. -Local Notation RComplex := (Rcomplex R). -Local Notation Re := (@complex.Re R). -Local Notation Im := (@complex.Im R). - -(*Important: C is a lmodType R while C^o is a lmodType C*) - -(*Section C_absRing.*) -(* This is now replaced by complex_numFieldType and numFieldType_normedModType.*) - -(* - Definition C_AbsRingMixin := @AbsRingMixin (complex_ringType R_rcfType) - (@normc R_rcfType) normc0 normcN1 normcD (@normcM R_rcfType ) - (@eq0_normc R_rcfType). - Definition C_absRingType := AbsRingType C C_AbsRingMixin. - Canonical C_absRingType. - Definition C_topologicalType := [topologicalType of C for C_absRingType]. - Canonical C_topologicalType. - Definition C_uniformType := [uniformType of C for C_absRingType]. - Canonical C_uniformType. - Definition Co_pointedType := [pointedType of C^o for C_absRingType]. - Definition Co_filteredType := [filteredType C^o of C^o for C_absRingType]. - Definition Co_topologicalType := [topologicalType of C^o for C_absRingType]. - - Canonical Zmod_topologicalType ( K : absRingType) - (V : normedModType K):= - [topologicalType of [zmodType of V]]. - - Definition Co_uniformType := [uniformType of C^o for C_absRingType]. - Definition Co_normedType := AbsRing_NormedModType C_absRingType. - Canonical C_normedType := [normedModType C^o of C for Co_normedType]. - (*C is convertible to C^o *) - - Canonical R_normedType := [normedModType R of R for [normedModType R of R^o]]. - - Canonical absRing_normedType (K : absRingType) := [normedModType K^o -of K for (AbsRing_NormedModType K)]. - -*) - -(* NB: not used *) -Lemma cvg_translim (T : topologicalType) (F G: set (set T)) (l :T) : - F `=>` G -> (G --> l) -> (F --> l). -Proof. move => FG Gl. apply : cvg_trans; [exact : FG | exact : Gl]. Qed. - -Lemma cvg_scaler (K : numFieldType) (V : normedModType K) (T : topologicalType) - (F : set (set T)) (H :Filter F) (f : T -> V) (k : K) : - cvg (f @ F) -> cvg ((k \*: f) @ F ). -Proof. by move => /cvg_ex [l H0] ; apply: cvgP; apply: cvgZr; apply: H0. Qed. - -Lemma limin_scaler (K : numFieldType) (V : normedModType K) (T : topologicalType) - (F : set (set T)) (FF : ProperFilter F) (f : T -> V) (k : K) : - cvg(f @ F) -> k *: lim (f @ F) = lim ((k \*: f) @ F ). -Proof. by move => cv; apply/esym/cvg_lim => //; apply: cvgZr. Qed. - -(* used in derive.v, what does center means*) -(*CoInductive -differentiable_def (K : absRingType) (V W : normedModType K) (f : V -> W) -(x : filter_on V) (phF : phantom (set (set V)) x) : Prop := - DifferentiableDef : continuous 'd f x /\ f = (cst (f (lim x)) + 'd f x) \o - center (lim x) +o_x center (lim x) -> differentiable_def f phF *) -(*Diff is defined from any normedmodule of any absringtype, - so C is a normedmodul on itself *) -(*Vague idea that this should work, as we see C^o as a vector space on C and not R*) - -(*Important : differentiable in derive.v, means continuoulsy differentiable, -not just that the limit exists. *) -(*derivable concerns only the existence of the derivative *) - -Definition holomorphic (f : C^o -> C^o) (c : C^o) := - cvg ((fun (h : C^o) => h^-1 *: ((f \o shift c) h - f c)) @ (locally' (0:C^o))). - -Definition complex_realfun (f : C^o -> C^o) : RComplex -> RComplex := f. -Arguments complex_realfun _ _ /. - -Definition CauchyRiemanEq_R2 (f : RComplex -> RComplex) c := - let u := (fun c => Re (f c)) : RComplex -> R^o in - let v:= (fun c => Im (f c)) : RComplex -> R^o in - 'D_1%:C u c = 'D_'i v c /\ 'D_1%:C v c = - 'D_'i u c. - -(* NB: not used *) -Definition Cderivable (V W : normedModType C) (f : V -> W) := derivable f. - -Definition CauchyRiemanEq (f : C -> C) z := - 'i * lim ((fun h : R => h^-1 *: ((f \o shift z) (h *: 1%:C) - f z)) @ (locally' (0:R^o))) = - lim ((fun h : R => h^-1 *: ((f \o shift z) (h *: 'i%C) - f z)) @ (locally' (0:R^o))). -(*this could be done for scale also ... *) - -(*I needed filter_of_filterE to make things easier - -looked a long time of it as I was looking for a [filter of lim]* - instead of a [filter of filter]*) - -(*There should be a lemma analogous to [filter of lim] to ease the search *) - -Definition Rderivable (V W : normedModType R) (f : V -> W) := derivable f. - -(*The topological structure on R is given by R^o *) -Lemma holo_derivable (f : C^o -> C^o) c : - holomorphic f c -> (forall v : C, Rderivable (complex_realfun f) c v). -Proof. -move=> /cvg_ex [l H]; rewrite /Rderivable /derivable => v /=. -rewrite /type_of_filter /= in l H. -set ff : RComplex -> RComplex := f. -set quotR := (X in (X @ _)). -pose mulv (h : R) := (h *: v). -pose quotC (h : C) : C^o := h^-1 *: ((f \o shift c) h - f c). -case: (EM (v = 0)) => [eqv0|/eqP vneq0]. -- apply (@cvgP _ _ _ (0:RComplex)). - have eqnear0 : {near locally' (0:R^o), 0 =1 quotR}. - exists 1 => // h _ _. - by rewrite /quotR /shift eqv0 /= scaler0 add0r addrN scaler0. - apply: cvg_trans. - + exact (near_eq_cvg eqnear0). - + exact: cvg_cst. - (*cvg_cst from normedtype applies only to endofunctions - That should NOT be the case, as one could use it insteas of cst_continuous *) -- apply (@cvgP _ _ _ (v *: l : RComplex)). - (*normedtype seem difficult to infer *) - (*Est-ce que on peut faire cohabiter plusieurs normes ? *) - have eqnear0 : {near (locally' (0 : R^o)), (v \*: quotC) \o mulv =1 quotR}. - exists 1 => // h _ neq0h //=; rewrite /quotC /quotR /mulv scale_inv //. - rewrite scalerAl scalerCA -scalecAl mulrA -(mulrC v) mulfV // mul1r. - by apply: (scalerI neq0h); rewrite !scalerA //= (divff neq0h). - have subsetfilters : quotR @ locally' (0:R^o) `=>` (v \*: quotC) \o mulv @ locally' (0:R^o). - exact: (near_eq_cvg eqnear0). - apply: cvg_trans subsetfilters _. - suff : v \*: quotC \o mulv @ locally' (0:R^o) `=>` locally (v *: l). - move/cvg_trans; apply. - (* locally (v *: l) `=>` [filter of v *: ]l *) - move=> a -[x x0 Hx]. - exists x%:C; first by rewrite ltcR. - by move=> /= y yx; apply Hx; rewrite /ball_ -ltcR. - apply: (@cvg_comp _ _ _ _ _ _ (locally' (0:C^o))). - + move => //= A [r leq0r ballrA]. - exists (normc r / normc v). - * rewrite mulr_gt0 //. - by rewrite normc_gt0 gt_eqF. - by rewrite invr_gt0 normc_gt0. - * move=> b; rewrite /ball_ sub0r normrN => ballrb neqb0. - have ballCrb : (@ball_ _ _ (fun x => `|x|) 0 r (mulv b)). - rewrite /ball_ sub0r normrN /mulv scalecr normrM. - rewrite ltr_pdivl_mulr in ballrb; last by rewrite normc_gt0. - rewrite -ltcR in ballrb. - rewrite -(ger0_norm (ltW leq0r)) (le_lt_trans _ ballrb) // rmorphM /=. - by rewrite le_eqVlt; apply/orP; left; apply/eqP; rewrite real_norm. - have bneq0C : (b%:C != 0%:C) by move: neqb0; apply: contra; rewrite eqCr. - by apply: (ballrA (mulv b) ballCrb); rewrite /mulv (@scaler_eq0 _ (C_RLalg R)); exact/norP. - + suff : v \*: quotC @ locally' (0 : (Rcomplex R)^o) --> v *: l by []. - by apply: cvgZr; rewrite /quotC. -Qed. - - -Lemma holo_CauchyRieman (f : C^o -> C^o) c : holomorphic f c -> CauchyRiemanEq f c. -Proof. -move=> H; rewrite /CauchyRiemanEq. -pose quotC := fun h : C => h^-1 *: ((f \o shift c) h - f c) : C^o. -pose quotR := fun h : R => h^-1 *: ((f \o shift c) (h *: 1%:C ) - f c) : (Rcomplex R). -pose quotiR := fun h : R => h^-1 *: ((f \o shift c) (h *: 'i%C) - f c): C^o. (* : (numFieldType_normedModType (complex_numFieldType R)). *) -have eqnear0x : {near (locally' (0:R^o)), quotC \o (fun h => h *: 1%:C) =1 quotR}. - exists 1; first by []. - by move => h _ _ //=; simpc; rewrite /quotC /quotR real_complex_inv -scalecr; simpc. -pose subsetfiltersx := near_eq_cvg eqnear0x. -have -> : lim (quotR @ (locally' (0:R^o))) = lim (quotC @ (locally' (0:C^o))). - apply: (@cvg_map_lim _ _) => //. (*IMP*) - exact: Proper_locally'_numFieldType. - suff: quotR @ (locally' (0:R^o)) `=>` quotC @ (locally' (0:C^o)). - move/cvg_trans; apply. - have : cvg (quotC @ locally' (0:C^o)) by []. - move/cvg_trans; apply. - move=> /= s [x x0 xs]; exists x%:C; first by rewrite ltcR. - by move=> y xy; apply xs; move: xy; rewrite /ball_ -ltcR. - apply: cvg_trans. - - exact : (subsetfiltersx (locally'_filter (0:R^o))). - - move=> {subsetfiltersx eqnear0x}. - apply: (@cvg_comp _ _ _ _ _ _ (locally' (0:(Rcomplex R)^o))). - + move => s //= [r r0 rs]. - exists (normc r); first by rewrite normc_gt0 gt_eqF. - move=> h rh h0; simpc; apply: (rs h%:C); last by rewrite eqCr. - by move: rh; rewrite /ball_ !sub0r !normrN -ltcR real_norm {2}(gt0_normc r0). - + by []. -have eqnear0y : {near (locally' (0:R^o)), 'i \*:quotC \o ( fun h => h *: 'i%C) =1 quotiR}. - exists 1 ; first by [] ; move => h _ _ //= ; simpc. - rewrite /quotC /quotiR (Im_mul h) invcM. - rewrite scalerA real_complex_inv Im_inv !scalecr; simpc; rewrite (Im_mul h). - by rewrite !real_complexE. -pose subsetfiltersy := (near_eq_cvg eqnear0y). -have properlocally' : ProperFilter (locally'(0:C^o)). - exact: Proper_locally'_numFieldType. -have <- : lim (quotiR @ (locally' (0:R^o))) = - 'i * lim (quotC @ (locally' (0:C^o))) . - have -> : 'i * lim (quotC @ (locally' (0:C^o))) = lim ('i \*: quotC @ (locally' (0:C^o))). - by rewrite scalei_muli limin_scaler. (* exact: H. *) - (*Set Printing All. Set Printing Depth 20.*) - (*simpl. - rewrite {1}/type_of_filter.*) (*too violent*) - have := cvg_map_lim _ . - rewrite {1}/Choice.sort. - rewrite {1}/Filtered.fpointedType. - rewrite {1}/Pointed.choiceType. - rewrite {1}/Pointed.sort. - rewrite {1}/Filtered.sort {1}/Filtered.clone. - apply => //. - (* apply: (@cvg_map_lim _ _ ). *) - (* C and C^o are too alike and Coq avoids - computing the nec. projections. - Instead it computes the can structures *) - exact: Proper_locally'_numFieldType. - suff : quotiR @ (locally' (0:R^o)) `=>` ('i \*: quotC @ (locally' (0:C^o))). - move=> H1 ; apply: cvg_trans. - exact: H1. - apply : cvg_scaler; exact : H. - apply: cvg_trans. - - by apply : (subsetfiltersy (locally'_filter 0)). - - move => {subsetfiltersx eqnear0x}. - unshelve apply : cvg_comp. - + exact (locally' (0:C^o)). - + move => A //= [r leq0r] absringrA. - exists (normc r); first by rewrite normc_gt0 gt_eqF. - move=> y ry y0. - apply absringrA. - move: ry; rewrite /ball_ !sub0r !normrN -ltcR {2}(gt0_normc leq0r) //. - rewrite scalecr normrM (_ : `|'i| = 1) ?mulr1 // ?real_norm //. - by rewrite normc_def /= expr0n expr1n add0r sqrtr1. - rewrite scalecr scaler_eq0 negb_or; apply/andP; split. - by rewrite eqCr. - by apply/eqP; case => /eqP; rewrite oner_eq0. - + by rewrite filter_of_filterE. -rewrite -/quotiR /lim_in /=; congr (get _). -rewrite funeqE => i; rewrite propeqE; split => /cvg_trans; apply. - move=> s [x x0 ix]; exists x%:C; first by rewrite ltcR. - by move=> y y0; apply ix; move: y0; rewrite /ball_ -ltcR. -move=> s [x x0 ix]; exists (normc x); first by rewrite normc_gt0 gt_eqF. -move=> y y0; apply ix; by move: y0; rewrite /ball_ -ltcR {2}(gt0_normc x0). -Qed. - -(* Local Notation "''D_' v f" := (derive f ^~ v). *) -(* Local Notation "''D_' v f c" := (derive f c v). *) - -Lemma Diff_CR_holo (f : C -> C) : - (forall c v : C, derivable (f : Rcomplex_normedModType R -> Rcomplex_normedModType R) c v) /\ - (forall c, CauchyRiemanEq f c) -> - (forall c, (holomorphic f c)). - (*sanity check : derivable (f : C ->C) does not type check *) -Proof. -move => [der CR] c. -(* Before 270: first attempt with littleo but requires to mix - littleo on filter on different types. Check now*) -suff : exists l, forall h : C, - f (c + h) = f c + h * l + (('o_ (0 : [filteredType C^o of C^o]) id) : _ --> numFieldType_normedModType (complex_numFieldType R) (*IMP*)) h. - admit. -(*This should be a lemma *) -move: (der c 1%:C ); simpl => /cvg_ex [lr /cvg_lim //= Dlr]. -move: (der c 'i); simpl => /cvg_ex [li /cvg_lim //= Dli]. -simpl in (type of lr); simpl in (type of Dlr). -simpl in (type of li); simpl in (type of Dli). -move : (CR c) ; rewrite /CauchyRiemanEq //= Dlr // Dli // => CRc. -pose l:= ((lr + lr*'i)) ; exists l; move => [a b]. -move: (der (c + a%:C) 'i); simpl => /cvg_ex [//= la /cvg_lim //= Dla]. -move: (der (c + a%:C) 'i) => /derivable_locallyxP. -have Htmp : ProperFilter ((fun h : R => h^-1 *: (f (h *: 'i%C + (c + a%:C)) - f (c + a%:C))) @ locally' (0:R^o)). - by apply fmap_proper_filter; apply Proper_locally'_numFieldType. -move: (Dla (@norm_hausdorff _ _) Htmp) => {}Dla. -rewrite /derive //= Dla => oR. -have -> : (a +i* b) = (a%:C + b*: 'i%C) by simpc. -rewrite addrA oR. -(*have fun a => la = cst(lr) + o_0(a). *) -move: (der c 1%:C); simpl => /derivable_locallyxP ; rewrite /derive //= Dlr => oC. -(* rewrite [a%:C]/(a *: 1%:C). *) -have -> : a%:C = (a *: 1%:C) by simpc. -rewrite oC. Print real_complex. -rewrite /type_of_filter /= in la Dla oR *. -have lem : ('o_ (0 : [filteredType R^o of R^o]) (@real_complex _ : _ -> numFieldType_normedModType (complex_numFieldType R) (*IMP*))) = - (fun a => (la - lr : C^o)). -move => s0. Check eqoE. -Fail suff : (fun _ : R => la - lr) = 'a_o_[filter of locally (0:R)] (real_complex R). -(* admit. -move => s1. - -apply: eqoE. (*eqoE and eqoP are not working*) apply: eqoE. apply: eqoE.*) - -(* (*another attempt*) *) -(* rewrite /holomorphic cvg_ex. *) -(* move: (der c 1%:C ); simpl => /cvg_ex [lr //= Dlr]. *) -(* move: (der c 'i); simpl => /cvg_ex [li //= Dli]. *) -(* simpl in (type of lr); simpl in (type of Dlr). *) -(* simpl in (type of li); simpl in (type of Dli). *) -(* move : (CR c) ; rewrite /CauchyRiemanEq //= (cvg_lim Dlr) (cvg_lim Dli) => CRc. *) -(* pose l:= ((lr + lr*'i)) ; exists l; move => A //= [r leq0r] normrA. *) -(* pose r':= r/(sqrtr 2). *) -(* have lrl : l / (1 + 'i*1) = lr. admit. *) -(* exists r ; first by []. *) -(* move => [a b] ballab abneq0 //=. *) -(* suff : normc (l- (a +i* b)^-1 *: ((f (a +i* b + c) - f c) : C^o)) <= r. *) -(* admit. *) -(* have : locally lr A. exists r'. *) -(* - by rewrite mulr_gt0 //= invr_gt0 sqrtr_gt0. *) -(* - move => t; rewrite /ball_ -lrl.admit. *) -(* (*we should have a tactic rewriting in any way that fits *) *) -(* move => /Dlr //=. *) -(* move : (Dli A) => //=. - *) -Admitted. - -Theorem CauchyRiemann (f : C^o -> C^o) c : (holomorphic f c) <-> - (forall v : C, derivable (complex_realfun f) c v) /\ (CauchyRiemanEq f c). -Proof. -Admitted. - -End Holomorphe.