equivalence between exponential funcitons in stdlib and mca

CHANGELOG_UNRELEASED.md

@@ -9,6 +9,7 @@
 
 - file `Rstruct.v`
   + lemma `Pos_to_natE` (from `mathcomp_extra.v`)
+  + lemmas `RabsE`, `RdistE`, `sum_f_R0E`, `factE`
 
 - new file `internal_Eqdep_dec.v` (don't use, internal, to be removed)
 
@@ -29,6 +30,9 @@
   + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`
   + lemma `preimage_set_system_id`
 
+- in `Rstruct_topology.v`:
+  + lemma `RexpE`
+
 ### Changed
 
 - file `nsatz_realtype.v` moved from `reals` to `reals-stdlib` package

analysis_stdlib/Rstruct_topology.v

@@ -10,11 +10,12 @@ Require Import Rtrigo1 Reals.
 From mathcomp Require Import all_ssreflect ssralg poly mxpoly ssrnum.
 From mathcomp Require Import archimedean.
 From HB Require Import structures.
-From mathcomp Require Import mathcomp_extra.
-From mathcomp Require Import boolp classical_sets.
+From mathcomp Require Import mathcomp_extra boolp classical_sets.
 From mathcomp Require Import reals interval_inference.
-From mathcomp Require Import topology.
 From mathcomp Require Export Rstruct.
+From mathcomp Require Import topology.
+(* The following line is for RexpE. *)
+From mathcomp Require normedtype sequences.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -87,3 +88,24 @@ Lemma nbhs_pt_comp (P : R -> Prop) (f : R -> R) (x : R) :
 Proof. by move=> Lf /continuity_pt_cvg; apply. Qed.
 
 End analysis_struct.
+
+Module RexpE.
+Import normedtype sequences.
+
+(* proof by comparing the defining power series *)
+Lemma RexpE (x : R) : Rtrigo_def.exp x = expR x.
+Proof.
+apply/esym; rewrite /exp /exist_exp; case: Alembert_C3 => y.
+rewrite /Pser /infinite_sum /= => exp_ub.
+rewrite /expR /exp_coeff /series/=; apply: (@cvg_lim R^o) => //.
+rewrite -cvg_shiftS /=; apply/cvgrPdist_lt => /= e /RltP /exp_ub[N Nexp_ub].
+near=> n.
+have nN : (n >= N)%coq_nat by apply/ssrnat.leP; near: n; exact: nbhs_infty_ge.
+move: Nexp_ub => /(_ _ nN) /[!RdistE] /RltP /=.
+rewrite distrC sum_f_R0E; congr (`| _ - _ | < e).
+by apply: eq_bigr=> k _; rewrite RinvE RpowE mulrC factE INRE.
+Unshelve. all: by end_near. Qed.
+
+End RexpE.
+
+Definition RexpE := RexpE.RexpE.

reals_stdlib/Rstruct.v

@@ -525,6 +525,24 @@ case: (lerP x y) => H; first by rewrite Rmin_left //; apply: RlebP.
 by rewrite ?ltW // Rmin_right //;  apply/RlebP; move/ltW : H.
 Qed.
 
+Lemma RabsE x : Rabs x = `|x|.
+Proof.
+by rewrite /Rabs; case: Rcase_abs => [/RltP x0|/Rge_le/RleP x0];
+  [rewrite ltr0_norm|rewrite ger0_norm].
+Qed.
+
+Lemma RdistE x y : Rdist x y = `|x - y|.
+Proof. by rewrite /Rdist RabsE RminusE. Qed.
+
+Lemma sum_f_R0E f n : sum_f_R0 f n = \sum_(0 <= k < n.+1) f k.
+Proof.
+elim: n => [|n ih/=]; first by rewrite big_nat1.
+by rewrite RplusE big_nat_recr//= ih.
+Qed.
+
+Lemma factE n : fact n = n`!.
+Proof. by elim: n => //= n ih; rewrite factS mulSn ih. Qed.
+
 Section bigmaxr.
 Context {R : realDomainType}.