wip and tried making factory from uniform to normedModType

Author: Tragicus

theories/holomorphy.v

@@ -23,6 +23,25 @@ I don't want the canonical lmodtype structure on C,
 Therefore this is based on a fork of real-closed *)
 HB.instance Definition _ (R : rcfType) := NormedModule.copy R[i] R[i]^o.
 
+HB.instance Definition _ (R : rcfType) := Uniform.copy (Rcomplex R) R[i].
+HB.instance Definition _ (R : rcfType) := Pointed.copy (Rcomplex R) R[i].
+
+Section Rcomplex_NormedModType.
+Variable (R : rcfType).
+HB.howto Rcomplex normedModType 11.
+
+Definition ball : R -> Rcomplex R -> R -> Prop
+    - ball_center_subproof : forall (x : M) (e : R), 0 < e -> ball x e x
+    - ball_sym_subproof : forall (x y : M) (e : R), ball x e y -> ball y e x
+    - ball_triangle_subproof :
+        forall (x y z : M) (e1 e2 : R),
+        ball x e1 y -> ball y e2 z -> ball x (e1 + e2)%E z
+    - entourageE_subproof : entourage = entourage_ ball
+
+HB.about Uniform_isPseudoMetric.Build.
+; NormedZmod_PseudoMetric_eq;
+      PseudoMetricNormedZmod_Lmodule_isNormedModule
+
 HB.factory Record Normed_And_Lmodule_isNormedModule (K : numFieldType) R of @Num.NormedZmodule K R & GRing.Lmodule K R := {
   normrZ : forall (l : K) (x : R), normr (l *: x) = normr l * normr x;
 }.
@@ -239,15 +258,15 @@ Lemma real_normc_ler (x y : R) :
 Proof.
 rewrite /normc /= -ler_sqr ?nnegrE ?normr_ge0 ?sqrtr_ge0 //.
 rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=.
-by rewrite ler_addl ?sqr_ge0.
+by rewrite lerDl ?sqr_ge0.
 Qed.
 
 Lemma im_normc_ler (x y : R) :
   `|y| <= normc (x +i* y).
 Proof.
 rewrite /normc /= -ler_sqr ?nnegrE ?normr_ge0 ?sqrtr_ge0 //.
 rewrite sqr_sqrtr ?addr_ge0 ?sqr_ge0 ?real_normK //=.
-by rewrite ler_addr ?sqr_ge0.
+by rewrite lerDr ?sqr_ge0.
 Qed.
 
 End complex_extras.
@@ -403,6 +422,14 @@ have -> : (fun h : C =>  h^-1 *: ((f (c + h) - f c))) @ (realC @  (dnbhs 0)) =
                  \o realC @  (dnbhs (0 : R)) by [].
 suff -> : ( (fun h : C => h^-1 *: (f (c + h) - f c)) \o realC)
 = (fun h : R => h^-1 *: ((f%:Rfun \o shift c) (h *: (1%:Rc)) - f c : Rcomplex _) ) :> (R -> C) .
+STOP.
+rewrite /=.
+f_equal => /=.
+Set Printing All.
+Search lim Logic.eq .
+Search (lim _ = lim _).
+Set Printing All.
+apply: lim_eq.
   admit.
 apply: funext => h /=.
 by  rewrite Inv_realC /= -!scalecr realC_alg [X in f X]addrC.

theories/normedtype_theory/normed_module.v

@@ -2061,3 +2061,53 @@ HB.instance Definition _ :=
 Check M : normedModType R.
 
 HB.end.
+
+HB.factory Record Uniform_Lmodule_isNormed (R : numFieldType) M of Uniform M & GRing.Lmodule R M := {
+ norm : M -> R;
+ ler_normD : forall x y, norm (x + y) <= norm x + norm y ;
+ normrZ : forall (l : R) (x : M), norm (l *: x) = `|l| * norm x ;
+ normr0_eq0 : forall x : M, norm x = 0 -> x = 0 ;
+ entourage_norm : forall x : M, nbhs_ball_ (ball_ norm) x = filter.nbhs x;
+}.
+
+HB.builders Context R M of Uniform_Lmodule_isNormed R M.
+
+Lemma normrMn (x : M) (n : nat) : norm (x *+ n) = norm x *+ n.
+Proof.
+  admit.
+Admitted.
+
+
+Lemma normrN (x : M) : norm (- x) = norm x.
+Proof. admit. Admitted.
+
+HB.instance Definition _ := Num.Zmodule_isNormed.Build R M ler_normD normr0_eq0 normrMn normrN.
+HB.instance Definition _ := isPointed.Build M 0.
+
+Definition ball := ball_ (fun x : M => `|x|).
+
+Lemma ball_center_subproof (x : M) (e : R) : 0 < e -> ball x e x.
+Proof. by rewrite /ball /ball_/= subrr normr0. Qed.
+
+Lemma ball_sym_subproof (x y : M) (e : R) : ball x e y -> ball y e x.
+Proof. by rewrite /ball /ball_/= distrC. Qed.
+
+Lemma ball_triangle_subproof (x y z : M) (e1 e2 : R) :
+        ball x e1 y ->
+        ball y e2 z ->
+        ball x (e1 + e2)%E z.
+Proof.
+rewrite /ball /ball_/= => ? ?.
+rewrite -[x](subrK y) -(addrA (x + _)).
+by rewrite (le_lt_trans (ler_normD _ _))// ltrD.
+Qed.
+
+Lemma entourageE_subproof : entourage = entourage_ ball.
+Proof. admit. Admitted.
+
+HB.instance Definition _ := Uniform_isPseudoMetric.Build R M ball_center_subproof ball_sym_subproof ball_triangle_subproof entourageE_subproof.
+
+HB.about NormedZmod_PseudoMetric_eq.Build.
+; PseudoMetricNormedZmod_Lmodule_isNormedModule
+
+HB.howto M normedModType.