wip

Author: mkerjean

theories/holomorphy.v

@@ -1,7 +1,7 @@
 
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 (*Require Import ssrsearch.*)
-From mathcomp Require Import ssreflect ssrfun ssrbool fieldext falgebra.
+From mathcomp Require Import ssreflect ssrfun ssrbool fieldext falgebra vector.
 From mathcomp Require Import ssrnat eqtype choice fintype bigop order ssralg ssrnum ssrfun.
 From mathcomp Require Import complex.
 From mathcomp Require Import boolp reals ereal derive.
@@ -277,8 +277,7 @@ apply/funext => P /=; rewrite propeqE; split.
 move => [B [] r r0] H /= H'; exists r%:C; first by rewrite ltcR.
 move => z h; apply: H' => /=; apply: H => /=.
 by rewrite -ltcR /=.
-
-Check  uniformityOfBallMixin.
+Admitted.
 
 Canonical Rcomplex_uniformType (R: realType) :=
   UniformType (Rcomplex R) (Rcomplex_uniformMixin R).
@@ -497,11 +496,55 @@ Qed.
 
 Lemma within_continuous_withinNx
   (R C : numFieldType) (U : normedModType C) (f : U -> R^o) :
-  {for (0 : U), continuous f} -> (f 0 = 0) -> f @ nbhs' (0 :U) --> nbhs'  (0 : R^o).
+  {for (0 : U), continuous f} -> (forall x,  f x = 0 -> x = 0) -> f @ nbhs' (0 :U) --> nbhs'  (0 : R^o).
 Proof.
-  move => cf f0 A /=.
-  rewrite !/nbhs /= /nbhs /= /nbhs' /within /= !nearE => [[]] r /= r0 H.
-  move : (cf A) => /=. near_simpl. rewrite f0. Admitted.
+  move => cf f0 A /=. 
+  rewrite !/nbhs /= /nbhs /= /nbhs' /within /= !nearE =>  H.  Admitted.
+
+Section complex_topological. (*WIP*)
+Variable R : realType.
+Local Notation C := R[i].
+
+Canonical complex_pointedType :=
+  [pointedType of C for pointed_of_zmodule [zmodType of C]].
+Canonical complex_filteredType :=
+  [filteredType C of C for filtered_of_normedZmod  [normedZmodType C of C]].
+Canonical complex_topologicalType  :=
+  TopologicalType C
+  (topologyOfEntourageMixin
+    (uniformityOfBallMixin
+      (@nbhs_ball_normE _ [normedZmodType C of C])
+      (pseudoMetric_of_normedDomain [normedZmodType C of C]))).
+Canonical numFieldType_uniformType := UniformType C
+  (uniformityOfBallMixin (@nbhs_ball_normE _ [normedZmodType C of C])
+    (pseudoMetric_of_normedDomain [normedZmodType C of C])).
+Canonical numFieldType_pseudoMetricTyp
+  := @PseudoMetric.Pack [numDomainType of C] C (@PseudoMetric.Class [numDomainType of C] C
+       (Uniform.class [uniformType of C])
+   (@pseudoMetric_of_normedDomain [numDomainType of C] [normedZmodType C of C])).
+
+Canonical complex_lmodType  :=
+  [lmodType R[i] of R[i] for [lmodType R[i] of R[i]^o]].
+
+Canonical complex_lalgType := [lalgType C of C for [lalgType C of C^o]].
+Canonical complex_algType := [algType C of C for [algType C of C^o]].
+Canonical complex_comAlgType := [comAlgType C of C].
+Canonical complex_unitAlgType := [unitAlgType C of C].
+Canonical complex_comUnitAlgType := [comUnitAlgType C of C]. 
+(* Canonical complex_vectType := [vectType C of C for [vectType C of C^o]]. *)
+(* Canonical complex_FalgType := [FalgType C of C]. *)
+(* Canonical complex_fieldExtType := *)
+(*   [fieldExtType C of C for [fieldExtType C of C^o]]. *)
+
+
+
+Canonical complex_pseudoMetricNormedZmodType :=
+  [pseudoMetricNormedZmodType C of C for
+  [pseudoMetricNormedZmodType C of [numFieldType of C^o]]].
+Canonical complex_normedModType :=
+  [normedModType C of C for [normedModType C of C^o]].
+
+End complex_topological.   
 
 Section Holomorphe_der.
 Variable R : realType.
@@ -538,24 +581,24 @@ so the following line shouldn't type check. *)
 Fail Definition Rderivable_fromcomplex_false (f : C^o -> C^o) (c v: C^o) :=
   cvg (fun (h : R^o) =>  h^-1 *: (f (c +h *: v) - f c)) @ (nbhs' (0:R^o)).
 
-Definition realC : R^o -> C^o := (fun r => r%:C).
+Definition realC : R^o -> C := (fun r => r%:C).
 
 Lemma continuous_realC: continuous realC.
 Proof.
 move => x A /= [] r /[dup] /realC_gt0 Rer0 /gt0_realC rRe H; exists (Re r); first by [].
 by move => z /= nz; apply: (H (realC z)); rewrite /= -realCB realC_norm rRe ltcR.
 Qed.
 
-Lemma Rdiff1 (f : C^o -> C^o) c :
-          lim ( (fun h : C^o =>  h^-1 *: ((f (c + h) - f c) ) )
+Lemma Rdiff1 (f : C -> C) c :
+          lim ( (fun h : C =>  h^-1 *: ((f (c + h) - f c) ) )
                  @ (realC @  (nbhs' 0)))
          = 'D_1 (f%:Rfun) c%:Rc :> C.
 Proof.
 rewrite /derive.
 have -> : (fun h : C^o =>  h^-1 *: ((f (c + h) - f c))) @ (realC @  (nbhs' 0)) =
          (fun h : C^o =>  h^-1 *: ((f (c + h) - f c)))
                  \o realC @  (nbhs' (0 : R^o)) by [].
-suff -> : ( (fun h : (R[i])^o => h^-1 *: (f (c + h) - f c)) \o realC)
+suff -> : ( (fun h : C => h^-1 *: (f (c + h) - f c)) \o realC)
 = (fun h : R^o => h^-1 *: ((f%:Rfun \o shift c) (h *: (1%:Rc)) - f c) ) :> (R -> C) . 
    by [].
 apply: funext => h /=.
@@ -574,59 +617,58 @@ have -> :
   = ((fun h : (R[i])^o => h^-1 *: (f (c + h * 'i) - f c)) \o realC) @ nbhs' 0 by [].
 suff -> :  (fun h : (R[i])^o => h^-1 * (f (c + h * 'i) - f c)) \o
 realC  = fun h : R => h^-1 *: ((f%:Rfun \o shift c) (h *: ('i%:Rc)) - f c).
-  by []. 
+  by [].
 apply: funext => h /=.
 by rewrite Inv_realC -scalecM -!scalecr realCZ [X in f X]addrC.
 Qed.
 
 
 (*extremely long with modified filteredType *)
 
-Definition CauchyRiemannEq (f : C^o -> C^o) c :=
+Definition CauchyRiemannEq (f : C -> C) c :=
   'i *'D_1 f%:Rfun c%:Rc =  'D_('i) f%:Rfun c%:Rc.
 
-Lemma holo_differentiable (f : C^o -> C^o) (c : C^o) :
+Lemma holo_differentiable (f : C -> C) (c : C) :
   holomorphic f c -> Rdifferentiable f c.
 Proof.
 move=> /holomorphicP /derivable1_diffP /diff_locallyP => [[diffc /=  /eqaddoP holo]].
 apply/diff_locallyP.
-pose Df : Rc -> Rc := fun (v : Rc) =>  ('d f (c: [topologicalType of C^o]) v).
+pose Df : Rc -> Rc := fun (v : Rc) =>  ('d f c v).
 have linDf : linear Df.
   move => t u v; rewrite /Df scalecr.
-  by rewrite (linearP ('d f (c: [topologicalType of C^o]))) scalecr /=.
+  by rewrite (linearP ('d f c)) scalecr /=.
 pose df : {linear Rc -> Rc} := (Linear linDf).
 have cdf : continuous (df : Rc -> Rc) by [].
 have eqdf : f%:Rfun \o +%R^~ c = cst (f c) + df +o_ (0 : Rc) id.
-  (* apply/eqaddoE; rewrite holo; congr (_ + _ + _) ; admit.*)
-  apply/eqaddoP => r /ltc0P r0; near=> x; rewrite -lecR -realCM /=; near: x.
+  (*apply/eqaddoE; rewrite holo; congr (_ + _ + _) ; admit.*)
+  apply/eqaddoP => r /ltc0P r0. near=> x; rewrite -lecR -realCM /=; near: x.
   by apply: holo.
-suff -> : ('d (f%:Rfun) (c : Rcomplex_normedModType R)) = df :> (_ -> _) by split.
+suff -> : ('d (f%:Rfun) (c : Rc) ) = df :> (_ -> _) by split. (*issue with notations*)
 by apply: diff_unique.
 Grab Existential Variables. by end_near. Qed.
 
-(*The fact that the topological structure is only available on C^o
-makes iterations of C^o apply *)
 
 (*The equality between 'i as imaginaryC from ssrnum and 'i is not transparent:
  neq0ci is part of ssrnum and uneasy to find *)
 
-Lemma holo_CauchyRiemann (f : C^o -> C^o) c: holomorphic f c -> CauchyRiemannEq f c.
+Lemma holo_CauchyRiemann (f : C -> C ) c: holomorphic f c -> CauchyRiemannEq f c.
 Proof.
 move=> /cvg_ex; rewrite //= /CauchyRiemannEq. rewrite -Rdiff1 -Rdiffi.
-set quotC : C^o -> C^o := fun h : R[i] => h^-1 *: (f (c + h) - f c).
-set quotR : C^o -> C^o:= fun h => h^-1 *: (f (c + h * 'i) - f c) .
+set quotC : C -> C := fun h : R[i] => h^-1 *: (f (c + h) - f c).
+set quotR : C -> C:= fun h => h^-1 *: (f (c + h * 'i) - f c) .
 move => /= [l H].
 have -> :  quotR @ (realC @ nbhs' 0) =  (quotR \o realC) @ nbhs' 0 by [].
 have realC'0:  realC @ nbhs' 0 --> nbhs' 0.
- by apply: within_continuous_withinNx; first by apply: continuous_realC.
- (* by move => /= x /complexI. *)
+ apply: within_continuous_withinNx; first by apply: continuous_realC.
+ by move => /= x /complexI.
 have HR0:(quotC \o (realC) @ nbhs' 0)  --> l.
  by apply: cvg_comp; last by exact: H.
 have lem : quotC \o  *%R^~ 'i%R @ (realC @ (nbhs' (0 : R^o))) --> l.
   apply: cvg_comp; last by exact: H.
   rewrite (filter_compE _ realC); apply: cvg_comp; first by exact: realC'0.
   apply: within_continuous_withinNx; first by apply: scalel_continuous.
-  by rewrite mul0r.
+  move => x /eqP; rewrite mulIr_eq0 ; last by apply/rregP; apply: neq0Ci.
+  by move/eqP.
 have HRcomp:  cvg (quotC \o *%R^~ 'i%R @ (realC @ (nbhs' (0 : R^o)))) .
   by apply/cvg_ex;  simpl; exists l.
 have ->: lim (quotR @ (realC @ (nbhs' (0 : R^o))))
@@ -640,7 +682,7 @@ suff: lim (quotC @ (realC @ (nbhs' (0 : R^o))))
       = lim (quotC \o  *%R^~ 'i%R @ (realC @ (nbhs' (0 : R^o)))) by move => -> .
 suff -> : lim (quotC @ (realC @ (nbhs' (0 : R^o)))) = l.
   by apply/eqP; rewrite eq_sym; apply/eqP; apply: (cvg_map_lim _ lem).
-by apply: (@cvg_map_lim [topologicalType of C^o]).
+by apply: cvg_map_lim. 
 Qed.
 
 
@@ -682,27 +724,36 @@ Qed.
 
 
 
-Lemma Diff_CR_holo (f : C^o -> C^o)  (c: C):
+Lemma Diff_CR_holo (f : C -> C)  (c: C):
+   (Rdifferentiable f c) /\
+  (CauchyRiemannEq f c)
+  -> (holomorphic f c).
+Proof.
+move => [] /= /[dup] H /diff_locallyP  => [[derc /eqaddoP diff]] CR.
+apply/holomorphicP/derivable1_diffP/diff_locallyP.
+pose Df := (fun h : C => h *: ('D_1 f%:Rfun c : C)).
+have lDf : linear Df.  move =>  t u v /=; rewrite /Df. admit.
+pose df := Linear lDf.
+have cdf : continuous df by apply: scalel_continuous.
+have lem : Df = 'd (f%:Rfun) (c : Rc). 
+  apply: funext => h; rewrite  /Df /= deriveE. admit.  admit. 
+have holo:  f \o  shift c = cst (f c) + df +o_ ( 0 : C) id.  
+  apply/eqaddoP => eps /[dup] /gt0_realC epsr /realC_gt0 eps0; near=> x.
+  rewrite epsr realCM lecR /=.  admit.
+have -> :   'd f c = df:> ( _ -> _) by  apply: diff_unique.
+by split.
+Grab Existential Variables.
+  (*by end_near. Qed. *)
+Admitted.
+
+Lemma Diff_CR_holo' (f : C -> C)  (c: C):
    (Rdifferentiable f c) /\
   (CauchyRiemannEq f c)
   -> (holomorphic f c).
 Proof.
-(* move => [] /= /[dup] H /diff_locallyP (*/eqaddoP*) => [[derc /eqaddoP diff]] CR. *)
-(* TODO : diff_locally to be renamed diff_nbhs *)
-(* apply/holomorphicP/derivable1_diffP/diff_locallyP;split.  *)
-(* pose Df : C^o -> C^o := (fun h => h *: ('D_1 f%:Rfun c : C^o)). *)
-(* have lDf : linear Df. admit. *)
-(* pose df := Linear lDf. *)
-(* have cdf : continuous df. admit. *)
-(* have holo:  f \o  shift c = cst (f c) + df +o_ (0 : [normedModType C of C^o]) id. *)
-(* apply/eqaddoP => eps /[dup] /gt0_realC epsr /realC_gt0 eps0; near=> x. *)
-(* rewrite epsr realCM lecR /=. *)
-(* Fail Check ('d f%:Rfun (c : [normedModType R of (Rcomplex R)])).  *)
-
-
 move => [] /= /[dup] H /diff_locally /eqaddoP => der CR.
-rewrite /holomorphic; apply: (cvgP (('D_1 f%:Rfun c) : C^o)).
-apply/(cvg_distP (('D_1 f%:Rfun c) : C^o)).
+rewrite /holomorphic; apply: (cvgP (('D_1 f%:Rfun c) : C)).
+apply/(cvg_distP (('D_1 f%:Rfun c) : C)).
 move => eps eps_lt0 /=.
 pose er := Re eps.
 have eq_ereps := gt0_realC eps_lt0.
@@ -730,19 +781,19 @@ rewrite -CR (scalecAl y) (* why scalec *) -scalecM !scalecr.
 rewrite -(scalerDl  (('D_1 f%:Rfun c%:Rc): C^o) x%:C). (*clean, do it in Rcomplex *)
 rewrite addrAC -!scalecr -realC_alg -zeq. (*clean*)
 rewrite addrC  [X in (-_ + X)]addrC [X in f X]addrC -[X in `|_ + X|]opprK -opprD.
-rewrite normrN scalecM -lecR => H.
-rewrite /normr /=; apply: le_lt_trans; first by exact H.
+rewrite normrN scalecM -lecR => H'.
+rewrite /normr /=; apply: le_lt_trans; first by exact H'.
 rewrite eq_ereps realCM ltcR /normr /= ltr_pmul2l ?normc_gt0 //.
 rewrite /er -[X in (_ < X)]mulr1 ltr_pmul2l //= ?invf_lt1 ?ltr1n //.
 rewrite -ltc0E -eq_ereps //.
 Qed.
 
 
 
-Lemma holomorphic_Rdiff (f : C^o -> C^o) (c : C) :
+Lemma holomorphic_Rdiff (f : C -> C) (c : C) :
   (Rdifferentiable f c) /\ (CauchyRiemannEq f c) <-> (holomorphic f c).
 Proof.
-  split => H; first by apply: Diff_CR_holo.
+  split => H; first by apply: Diff_CR_holo'.
   split; first by apply: holo_differentiable.
   by apply: holo_CauchyRiemann.
 Qed.