update w.r.t. master

_CoqProject

@@ -35,6 +35,5 @@ theories/altreals/discrete.v
 theories/altreals/realseq.v
 theories/altreals/realsum.v
 theories/altreals/distr.v
-theories/inverse_continuous.v
 
 -R theories mathcomp.analysis

theories/exp.v

@@ -4,7 +4,7 @@ From mathcomp Require Import matrix interval rat.
 Require Import boolp reals ereal.
 Require Import nsatz_realtype.
 Require Import classical_sets posnum topology normedtype landau sequences.
-Require Import derive inverse_continuous.
+Require Import derive realfun.
 
 (******************************************************************************)
 (*               Theory of exponential/logarithm functions                    *)
@@ -68,68 +68,13 @@ Qed.
   f = g -> (f --> lim f) = (g --> lim g).
 Proof. by move=> R1 f1 g1 ->. Qed.*)
 
-Lemma eq_cvgl (f g : R ^nat) (x : R) : f = g -> (f --> x) = (g --> x).
-Proof. by move->. Qed.
-
-(* NB: PR in progress *)
-Lemma seriesN (f : R ^nat) : series (- f) = - series f.
-Proof. by rewrite funeqE => n; rewrite /series /= sumrN. Qed.
-
-Lemma seriesZr (f : R ^nat) k : series (k *: f) = k *: series f.
-Proof. by rewrite funeqE => n; rewrite /series /= -scaler_sumr. Qed.
-
-Lemma seriesD (f g : R ^nat) : series (f + g) = series f + series g.
-Proof. by rewrite /series /= funeqE => n; rewrite big_split. Qed.
-
-Lemma is_cvg_seriesN (f : R ^nat) : cvg (series (- f)) = cvg (series f).
-Proof. by rewrite seriesN is_cvgNE. Qed.
-
-Lemma lim_seriesN (f : R ^nat) : cvg (series f) ->
-  lim (series (- f)) = - lim (series f).
-Proof. by move=> cf; rewrite seriesN limN. Qed.
-
-Lemma is_cvg_seriesZr (f : R ^nat) k : cvg (series f) -> cvg (series (k *: f)).
-Proof. by move=> cf; rewrite seriesZr; exact: is_cvgZr. Qed.
-
-Lemma lim_seriesZr (f : R ^nat) k : cvg (series f) ->
-  lim (series (k *: f)) = k *: lim (series f).
-Proof. by move=> cf; rewrite seriesZr limZr. Qed.
-
-Lemma is_cvg_seriesD (f g : R ^nat) :
-  cvg (series f) -> cvg (series g) -> cvg (series (f + g)).
-Proof. by move=> cf cg; rewrite seriesD; exact: is_cvgD. Qed.
-
-Lemma lim_seriesD (f g : R ^nat) : cvg (series f) -> cvg (series g) ->
-  lim (series (f + g)) = lim (series f) + lim (series g).
-Proof. by move=> cf cg; rewrite seriesD limD. Qed.
-
-Lemma is_cvg_seriesB (f g : R ^nat) :
-  cvg (series f) -> cvg (series g) -> cvg (series (f - g)).
-Proof. by move=> cf cg; apply: is_cvg_seriesD; rewrite ?is_cvg_seriesN. Qed.
-
-Lemma lim_seriesB (f g : R ^nat) : cvg (series f) -> cvg (series g) ->
-  lim (series (f - g)) = lim (series f) - lim (series g).
-Proof. by move=> Cf Cg; rewrite lim_seriesD ?is_cvg_seriesN// lim_seriesN. Qed.
-
-Lemma lim_series_norm (f : R ^nat) :
-  cvg [normed series f] -> `|lim (series f)| <= lim [normed series f].
-Proof.
-move=> cnf; have cf := normed_cvg cnf.
-rewrite -lim_norm // (ler_lim (is_cvg_norm cf) cnf) //.
-by near=> x; rewrite ler_norm_sum.
-Grab Existential Variables. all: end_near. Qed.
-
-Lemma lim_series_le (f g : R ^nat) :
-  cvg (series f) -> cvg (series g) -> (forall n, f n <= g n) ->
-  lim (series f) <= lim (series g).
-Proof.
-by move=> cf cg fg; apply (ler_lim cf cg); near=> x; rewrite ler_sum.
-Grab Existential Variables. all: end_near. Qed.
-(* /NB: PR in progress *)
+(* NB: useful? *)
+(*Lemma eq_cvgl (f g : R ^nat) (x : R) : f = g -> (f --> x) = (g --> x).
+Proof. by move->. Qed.*)
 
 Lemma cvg_to_0_linear (f : R -> R) K k :
   0 < k -> (forall h, 0 < `|h| < k -> `|f h| <= K * `|h|) ->
-    f x @[x --> nbhs' (0 : R)] --> (0 : R).
+    f x @[x --> (0 : R)^'] --> (0 : R).
 Proof.
 move=> k0 kfK; have [K0|K0] := lerP K 0.
 - apply/cvg_distP => _/posnumP[e]; rewrite near_map; near=> x.
@@ -151,19 +96,19 @@ Grab Existential Variables. all: end_near. Qed.
 Lemma lim_cvg_to_0_linear (f : nat -> R) (g : R -> nat -> R) k :
   0 < k -> cvg (series f) ->
   (forall h : R, 0 < `|h| < k -> forall n, `|g h n| <= f n * `|h|) ->
-  lim (series (g x)) @[x --> nbhs' (0 : R)] --> (0 : R).
+  lim (series (g x)) @[x --> (0 : R)^'] --> (0 : R).
 Proof.
 move=> k_gt0 Cf Hg.
 apply: (@cvg_to_0_linear _ (lim (series f)) k) => // h hLk; rewrite mulrC.
-have Ckf := @is_cvg_seriesZr _ `|h| Cf.
-have Lkf := lim_seriesZr `|h| Cf.
+have Ckf := @is_cvg_seriesZ _ _ `|h| Cf.
+have Lkf := lim_seriesZ `|h| Cf.
 have Cng : cvg [normed series (g h)].
   apply: series_le_cvg (Hg _ hLk) _  => //.
     by move=> h1; apply: le_trans (Hg _ hLk _).
   by rewrite (funext (fun _ => (@mulrC R _ _))).
 apply: le_trans (_ : lim [normed series (g h)] <= _).
   by apply: lim_series_norm.
-rewrite -[_ * _]lim_seriesZr //.
+rewrite -[_ * _]lim_seriesZ //.
 apply: lim_series_le => //= => n.
 by rewrite [X in _ <= X]mulrC; apply: Hg.
 Qed.
@@ -175,10 +120,10 @@ Variables (K : numFieldType) (U V : normedModType K).
 
 Lemma continuous_shift (f : U -> V) u :
   {for u, continuous f} = {for 0, continuous (f \o shift u)}.
-Proof. by rewrite [in RHS]forE /= add0r cvg_shift add0r. Qed.
+Proof. by rewrite [in RHS]forE /= add0r cvg_comp_shift add0r. Qed.
 
 Lemma continuous_withinNshiftx (f : U -> V) u :
-  f \o shift u @ nbhs' 0 --> f u <-> {for u, continuous f}.
+  f \o shift u @ 0^' --> f u <-> {for u, continuous f}.
 Proof.
 rewrite continuous_shift; split=> [cfu|].
   by apply/(continuous_withinNx _ _).2/(cvg_trans cfu); rewrite /= add0r.
@@ -197,7 +142,6 @@ rewrite diff_comp // !derive1E' //= -[X in 'd  _ _ X = _]mulr1.
 by rewrite [LHS]linearZ mulrC.
 Qed.
 
-
 (******************************************************************************)
 (* Unfold function application (f + f) 0 gives f 0 + f 0                      *)
 (******************************************************************************)
@@ -257,7 +201,7 @@ Variable R : realType.
 (* Attempt to prove the diff of inverse *)
 
 Lemma is_derive1_caratheodory (f : R -> R) (x a : R) :
-  is_derive x 1 f a <-> 
+  is_derive x 1 f a <->
   exists g, [/\ forall z, f z - f x = g z * (z - x),
         {for x, continuous g} & g x = a].
 Proof.
@@ -267,18 +211,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 @ nbhs' 0 --> a by case: Hd => H1 <-.
+    have F1 : g1 @ 0^' --> a by case: Hd => H1 <-.
     apply: cvg_trans F1; apply: near_eq_cvg; rewrite /g1; rcfE.
     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 --> nbhs' 0] --> a.
+suff Hf : h^-1 *: ((f \o shift x) h%:A - f x) @[h --> 0^'] --> 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 --> nbhs' 0] --> a.
+  have F1 :  (g \o shift x) y @[y --> 0^'] --> a.
   by rewrite -gxE; apply/continuous_withinNshiftx.
 apply: cvg_trans F1; apply: near_eq_cvg.
 near=> y.
@@ -318,7 +262,7 @@ constructor; first by apply: derivableV => //; case: Df.
 by rewrite deriveV //; case: Df => _ ->.
 Qed.
 
-Lemma is_derive_inverse (f g : R ->R) l x :  
+Lemma is_derive_inverse (f g : R ->R) l x :
   {near x, cancel f g}  ->
   {near x, continuous f}  ->
   is_derive x 1 f l -> l != 0 -> is_derive (f x) 1 g l^-1.
@@ -327,7 +271,7 @@ move=> fgK fC fD lNZ.
 have /is_derive1_caratheodory [h [fE hC hxE]] := fD.
 (* There should be something simpler *)
 have gfxE :  g (f x) = x by have [d Hd]:= nbhs_ex fgK; apply: Hd.
-pose g1 y := if y == f x then (h (g y))^-1 
+pose g1 y := if y == f x then (h (g y))^-1
              else (g y - g (f x)) / (y - f x).
 apply/is_derive1_caratheodory.
 exists g1; split; first 2 last.
@@ -337,11 +281,11 @@ exists g1; split; first 2 last.
 have F1 : (h (g x))^-1 @[x --> f x] --> g1 (f x).
   rewrite /g1 eqxx; apply: continuousV; first by rewrite /= gfxE hxE.
   apply: continuous_comp; last by rewrite gfxE.
-  by apply: nbhs_singleton (continuous_inverse _ _).
+  by apply: nbhs_singleton (near_can_continuous _ _).
 apply: cvg_sub0 F1.
 apply/cvg_distP => eps eps_gt0 /=; rewrite !near_simpl /=.
 near=> y; rewrite sub0r normrN; rcfE.
-have fgyE : f (g y) = y by near: y; apply: inverse_swap_continuous.
+have fgyE : f (g y) = y by near: y; apply: near_continuous_can_sym.
 rewrite /g1; case: eqP => [_|/eqP x1Dfx]; first by rewrite subrr normr0.
 have -> : y - f x  = h (g y) * (g y - x) by rewrite -fE fgyE.
 rewrite gfxE invfM mulrC divfK ?subrr ?normr0 // subr_eq0.
@@ -421,12 +365,10 @@ Lemma diffs_equiv f x :
   cvg (series s1) -> series s2 --> lim (series s1).
 Proof.
 move=> s1 s2 Cx; rewrite -[lim _]subr0 [X in X --> _]/series /=.
-have s2E n :
-  \sum_(0 <= i < n) s2 i = \sum_(0 <= i < n) s1 i - n%:R * f n * x ^+ n.-1.
-  by rewrite diffs_sumE addrK.
-rewrite (eq_cvgl _ (funext s2E)).
-apply: cvgB => //; rewrite -cvg_shiftS.
-by apply: cvg_series_cvg_0.
+rewrite (_ : (fun n => _) =
+    (fun n => \sum_(0 <= i < n) s1 i - n%:R * f n * x ^+ n.-1)); last first.
+  by rewrite funeqE => n; rewrite diffs_sumE addrK.
+by apply: cvgB => //; rewrite -cvg_shiftS; exact: cvg_series_cvg_0.
 Qed.
 
 Lemma is_cvg_diffs_equiv f x :
@@ -510,7 +452,7 @@ Proof.
 move=> Ck CdK CddK xLK; set s := (fun n : nat => _).
 set (f := fun x => _).
 suff Hf :
-  h^-1 *: (f (h + x) - f x) @[h --> nbhs' 0] --> lim (series s).
+  h^-1 *: (f (h + x) - f x) @[h --> 0^'] --> lim (series s).
   have F : f^`() x = lim (series s) by  apply: cvg_lim Hf.
   rewrite (_ : (fun h => h^-1 *: (f (h + x) - f x)) =
               (fun h => h^-1 *: (f (h%:A + x) - f x))) in Hf; last first.
@@ -521,7 +463,7 @@ set sx := fun n : nat => c n * x ^+ n.
 have Csx : cvg (series sx) by apply: is_cvg_series_Xn_inside Ck _.
 pose shx := fun h (n : nat) => c n * (h + x) ^+ n.
 suff Cc :
-      lim (h^-1 *: (series (shx h - sx))) @[h --> nbhs' 0] --> lim (series s).
+      lim (h^-1 *: (series (shx h - sx))) @[h --> 0^'] --> lim (series s).
   apply: cvg_sub0 Cc.
   apply/cvg_distP => eps eps_gt0 /=; rewrite !near_simpl /=.
   near=> h; rewrite sub0r normrN /=.
@@ -544,7 +486,7 @@ apply: cvg_zero => /=.
 suff Cc :
   lim (series
        (fun n => c n * (((h + x) ^+ n - x ^+ n) / h - n%:R * x ^+ n.-1)))
-   @[h --> nbhs' 0] --> (0 : R).
+   @[h --> 0^'] --> (0 : R).
   apply: cvg_sub0 Cc.
   apply/cvg_distP => eps eps_gt0 /=.
   rewrite !near_simpl /=.
@@ -567,7 +509,7 @@ suff Cc :
     rewrite ler_pdivr_mulr // mulr2n mulrDr mulr1.
     by rewrite ler_paddr // subr_ge0 ltW.
   have C1 := is_cvg_seriesB Cshx Csx.
-  have Ckf := @is_cvg_seriesZr _ _ h^-1 C1.
+  have Ckf := @is_cvg_seriesZ _ _ h^-1 C1.
   have Cu :
    (series (h^-1 *: (shx h - sx)) - series s1) x0 @[x0 --> \oo] -->
     lim (series (h^-1 *: (shx h - sx))) - lim (series s).
@@ -796,7 +738,7 @@ move=> x_ge1; have x_ge0 : 0 <= x by apply: le_trans x_ge1.
 case: (@IVT _ (fun y => expR y - x) 0 x 0) => //.
 - move=> x1 x1Ix; apply: continuousB => // y1.
     by apply: continuous_expR.
-  by apply: continuous_cst.
+  by apply: cst_continuous.
 rewrite expR0; case: (ltrgtP (1- x) (expR x - x)) => [_| |].
 - rewrite subr_le0 x_ge1 subr_ge0.
   by apply: le_trans (expR_ge1Dx _); rewrite ?ler_addr.
@@ -913,7 +855,7 @@ Qed.
 Lemma continuous_ln x : 0 < x -> {for x, continuous ln}.
 Proof.
 move=> x_gt0; rewrite -[x]lnK//.
-apply: nbhs_singleton (continuous_inverse _ _); near=> z; first by apply: expK.
+apply: nbhs_singleton (near_can_continuous _ _); near=> z; first exact: expK.
 by apply: continuous_expR.
 Grab Existential Variables. all: end_near. Qed.