Topological vector spaces

_CoqProject

@@ -28,6 +28,7 @@ theories/topology.v
 theories/function_spaces.v
 theories/cantor.v
 theories/prodnormedzmodule.v
+theories/tvs.v
 theories/normedtype.v
 theories/realfun.v
 theories/sequences.v

theories/Make

@@ -16,6 +16,7 @@ topology.v
 function_spaces.v
 cantor.v
 prodnormedzmodule.v
+tvs.v
 normedtype.v
 realfun.v
 sequences.v

theories/charge.v

@@ -700,7 +700,7 @@ have nuAoo : 0 <= nu Aoo.
 have A_cvg_0 : nu (A_ (v n)) @[n --> \oo] --> 0.
   rewrite [X in X @ _ --> _](_ : _ = (fun n => (fine (nu (A_ (v n))))%:E)); last first.
     by apply/funext => n/=; rewrite fineK// fin_num_measure.
-  apply: continuous_cvg => //; apply: cvg_series_cvg_0.
+  apply: continuous_cvg => //; apply: (@cvg_series_cvg_0 _ R^o).
   rewrite (_ : series _ = fine \o (fun n => \sum_(0 <= i < n) nu (A_ (v i)))); last first.
     apply/funext => n /=.
     by rewrite /series/= sum_fine//= => i _; rewrite fin_num_measure.
@@ -831,7 +831,7 @@ have znuD n : z_ (v n) <= nu D.
 have max_le0 n : maxe (z_ (v n) * 2^-1%:E) (- 1%E) <= 0.
   by rewrite ge_max leeN10 andbT pmule_lle0.
 have not_s_cvg_0 : ~ (z_ \o v) n @[n --> \oo]  --> 0.
-  move/fine_cvgP => -[zfin] /cvgrPdist_lt.
+  move/fine_cvgP => -[zfin] /(@cvgrPdist_lt _ R^o).
   have /[swap] /[apply] -[M _ hM] : (0 < `|fine (nu D)|)%R.
     by rewrite normr_gt0// fine_eq0// ?lt_eqF// fin_num_measure.
   near \oo => n.
@@ -862,7 +862,7 @@ have : cvg (series (fun n => fine (maxe (z_ (v n) * 2^-1%:E) (- 1%E))) n @[n -->
   apply/funext => n/=; rewrite sum_fine// => m _.
   rewrite le0_fin_numE; first by rewrite lt_max ltNyr orbT.
   by rewrite /maxe; case: ifPn => // _; rewrite mule_le0_ge0.
-move/cvg_series_cvg_0 => maxe_cvg_0.
+move/(@cvg_series_cvg_0 _ R^o) => maxe_cvg_0.
 apply: not_s_cvg_0.
 rewrite (_ : _ \o _ = (fun n => z_ (v n) * 2^-1%:E) \* cst 2%:E); last first.
   by apply/funext => n/=; rewrite -muleA -EFinM mulVr ?mule1// unitfE.
@@ -874,7 +874,7 @@ apply/fine_cvgP; split.
   rewrite sub0r normrN ltNge => maxe_lt1; rewrite fin_numE; apply/andP; split.
     by apply: contra maxe_lt1 => /eqP ->; rewrite max_r ?leNye//= normrN1 lexx.
   by rewrite lt_eqF// (@le_lt_trans _ _ 0)// mule_le0_ge0.
-apply/cvgrPdist_lt => _ /posnumP[e].
+apply/(@cvgrPdist_lt _ R^o) => _ /posnumP[e].
 have : (0 < minr e%:num 1)%R by rewrite lt_min// ltr01 andbT.
 move/cvgrPdist_lt : maxe_cvg_0 => /[apply] -[M _ hM].
 near=> n; rewrite sub0r normrN.

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.

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 /=.

theories/ftc.v

@@ -36,9 +36,9 @@ Local Open Scope ereal_scope.
 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
+  let F x : R^o := (\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.
@@ -79,7 +79,7 @@ apply: cvg_at_right_left_dnbhs.
         by apply/negP; rewrite negb_and -!leNgt xz orbT.
       - by apply/negP; rewrite -leNgt.
   rewrite [f in f n @[n --> _] --> _](_ : _ =
-      fun n => (d n)^-1 *: fine (\int[mu]_(t in E x n) (f t)%:E)); last first.
+      fun n => (d n)^-1 *: (fine (\int[mu]_(t in E x n) (f t)%:E) : R^o)); last first.
     apply/funext => n; congr (_ *: _); rewrite -fineB/=.
     by rewrite /= (addrC (d n) x) ixdf.
     by apply: integral_fune_fin_num => //; exact: integrableS intf.
@@ -106,7 +106,7 @@ apply: cvg_at_right_left_dnbhs.
   have nice_E y : nicely_shrinking y (E y).
     split=> [n|]; first exact: measurable_itv.
     exists (2, (fun n => PosNum (Nd_gt0 n))); split => //=.
-      by rewrite -oppr0; exact: cvgN.
+      by rewrite -oppr0; exact: (@cvgN _ R^o).
     move=> n z.
       rewrite /E/= in_itv/= /ball/= => /andP[yz zy].
       by rewrite ltr_distlC opprK yz /= (le_lt_trans zy)// ltrDl.
@@ -141,7 +141,7 @@ apply: cvg_at_right_left_dnbhs.
         rewrite /E /= !in_itv/= leNgt => xdnz.
         by apply/negP; rewrite negb_and xdnz.
     move=> b a ax.
-    move/cvgrPdist_le : d0.
+    move/(@cvgrPdist_le _ R^o) : d0.
     move/(_ (x - a)%R); rewrite subr_gt0 => /(_ ax)[m _ /=] h.
     near=> n.
     have mn : (m <= n)%N by near: n; exists m.
@@ -170,7 +170,7 @@ apply: cvg_at_right_left_dnbhs.
       by apply/negP; rewrite negb_and -leNgt zxdn.
   suff: ((d n)^-1 * - fine (\int[mu]_(y in E x n) (f y)%:E))%R
           @[n --> \oo] --> f x.
-    apply: cvg_trans; apply: near_eq_cvg; near=> n;  congr (_ *: _).
+    apply: cvg_trans; apply: near_eq_cvg; near=> n;  congr (_ *: (_ : R^o)).
     rewrite /F -fineN -fineB; last 2 first.
       by apply: integral_fune_fin_num => //; exact: integrableS intf.
       by apply: integral_fune_fin_num => //; exact: integrableS intf.
@@ -188,9 +188,9 @@ Unshelve. all: by end_near. Qed.
 
 (* NB: right-closed interval *)
 Lemma FTC1_lebesgue_pt f a : mu.-integrable setT (EFin \o f) ->
-  let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in
+  let F x : R^o := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in
   forall x, a < BRight x -> lebesgue_pt f x ->
-  derivable F x 1 /\ F^`() x = f x.
+  derivable (F : R^o -> R^o) x 1 /\ F^`() x = f x.
 Proof.
 move=> intf F x ax fx; split; last first.
   by apply/cvg_lim; [exact: Rhausdorff|exact: FTC0].
@@ -203,8 +203,8 @@ by apply/funext => y;rewrite /g /h /= [X in F (X + _)]mulr1.
 Qed.
 
 Corollary FTC1 f a : mu.-integrable setT (EFin \o f) ->
-  let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in
-  {ae mu, forall x, a < BRight x -> derivable F x 1 /\ F^`() x = f x}.
+  let F x : R^o := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in
+  {ae mu, forall x, a < BRight x -> derivable (F : R^o -> R^o) x 1 /\ F^`() x = f x}.
 Proof.
 move=> intf F.
 have /lebesgue_differentiation : locally_integrable setT f.
@@ -214,22 +214,22 @@ by move=> i fi ai; apply: FTC1_lebesgue_pt => //; rewrite ltNyr.
 Qed.
 
 Corollary FTC1Ny f : mu.-integrable setT (EFin \o f) ->
-  let F x := (\int[mu]_(t in [set` `]-oo, x]]) (f t))%R in
-  {ae mu, forall x, derivable F x 1 /\ F^`() x = f x}.
+  let F x : R^o := (\int[mu]_(t in [set` `]-oo, x]]) (f t))%R in
+  {ae mu, forall x, derivable (F : R^o -> R^o) x 1 /\ F^`() x = f x}.
 Proof.
 move=> intf F; have := FTC1 -oo%O intf.
 apply: filterS; first exact: (ae_filter_ringOfSetsType mu).
 by move=> r /=; apply; rewrite ltNyr.
 Qed.
 
 Corollary continuous_FTC1 f a : mu.-integrable setT (EFin \o f) ->
-  let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in
+  let F x : R^o := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in
   forall x, a < BRight x -> {for x, continuous f} ->
-  derivable F x 1 /\ F^`() x = f x.
+  derivable (F : R^o -> R^o) x 1 /\ F^`() x = f x.
 Proof.
 move=> fi F x ax fx; have lfx : lebesgue_pt f x.
   near (0%R:R)^'+ => e; apply: (@continuous_lebesgue_pt _ _ _ (ball x e)).
-  - exact: ball_open_nbhs.
+  - exact: (@ball_open_nbhs _ R^o).
   - exact: measurable_ball.
   - by apply/measurable_funTS/EFin_measurable_fun; exact: measurable_int fi.
   - exact: fx.
@@ -294,12 +294,12 @@ 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).
   by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setIidr.
-apply/cvgrPdist_le => /= e e0; rewrite near_simpl; near=> x.
+apply/(@cvgrPdist_le _ R^o) => /= e e0; near=> x.
 rewrite {1}/int /parameterized_integral sub0r normrN.
 have [|xa] := leP a x.
   move=> ax; apply/ltW; move: ax.
@@ -319,7 +319,7 @@ have /= int_normr_cont : forall e : R, 0 < e ->
   by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setTI.
 have intfab : mu.-integrable `[a, b] (EFin \o fab).
   by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setIidr.
-rewrite /int /parameterized_integral; apply/cvgrPdist_le => /= e e0.
+rewrite /int /parameterized_integral; apply/(@cvgrPdist_le _ R^o) => /= e e0.
 have [d [d0 /= {}int_normr_cont]] := int_normr_cont _ e0.
 near=> x.
 rewrite [in X in X - _](@itv_bndbnd_setU _ _ _ (BRight x))//;
@@ -363,8 +363,7 @@ have /= int_normr_cont : forall e : R, 0 < e ->
 have intfab : mu.-integrable `[a, b] (EFin \o fab).
   by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setIidr.
 rewrite /int /parameterized_integral => z; rewrite in_itv/= => /andP[az zb].
-apply/cvgrPdist_le => /= e e0.
-rewrite near_simpl.
+apply/(@cvgrPdist_le _ R^o) => /= e e0.
 have [d [d0 /= {}int_normr_cont]] := int_normr_cont _ e0.
 near=> x.
 have [xz|xz|->] := ltgtP x z; last by rewrite subrr normr0 ltW.
@@ -425,28 +424,28 @@ Notation mu := lebesgue_measure.
 Local Open Scope ereal_scope.
 Implicit Types (f : R -> R) (a b : R).
 
-Corollary continuous_FTC2 f F a b : (a < b)%R -> {in `[a, b], continuous f} ->
+Corollary continuous_FTC2 (f F : R^o -> R^o) a b : (a < b)%R -> {in `[a, b], continuous f} ->
   derivable_oo_continuous_bnd F a b ->
   {in `]a, b[, F^`() =1 f} ->
   (\int[mu]_(x in `[a, b]) (f x)%:E = (F b)%:E - (F a)%:E)%E.
 Proof.
 move=> ab cf dF F'f.
 pose fab := f \_ `[a, b].
-pose G x : R := (\int[mu]_(t in `[a, x]) fab t)%R.
+pose G x : R^o := (\int[mu]_(t in `[a, x]) fab t)%R.
 have iabf : mu.-integrable `[a, b] (EFin \o f).
   apply: continuous_compact_integrable; first exact: segment_compact.
   by apply: continuous_in_subspaceT => x /[!inE] => /cf.
 have ifab : mu.-integrable setT (EFin \o fab).
   by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setTI.
-have G'f : {in `]a, b[, forall x, G^`() x = fab x /\ derivable G x 1}.
+have G'f : {in `]a, b[, forall x, G^`() x = fab x /\ derivable (G : R^o -> R^o) x 1}.
   move=> x /[!in_itv]/= /andP[ax xb].
   have := @continuous_FTC1 _ _ (BLeft a) ifab x.
   rewrite /= lte_fin => /(_ ax).
   have : {for x, continuous fab}.
     have /cf xf : x \in `[a, b] by rewrite in_itv/= (ltW ax) (ltW xb).
     rewrite /prop_for /continuous_at {2}/fab/= patchE.
     rewrite mem_set ?mulr1 /=; last by rewrite in_itv/= (ltW ax) (ltW xb).
-    apply: cvg_trans xf; apply: near_eq_cvg; rewrite !near_simpl; near=> z.
+    apply: cvg_trans xf; apply: near_eq_cvg; near=> z.
     rewrite /fab/= patchE mem_set ?mulr1//=.
     near: z; have := @near_in_itv R a b x.
     rewrite in_itv/= ax xb => /(_ isT).
@@ -469,11 +468,11 @@ have [k FGk] : exists k : R, {in `]a, b[, (F - G =1 cst k)%R}.
         + by move: yab; rewrite in_itv/= => /andP[_ /ltW].
       have Fz1 : derivable F z 1.
         by case: dF => /= + _ _; apply; rewrite inE in zab.
-      have Gz1 : derivable G z 1 by have [|] := G'f z.
+      have Gz1 : derivable (G : R^o -> R^o) z 1 by have [|] := G'f z.
       apply: DeriveDef.
       + by apply: derivableB; [exact: Fz1|exact: Gz1].
       + by rewrite deriveB -?derive1E; [by []|exact: Fz1|exact: Gz1].
-    - apply: derivable_within_continuous => z zxy.
+    - apply: (@derivable_within_continuous _ R^o) => z zxy.
       apply: derivableB.
       + case: dF => /= + _ _; apply.
         rewrite in_itv/=; move: zxy; rewrite in_itv/= => /andP[xz zy].
@@ -519,7 +518,7 @@ have GbcFb : G x @[x --> b^'-] --> (- c + F b)%R.
 have contF : {within `[a, b], continuous F}.
   apply/(continuous_within_itvP _ ab); split; last exact: (conj Fa Fb).
   move=> z zab.
-  apply/differentiable_continuous/derivable1_diffP.
+  apply/(@differentiable_continuous _ R^o R^o)/derivable1_diffP.
   by case: dF => /= dF _ _; apply: dF.
 have iabfab : mu.-integrable `[a, b] (EFin \o fab).
   by rewrite -restrict_EFin; apply/integrable_restrict => //; rewrite setIidr.