make normedtype.v depend on evt.v

affeldt-aist · affeldt-aist · commit 198726dd57dd · 2024-09-06T00:40:40.000+09:00
diff --git a/_CoqProject b/_CoqProject
@@ -28,6 +28,7 @@ theories/topology.v
 theories/function_spaces.v
 theories/cantor.v
 theories/prodnormedzmodule.v
+theories/evt.v
 theories/normedtype.v
 theories/realfun.v
 theories/sequences.v
diff --git a/theories/Make b/theories/Make
@@ -16,6 +16,7 @@ topology.v
 function_spaces.v
 cantor.v
 prodnormedzmodule.v
+evt.v
 normedtype.v
 realfun.v
 sequences.v
diff --git a/theories/derive.v b/theories/derive.v
@@ -233,13 +233,13 @@ Qed.
 End diff_locally_converse_tentative.
 
 Definition derive (f : V -> W) a v :=
-  lim ((fun h => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ 0^').
+  lim ((fun h => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ (0:R)^').
 
 Local Notation "''D_' v f" := (derive f ^~ v).
 Local Notation "''D_' v f c" := (derive f c v). (* printing *)
 
 Definition derivable (f : V -> W) a v :=
-  cvg ((fun h => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ 0^').
+  cvg ((fun h => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ (0:R)^').
 
 Class is_derive (a v : V) (f : V -> W) (df : W) := DeriveDef {
   ex_derive : derivable f a v;
@@ -356,7 +356,7 @@ Lemma derivemxE m n (f : 'rV[R]_m.+1 -> 'rV[R]_n.+1) (a v : 'rV[R]_m.+1) :
 Proof. by move=> /deriveE->; rewrite /jacobian mul_rV_lin1. Qed.
 
 Definition derive1 V (f : R -> V) (a : R) :=
-   lim ((fun h => h^-1 *: (f (h + a) - f a)) @ 0^').
+   lim ((fun h => h^-1 *: (f (h + a) - f a)) @ (0:R)^').
 
 Local Notation "f ^` ()" := (derive1 f).
 
@@ -1125,7 +1125,7 @@ Implicit Types f g : V -> W.
 
 Fact der_add f g (x v : V) : derivable f x v -> derivable g x v ->
   (fun h => h^-1 *: (((f + g) \o shift x) (h *: v) - (f + g) x)) @
-  0^'  --> 'D_v f x + 'D_v g x.
+  (0:R)^'  --> 'D_v f x + 'D_v g x.
 Proof.
 move=> df dg.
 evar (fg : R -> W); rewrite [X in X @ _](_ : _ = fg) /=; last first.
@@ -1177,7 +1177,7 @@ Qed.
 
 Fact der_opp f (x v : V) : derivable f x v ->
   (fun h => h^-1 *: (((- f) \o shift x) (h *: v) - (- f) x)) @
-  0^' --> - 'D_v f x.
+  (0:R)^' --> - 'D_v f x.
 Proof.
 move=> df; evar (g : R -> W); rewrite [X in X @ _](_ : _ = g) /=; last first.
   by rewrite funeqE => h; rewrite !scalerDr !scalerN -opprD -scalerBr /g.
diff --git a/theories/evt.v b/theories/evt.v
@@ -18,12 +18,24 @@ Local Open Scope ring_scope.
 
 HB.structure Definition PointedNmodule := {M of Pointed M & GRing.Nmodule M}.
 HB.structure Definition PointedZmodule := {M of Pointed M & GRing.Zmodule M}.
+HB.structure Definition PointedLmodule (K : numDomainType) :=
+  {M of Pointed M & GRing.Lmodule K M}.
 HB.structure Definition FilteredNmodule := {M of Filtered M M & GRing.Nmodule M}.
 HB.structure Definition FilteredZmodule := {M of Filtered M M & GRing.Zmodule M}.
+HB.structure Definition FilteredLmodule (K : numDomainType) :=
+  {M of Filtered M M & GRing.Lmodule K M}.
 HB.structure Definition NbhsNmodule := {M of Nbhs M & GRing.Nmodule M}.
 HB.structure Definition NbhsZmodule := {M of Nbhs M & GRing.Zmodule M}.
+HB.structure Definition NbhsLmodule (K : numDomainType) :=
+  {M of Nbhs M & GRing.Lmodule K M}.
 HB.structure Definition TopologicalNmodule := {M of Topological M & GRing.Nmodule M}.
-HB.structure Definition TopologicalZmodule := {M of Uniform M & GRing.Zmodule M}.
+HB.structure Definition TopologicalZmodule :=
+  {M of Topological M & GRing.Zmodule M}.
+HB.structure Definition TopologicalLmodule (K : numDomainType) :=
+  {M of Topological M & GRing.Lmodule K M}.
+HB.structure Definition UniformZmodule := {M of Uniform M & GRing.Zmodule M}.
+HB.structure Definition UniformLmodule (K : numDomainType) :=
+  {M of Uniform M & GRing.Lmodule K M}.
 
 Definition convex (R : ringType) (M : lmodType R) (A : set M) :=
   forall x y lambda, lambda *: x + (1 - lambda) *: y \in A.
diff --git a/theories/exp.v b/theories/exp.v
@@ -198,18 +198,18 @@ Lemma pseries_snd_diffs (c : R^nat) K x :
 Proof.
 move=> Ck CdK CddK xLK; rewrite /pseries.
 set s := (fun n : nat => _); set (f := fun x0 => _).
-suff hfxs : h^-1 *: (f (h + x) - f x) @[h --> 0^'] --> limn (series s).
+suff hfxs : h^-1 *: (f (h + x) - f x) @[h --> (0:R)^'] --> limn (series s).
   have F : f^`() x = limn (series s) by apply: cvg_lim hfxs.
   have Df : derivable f x 1.
-    move: hfxs; rewrite /derivable [X in X @ 0^'](_ : _ =
+    move: hfxs; rewrite /derivable [X in X @ (0:R)^'](_ : _ =
         (fun h => h^-1 *: (f (h%:A + x) - f x))) /=; last first.
       by apply/funext => i //=; rewrite [i%:A]mulr1.
     by move=> /(cvg_lim _) -> //.
   by constructor; [exact: Df|rewrite -derive1E].
 pose sx := fun n : nat => c n * x ^+ n.
 have Csx : cvgn (pseries c x) by apply: is_cvg_pseries_inside Ck _.
 pose shx := fun h (n : nat) => c n * (h + x) ^+ n.
-suff Cc : limn (h^-1 *: (series (shx h - sx))) @[h --> 0^'] --> limn (series s).
+suff Cc : limn (h^-1 *: (series (shx h - sx))) @[h --> (0:R)^'] --> limn (series s).
   apply: cvg_sub0 Cc.
   apply/cvgrPdist_lt => eps eps_gt0 /=.
   near=> h; rewrite sub0r normrN /=.
@@ -229,7 +229,7 @@ suff Cc : limn (h^-1 *: (series (shx h - sx))) @[h --> 0^'] --> limn (series s).
 apply: cvg_zero => /=.
 suff Cc : limn
     (series (fun n => c n * (((h + x) ^+ n - x ^+ n) / h - n%:R * x ^+ n.-1)))
-    @[h --> 0^'] --> (0 : R).
+    @[h --> (0:R)^'] --> (0 : R).
   apply: cvg_sub0 Cc.
   apply/cvgrPdist_lt => eps eps_gt0 /=.
   near=> h; rewrite sub0r normrN /=.
diff --git a/theories/ftc.v b/theories/ftc.v
@@ -38,7 +38,7 @@ Implicit Types (f : R -> R) (a : itv_bound R).
 Let FTC0 f a : mu.-integrable setT (EFin \o f) ->
   let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) f t)%R in
   forall x, a < BRight x -> lebesgue_pt f x ->
-    h^-1 *: (F (h + x) - F x) @[h --> 0%R^'] --> f x.
+    h^-1 *: (F (h + x) - F x) @[h --> (0:R)%R^'] --> f x.
 Proof.
 move=> intf F x ax fx.
 have locf : locally_integrable setT f.
@@ -294,7 +294,7 @@ Unshelve. all: by end_near. Qed.
 
 Lemma parameterized_integral_cvg_left a b (f : R -> R) : a < b ->
   mu.-integrable `[a, b] (EFin \o f) ->
-  int a x f @[x --> a] --> 0.
+  int a x f @[x --> a] --> (0:R).
 Proof.
 move=> ab intf; pose fab := f \_ `[a, b].
 have intfab : mu.-integrable `[a, b] (EFin \o fab).
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
@@ -6149,7 +6149,7 @@ Hypotheses (xU : open_nbhs x U) (mU : measurable U) (mUf : measurable_fun U f)
            (fx : {for x, continuous f}).
 
 Let continuous_integralB_fin_num :
-  \forall t \near 0%R,
+  \forall t \near (0:R)%R,
     \int[mu]_(y in ball x t) `|(f y)%:E - (f x)%:E| \is a fin_num.
 Proof.
 move: fx => /cvgrPdist_le /= fx'.
@@ -6172,7 +6172,7 @@ apply: ge0_le_integral => //=; first exact: measurable_ball.
 Unshelve. all: by end_near. Qed.
 
 Let continuous_davg_fin_num :
-  \forall A \near 0%R, davg f x A \is a fin_num.
+  \forall A \near (0:R)%R, davg f x A \is a fin_num.
 Proof.
 have [e /= e0 exf] := continuous_integralB_fin_num.
 move: fx => /cvgrPdist_le fx'.
@@ -6183,7 +6183,7 @@ near=> t; have [t0|t0] := leP t 0%R; first by rewrite davg0.
 by rewrite fin_numM// exf/=.
 Unshelve. all: by end_near. Qed.
 
-Lemma continuous_cvg_davg : davg f x r @[r --> 0%R] --> 0.
+Lemma continuous_cvg_davg : davg f x r @[r --> (0:R)%R] --> 0.
 Proof.
 apply/fine_cvgP; split; first exact: continuous_davg_fin_num.
 apply/cvgrPdist_le => e e0.
@@ -6795,7 +6795,7 @@ Local Notation mu := lebesgue_measure.
 Definition nicely_shrinking x E :=
   (forall n, measurable (E n)) /\
   exists Cr : R * {posnum R}^nat, [/\ Cr.1 > 0,
-    (Cr.2 n)%:num @[n --> \oo] --> 0,
+    (Cr.2 n)%:num @[n --> \oo] --> (0:R),
     (forall n, E n `<=` ball x (Cr.2 n)%:num) &
     (forall n, mu (ball x (Cr.2 n)%:num) <= Cr.1%:E * mu (E n))%E].
 
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
@@ -1816,7 +1816,7 @@ rewrite (_ : [set~ 0] = `]-oo, 0[ `|` `]0, +oo[); last first.
     rewrite in_itv/= -eq_le eq_sym; [move/eqP/negbTE => ->|move/negP/eqP].
 apply/measurable_funU => //; split.
 - apply/measurable_restrictT => //=.
-  rewrite (_ : _ \_ _ = cst 0)//; apply/funext => y; rewrite patchE.
+  rewrite (_ : _ \_ _ = cst (0:R))//; apply/funext => y; rewrite patchE.
   by case: ifPn => //; rewrite inE/= in_itv/= => y0; rewrite ln0// ltW.
 - have : {in `]0, +oo[%classic, continuous (@ln R)}.
     by move=> x; rewrite inE/= in_itv/= andbT => x0; exact: continuous_ln.
diff --git a/theories/normedtype.v b/theories/normedtype.v
@@ -6,6 +6,7 @@ From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import archimedean.
 From mathcomp Require Import cardinality set_interval Rstruct.
 Require Import ereal reals signed topology prodnormedzmodule function_spaces.
+Require Import evt.
 
 (**md**************************************************************************)
 (* # Norm-related Notions                                                     *)
diff --git a/theories/realfun.v b/theories/realfun.v
@@ -1511,7 +1511,7 @@ Proof. exact: (@exprn_continuous 2%N). Qed.
 Lemma sqrt_continuous : continuous (@Num.sqrt R).
 Proof.
 move=> x; case: (ltrgtP x 0) => [xlt0 | xgt0 | ->].
-- apply: (near_cst_continuous 0).
+- apply: (near_cst_continuous (0:R)).
   by near do rewrite ltr0_sqrtr//; apply: (cvgr_lt x).
   pose I b : set R := [set` `]0 ^+ 2, b ^+ 2[].
   suff main b : 0 <= b -> {in I b, continuous (@Num.sqrt R)}.
@@ -1545,18 +1545,18 @@ split => [Hd|[g [fxE Cg gxE]]].
     by rewrite -subr_eq0 => /divfK->.
   - apply/continuous_withinNshiftx; rewrite eqxx /=.
     pose g1 h := (h^-1 *: ((f \o shift x) h%:A - f x)).
-    have F1 : g1 @ 0^' --> a by case: Hd => H1 <-.
+    have F1 : g1 @ (0:R)^' --> a by case: Hd => H1 <-.
     apply: cvg_trans F1; apply: near_eq_cvg; rewrite /g1 !fctE.
     near=> i.
     rewrite ifN; first by rewrite addrK mulrC /= [_%:A]mulr1.
     rewrite -subr_eq0 addrK.
     by near: i; rewrite near_withinE /= near_simpl; near=> x1.
   by rewrite eqxx.
-suff Hf : h^-1 *: ((f \o shift x) h%:A - f x) @[h --> 0^'] --> a.
+suff Hf : h^-1 *: ((f \o shift x) h%:A - f x) @[h --> (0:R)^'] --> a.
   have F1 : 'D_1 f x = a by apply: cvg_lim.
   rewrite -F1 in Hf.
     by constructor.
-  have F1 :  (g \o shift x) y @[y --> 0^'] --> a.
+  have F1 :  (g \o shift x) y @[y --> (0:R)^'] --> a.
   by rewrite -gxE; apply/continuous_withinNshiftx.
 apply: cvg_trans F1; apply: near_eq_cvg.
 near=> y.
diff --git a/theories/sequences.v b/theories/sequences.v
@@ -566,14 +566,14 @@ Notation nonincreasing_cvg_ge := nonincreasing_cvgn_ge (only parsing).
 Notation nondecreasing_cvg_le := nondecreasing_cvgn_le (only parsing).
 
 Lemma __deprecated__invr_cvg0 (R : realFieldType) (u : R^nat) :
-  (forall i, 0 < u i) -> ((u i)^-1 @[i --> \oo] --> 0) <-> (u @ \oo --> +oo).
+  (forall i, 0 < u i) -> ((u i)^-1 @[i --> \oo] --> (0:R)) <-> (u @ \oo --> +oo).
 Proof. by move=> ?; rewrite gtr0_cvgV0//; apply: nearW. Qed.
 #[deprecated(since="mathcomp-analysis 0.6.0",
   note="renamed to `gtr0_cvgV0` and generalized")]
 Notation invr_cvg0 := __deprecated__invr_cvg0 (only parsing).
 
 Lemma __deprecated__invr_cvg_pinfty (R : realFieldType) (u : R^nat) :
-  (forall i, 0 < u i) -> ((u i)^-1 @[i --> \oo] --> +oo) <-> (u @ \oo--> 0).
+  (forall i, 0 < u i) -> ((u i)^-1 @[i --> \oo] --> +oo) <-> (u @ \oo--> (0:R)).
 Proof. by move=> ?; rewrite cvgrVy//; apply: nearW. Qed.
 #[deprecated(since="mathcomp-analysis 0.6.0",
   note="renamed to `cvgrVy` and generalized")]
@@ -817,7 +817,7 @@ Proof. by rewrite /=. Qed.
 Lemma harmonic_ge0 {R : numFieldType} i : 0 <= harmonic i :> R.
 Proof. exact/ltW/harmonic_gt0. Qed.
 
-Lemma cvg_harmonic {R : archiFieldType} : @harmonic R @ \oo --> 0.
+Lemma cvg_harmonic {R : archiFieldType} : @harmonic R @ \oo --> (0:R).
 Proof.
 apply/cvgrPdist_le => _/posnumP[e]; near=> i.
 rewrite distrC subr0 ger0_norm//= -lef_pV2 ?qualifE//= invrK.
@@ -1156,7 +1156,7 @@ Qed.
 
 Lemma cvg_to_0_linear (R : realFieldType) (f : R -> R) K (k : R) :
   0 < k -> (forall r, 0 < `| r | < k -> `|f r| <= K * `| r |) ->
-    f x @[x --> 0^'] --> 0.
+    f x @[x --> (0:R)^'] --> (0:R).
 Proof.
 move=> k0 kfK; have [K0|K0] := lerP K 0.
 - apply/cvgrPdist_lt => _/posnumP[e]; near=> x.
@@ -1165,7 +1165,7 @@ move=> k0 kfK; have [K0|K0] := lerP K 0.
   near: x; exists (k / 2); first by rewrite /mkset divr_gt0.
   move=> t /=; rewrite distrC subr0 => tk2 t0.
   by rewrite normr_gt0 t0 (lt_trans tk2) // -[in ltLHS](add0r k) midf_lt.
-- apply/(@eqolim0 _ _ R (0^'))/eqoP => _/posnumP[e]; near=> x.
+- apply/(@eqolim0 _ _ R (0:R)^')/eqoP => _/posnumP[e]; near=> x.
   rewrite (le_trans (kfK _ _)) //=.
   + near: x; exists (k / 2); first by rewrite /mkset divr_gt0.
     move=> t /=; rewrite distrC subr0 => tk2 t0.
@@ -1178,7 +1178,7 @@ Unshelve. all: by end_near. Qed.
 Lemma lim_cvg_to_0_linear (R : realType) (f : nat -> R) (g : R -> nat -> R) k :
   0 < k -> cvgn (series f) ->
   (forall r, 0 < `|r| < k -> forall n, `|g r n| <= f n * `| r |) ->
-  limn (series (g x)) @[x --> 0^'] --> 0.
+  limn (series (g x)) @[x --> (0:R)^'] --> (0:R).
 Proof.
 move=> k_gt0 Cf Hg.
 apply: (@cvg_to_0_linear _ _ (limn (series f)) k) => // h hLk; rewrite mulrC.
@@ -2131,7 +2131,7 @@ Context {R : realFieldType}.
 Implicit Types (u : R^nat) (r : R).
 
 Lemma minr_cvg_0_cvg_0 u r : 0 < r -> (forall k, 0 <= u k) ->
-  minr (u n) r @[n --> \oo] --> 0 -> u n @[n --> \oo] --> 0.
+  minr (u n) r @[n --> \oo] --> (0:R) -> u n @[n --> \oo] --> (0:R).
 Proof.
 move=> r0 u0 minr_cvg; apply/cvgrPdist_lt => _ /posnumP[e].
 have : 0 < minr e%:num r by rewrite lt_min// r0 andbT.
@@ -2143,7 +2143,7 @@ by rewrite le_min u0 ltW.
 Unshelve. all: by end_near. Qed.
 
 Lemma maxr_cvg_0_cvg_0 u r : r < 0 -> (forall k, u k <= 0) ->
-  maxr (u n) r @[n --> \oo] --> 0 -> u n @[n --> \oo] --> 0.
+  maxr (u n) r @[n --> \oo] --> (0:R) -> u n @[n --> \oo] --> (0:R).
 Proof.
 rewrite -[in r < _]oppr0 ltrNr => r0 u0.
 under eq_fun do rewrite -(opprK (u _)) -[in maxr _ _](opprK r) -oppr_min.
@@ -2175,7 +2175,7 @@ Unshelve. all: by end_near. Qed.
 
 Lemma mine_cvg_minr_cvg u r : (0 < r)%R -> (forall k, 0 <= u k) ->
   mine (u n) r%:E @[n --> \oo] --> 0 ->
-  minr (fine (u n)) r @[n --> \oo] --> 0%R.
+  minr (fine (u n)) r @[n --> \oo] --> (0:R)%R.
 Proof.
 move=> r0 u0 mine_cvg; apply: (cvg_trans _ (fine_cvg mine_cvg)).
 move/fine_cvgP : mine_cvg => [_ /=] /cvgrPdist_lt.
@@ -2213,7 +2213,7 @@ Qed.
 
 Lemma maxe_cvg_maxr_cvg u r : (r < 0)%R -> (forall k, u k <= 0) ->
   maxe (u n) r%:E @[n --> \oo] --> 0 ->
-  maxr (fine (u n)) r @[n --> \oo] --> 0%R.
+  maxr (fine (u n)) r @[n --> \oo] --> (0:R)%R.
 Proof.
 rewrite -[in (r < _)%R]oppr0 ltrNr => r0 u0.
 under eq_fun do rewrite -(oppeK (u _)) -[in maxe _ _](oppeK r%:E) -oppe_min.
