diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-29 17:28:49 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-29 17:28:49 +0000 |
| commit | 9a6e3fe764dc2543dfa94de20fe5eec42d6be705 (patch) | |
| tree | 77c0021911e3696a8c98e35a51840800db4be2a9 /theories/Reals/Exp_prop.v | |
| parent | 9058fb97426307536f56c3e7447be2f70798e081 (diff) | |
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Exp_prop.v')
| -rw-r--r-- | theories/Reals/Exp_prop.v | 1803 |
1 files changed, 962 insertions, 841 deletions
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index 5c06af34a..c424b9e14 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -8,883 +8,1004 @@ (*i $Id$ i*) -Require Rbase. -Require Rfunctions. -Require SeqSeries. -Require Rtrigo. -Require Ranalysis1. -Require PSeries_reg. -Require Div2. -Require Even. -Require Max. -V7only [Import R_scope.]. +Require Import Rbase. +Require Import Rfunctions. +Require Import SeqSeries. +Require Import Rtrigo. +Require Import Ranalysis1. +Require Import PSeries_reg. +Require Import Div2. +Require Import Even. +Require Import Max. Open Local Scope nat_scope. -V7only [Import nat_scope.]. Open Local Scope R_scope. -Definition E1 [x:R] : nat->R := [N:nat](sum_f_R0 [k:nat]``/(INR (fact k))*(pow x k)`` N). +Definition E1 (x:R) (N:nat) : R := + sum_f_R0 (fun k:nat => / INR (fact k) * x ^ k) N. -Lemma E1_cvg : (x:R) (Un_cv (E1 x) (exp x)). -Intro; Unfold exp; Unfold projT1. -Case (exist_exp x); Intro. -Unfold exp_in Un_cv; Unfold infinit_sum E1; Trivial. +Lemma E1_cvg : forall x:R, Un_cv (E1 x) (exp x). +intro; unfold exp in |- *; unfold projT1 in |- *. +case (exist_exp x); intro. +unfold exp_in, Un_cv in |- *; unfold infinit_sum, E1 in |- *; trivial. Qed. -Definition Reste_E [x,y:R] : nat->R := [N:nat](sum_f_R0 [k:nat](sum_f_R0 [l:nat]``/(INR (fact (S (plus l k))))*(pow x (S (plus l k)))*(/(INR (fact (minus N l)))*(pow y (minus N l)))`` (pred (minus N k))) (pred N)). +Definition Reste_E (x y:R) (N:nat) : R := + sum_f_R0 + (fun k:nat => + sum_f_R0 + (fun l:nat => + / INR (fact (S (l + k))) * x ^ S (l + k) * + (/ INR (fact (N - l)) * y ^ (N - l))) ( + pred (N - k))) (pred N). -Lemma exp_form : (x,y:R;n:nat) (lt O n) -> ``(E1 x n)*(E1 y n)-(Reste_E x y n)==(E1 (x+y) n)``. -Intros; Unfold E1. -Rewrite cauchy_finite. -Unfold Reste_E; Unfold Rminus; Rewrite Rplus_assoc; Rewrite Rplus_Ropp_r; Rewrite Rplus_Or; Apply sum_eq; Intros. -Rewrite binomial. -Rewrite scal_sum; Apply sum_eq; Intros. -Unfold C; Unfold Rdiv; Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym (INR (fact i))); Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1r; Rewrite Rinv_Rmult. -Ring. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Apply H. +Lemma exp_form : + forall (x y:R) (n:nat), + (0 < n)%nat -> E1 x n * E1 y n - Reste_E x y n = E1 (x + y) n. +intros; unfold E1 in |- *. +rewrite cauchy_finite. +unfold Reste_E in |- *; unfold Rminus in |- *; rewrite Rplus_assoc; + rewrite Rplus_opp_r; rewrite Rplus_0_r; apply sum_eq; + intros. +rewrite binomial. +rewrite scal_sum; apply sum_eq; intros. +unfold C in |- *; unfold Rdiv in |- *; repeat rewrite Rmult_assoc; + rewrite (Rmult_comm (INR (fact i))); repeat rewrite Rmult_assoc; + rewrite <- Rinv_l_sym. +rewrite Rmult_1_r; rewrite Rinv_mult_distr. +ring. +apply INR_fact_neq_0. +apply INR_fact_neq_0. +apply INR_fact_neq_0. +apply H. Qed. -Definition maj_Reste_E [x,y:R] : nat->R := [N:nat]``4*(pow (Rmax R1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (S (S O)) N))/(Rsqr (INR (fact (div2 (pred N)))))``. +Definition maj_Reste_E (x y:R) (N:nat) : R := + 4 * + (Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (2 * N) / + Rsqr (INR (fact (div2 (pred N))))). -Lemma Rle_Rinv : (x,y:R) ``0<x`` -> ``0<y`` -> ``x<=y`` -> ``/y<=/x``. -Intros; Apply Rle_monotony_contra with x. -Apply H. -Rewrite <- Rinv_r_sym. -Apply Rle_monotony_contra with y. -Apply H0. -Rewrite Rmult_1r; Rewrite Rmult_sym; Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1r; Apply H1. -Red; Intro; Rewrite H2 in H0; Elim (Rlt_antirefl ? H0). -Red; Intro; Rewrite H2 in H; Elim (Rlt_antirefl ? H). +Lemma Rle_Rinv : forall x y:R, 0 < x -> 0 < y -> x <= y -> / y <= / x. +intros; apply Rmult_le_reg_l with x. +apply H. +rewrite <- Rinv_r_sym. +apply Rmult_le_reg_l with y. +apply H0. +rewrite Rmult_1_r; rewrite Rmult_comm; rewrite Rmult_assoc; + rewrite <- Rinv_l_sym. +rewrite Rmult_1_r; apply H1. +red in |- *; intro; rewrite H2 in H0; elim (Rlt_irrefl _ H0). +red in |- *; intro; rewrite H2 in H; elim (Rlt_irrefl _ H). Qed. (**********) -Lemma div2_double : (N:nat) (div2 (mult (2) N))=N. -Intro; Induction N. -Reflexivity. -Replace (mult (2) (S N)) with (S (S (mult (2) N))). -Simpl; Simpl in HrecN; Rewrite HrecN; Reflexivity. -Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring. +Lemma div2_double : forall N:nat, div2 (2 * N) = N. +intro; induction N as [| N HrecN]. +reflexivity. +replace (2 * S N)%nat with (S (S (2 * N))). +simpl in |- *; simpl in HrecN; rewrite HrecN; reflexivity. +apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR; + ring. Qed. -Lemma div2_S_double : (N:nat) (div2 (S (mult (2) N)))=N. -Intro; Induction N. -Reflexivity. -Replace (mult (2) (S N)) with (S (S (mult (2) N))). -Simpl; Simpl in HrecN; Rewrite HrecN; Reflexivity. -Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring. +Lemma div2_S_double : forall N:nat, div2 (S (2 * N)) = N. +intro; induction N as [| N HrecN]. +reflexivity. +replace (2 * S N)%nat with (S (S (2 * N))). +simpl in |- *; simpl in HrecN; rewrite HrecN; reflexivity. +apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR; + ring. Qed. -Lemma div2_not_R0 : (N:nat) (lt (1) N) -> (lt O (div2 N)). -Intros; Induction N. -Elim (lt_n_O ? H). -Cut (lt (1) N)\/N=(1). -Intro; Elim H0; Intro. -Assert H2 := (even_odd_dec N). -Elim H2; Intro. -Rewrite <- (even_div2 ? a); Apply HrecN; Assumption. -Rewrite <- (odd_div2 ? b); Apply lt_O_Sn. -Rewrite H1; Simpl; Apply lt_O_Sn. -Inversion H. -Right; Reflexivity. -Left; Apply lt_le_trans with (2); [Apply lt_n_Sn | Apply H1]. +Lemma div2_not_R0 : forall N:nat, (1 < N)%nat -> (0 < div2 N)%nat. +intros; induction N as [| N HrecN]. +elim (lt_n_O _ H). +cut ((1 < N)%nat \/ N = 1%nat). +intro; elim H0; intro. +assert (H2 := even_odd_dec N). +elim H2; intro. +rewrite <- (even_div2 _ a); apply HrecN; assumption. +rewrite <- (odd_div2 _ b); apply lt_O_Sn. +rewrite H1; simpl in |- *; apply lt_O_Sn. +inversion H. +right; reflexivity. +left; apply lt_le_trans with 2%nat; [ apply lt_n_Sn | apply H1 ]. Qed. -Lemma Reste_E_maj : (x,y:R;N:nat) (lt O N) -> ``(Rabsolu (Reste_E x y N))<=(maj_Reste_E x y N)``. -Intros; Pose M := (Rmax R1 (Rmax (Rabsolu x) (Rabsolu y))). -Apply Rle_trans with (Rmult (pow M (mult (2) N)) (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``/(Rsqr (INR (fact (div2 (S N)))))`` (pred (minus N k))) (pred N))). -Unfold Reste_E. -Apply Rle_trans with (sum_f_R0 [k:nat](Rabsolu (sum_f_R0 [l:nat]``/(INR (fact (S (plus l k))))*(pow x (S (plus l k)))*(/(INR (fact (minus N l)))*(pow y (minus N l)))`` (pred (minus N k)))) (pred N)). -Apply (sum_Rabsolu [k:nat](sum_f_R0 [l:nat]``/(INR (fact (S (plus l k))))*(pow x (S (plus l k)))*(/(INR (fact (minus N l)))*(pow y (minus N l)))`` (pred (minus N k))) (pred N)). -Apply Rle_trans with (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(Rabsolu (/(INR (fact (S (plus l k))))*(pow x (S (plus l k)))*(/(INR (fact (minus N l)))*(pow y (minus N l)))))`` (pred (minus N k))) (pred N)). -Apply sum_Rle; Intros. -Apply (sum_Rabsolu [l:nat]``/(INR (fact (S (plus l n))))*(pow x (S (plus l n)))*(/(INR (fact (minus N l)))*(pow y (minus N l)))``). -Apply Rle_trans with (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(pow M (mult (S (S O)) N))*/(INR (fact (S l)))*/(INR (fact (minus N l)))`` (pred (minus N k))) (pred N)). -Apply sum_Rle; Intros. -Apply sum_Rle; Intros. -Repeat Rewrite Rabsolu_mult. -Do 2 Rewrite <- Pow_Rabsolu. -Rewrite (Rabsolu_right ``/(INR (fact (S (plus n0 n))))``). -Rewrite (Rabsolu_right ``/(INR (fact (minus N n0)))``). -Replace ``/(INR (fact (S (plus n0 n))))*(pow (Rabsolu x) (S (plus n0 n)))* - (/(INR (fact (minus N n0)))*(pow (Rabsolu y) (minus N n0)))`` with ``/(INR (fact (minus N n0)))*/(INR (fact (S (plus n0 n))))*(pow (Rabsolu x) (S (plus n0 n)))*(pow (Rabsolu y) (minus N n0))``; [Idtac | Ring]. -Rewrite <- (Rmult_sym ``/(INR (fact (minus N n0)))``). -Repeat Rewrite Rmult_assoc. -Apply Rle_monotony. -Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. -Apply Rle_trans with ``/(INR (fact (S n0)))*(pow (Rabsolu x) (S (plus n0 n)))*(pow (Rabsolu y) (minus N n0))``. -Rewrite (Rmult_sym ``/(INR (fact (S (plus n0 n))))``); Rewrite (Rmult_sym ``/(INR (fact (S n0)))``); Repeat Rewrite Rmult_assoc; Apply Rle_monotony. -Apply pow_le; Apply Rabsolu_pos. -Rewrite (Rmult_sym ``/(INR (fact (S n0)))``); Apply Rle_monotony. -Apply pow_le; Apply Rabsolu_pos. -Apply Rle_Rinv. -Apply INR_fact_lt_0. -Apply INR_fact_lt_0. -Apply le_INR; Apply fact_growing; Apply le_n_S. -Apply le_plus_l. -Rewrite (Rmult_sym ``(pow M (mult (S (S O)) N))``); Rewrite Rmult_assoc; Apply Rle_monotony. -Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. -Apply Rle_trans with ``(pow M (S (plus n0 n)))*(pow (Rabsolu y) (minus N n0))``. -Do 2 Rewrite <- (Rmult_sym ``(pow (Rabsolu y) (minus N n0))``). -Apply Rle_monotony. -Apply pow_le; Apply Rabsolu_pos. -Apply pow_incr; Split. -Apply Rabsolu_pos. -Apply Rle_trans with (Rmax (Rabsolu x) (Rabsolu y)). -Apply RmaxLess1. -Unfold M; Apply RmaxLess2. -Apply Rle_trans with ``(pow M (S (plus n0 n)))*(pow M (minus N n0))``. -Apply Rle_monotony. -Apply pow_le; Apply Rle_trans with R1. -Left; Apply Rlt_R0_R1. -Unfold M; Apply RmaxLess1. -Apply pow_incr; Split. -Apply Rabsolu_pos. -Apply Rle_trans with (Rmax (Rabsolu x) (Rabsolu y)). -Apply RmaxLess2. -Unfold M; Apply RmaxLess2. -Rewrite <- pow_add; Replace (plus (S (plus n0 n)) (minus N n0)) with (plus N (S n)). -Apply Rle_pow. -Unfold M; Apply RmaxLess1. -Replace (mult (2) N) with (plus N N); [Idtac | Ring]. -Apply le_reg_l. -Replace N with (S (pred N)). -Apply le_n_S; Apply H0. -Symmetry; Apply S_pred with O; Apply H. -Apply INR_eq; Do 2 Rewrite plus_INR; Do 2 Rewrite S_INR; Rewrite plus_INR; Rewrite minus_INR. -Ring. -Apply le_trans with (pred (minus N n)). -Apply H1. -Apply le_S_n. -Replace (S (pred (minus N n))) with (minus N n). -Apply le_trans with N. -Apply simpl_le_plus_l with n. -Rewrite <- le_plus_minus. -Apply le_plus_r. -Apply le_trans with (pred N). -Apply H0. -Apply le_pred_n. -Apply le_n_Sn. -Apply S_pred with O. -Apply simpl_lt_plus_l with n. -Rewrite <- le_plus_minus. -Replace (plus n (0)) with n; [Idtac | Ring]. -Apply le_lt_trans with (pred N). -Apply H0. -Apply lt_pred_n_n. -Apply H. -Apply le_trans with (pred N). -Apply H0. -Apply le_pred_n. -Apply Rle_sym1; Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. -Apply Rle_sym1; Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. -Rewrite scal_sum. -Apply sum_Rle; Intros. -Rewrite <- Rmult_sym. -Rewrite scal_sum. -Apply sum_Rle; Intros. -Rewrite (Rmult_sym ``/(Rsqr (INR (fact (div2 (S N)))))``). -Rewrite Rmult_assoc; Apply Rle_monotony. -Apply pow_le. -Apply Rle_trans with R1. -Left; Apply Rlt_R0_R1. -Unfold M; Apply RmaxLess1. -Assert H2 := (even_odd_cor N). -Elim H2; Intros N0 H3. -Elim H3; Intro. -Apply Rle_trans with ``/(INR (fact n0))*/(INR (fact (minus N n0)))``. -Do 2 Rewrite <- (Rmult_sym ``/(INR (fact (minus N n0)))``). -Apply Rle_monotony. -Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. -Apply Rle_Rinv. -Apply INR_fact_lt_0. -Apply INR_fact_lt_0. -Apply le_INR. -Apply fact_growing. -Apply le_n_Sn. -Replace ``/(INR (fact n0))*/(INR (fact (minus N n0)))`` with ``(C N n0)/(INR (fact N))``. -Pattern 1 N; Rewrite H4. -Apply Rle_trans with ``(C N N0)/(INR (fact N))``. -Unfold Rdiv; Do 2 Rewrite <- (Rmult_sym ``/(INR (fact N))``). -Apply Rle_monotony. -Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. -Rewrite H4. -Apply C_maj. -Rewrite <- H4; Apply le_trans with (pred (minus N n)). -Apply H1. -Apply le_S_n. -Replace (S (pred (minus N n))) with (minus N n). -Apply le_trans with N. -Apply simpl_le_plus_l with n. -Rewrite <- le_plus_minus. -Apply le_plus_r. -Apply le_trans with (pred N). -Apply H0. -Apply le_pred_n. -Apply le_n_Sn. -Apply S_pred with O. -Apply simpl_lt_plus_l with n. -Rewrite <- le_plus_minus. -Replace (plus n (0)) with n; [Idtac | Ring]. -Apply le_lt_trans with (pred N). -Apply H0. -Apply lt_pred_n_n. -Apply H. -Apply le_trans with (pred N). -Apply H0. -Apply le_pred_n. -Replace ``(C N N0)/(INR (fact N))`` with ``/(Rsqr (INR (fact N0)))``. -Rewrite H4; Rewrite div2_S_double; Right; Reflexivity. -Unfold Rsqr C Rdiv. -Repeat Rewrite Rinv_Rmult. -Rewrite (Rmult_sym (INR (fact N))). -Repeat Rewrite Rmult_assoc. -Rewrite <- Rinv_r_sym. -Rewrite Rmult_1r; Replace (minus N N0) with N0. -Ring. -Replace N with (plus N0 N0). -Symmetry; Apply minus_plus. -Rewrite H4. -Apply INR_eq; Rewrite plus_INR; Rewrite mult_INR; Do 2 Rewrite S_INR; Ring. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Unfold C Rdiv. -Rewrite (Rmult_sym (INR (fact N))). -Repeat Rewrite Rmult_assoc. -Rewrite <- Rinv_r_sym. -Rewrite Rinv_Rmult. -Rewrite Rmult_1r; Ring. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Replace ``/(INR (fact (S n0)))*/(INR (fact (minus N n0)))`` with ``(C (S N) (S n0))/(INR (fact (S N)))``. -Apply Rle_trans with ``(C (S N) (S N0))/(INR (fact (S N)))``. -Unfold Rdiv; Do 2 Rewrite <- (Rmult_sym ``/(INR (fact (S N)))``). -Apply Rle_monotony. -Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. -Cut (S N) = (mult (2) (S N0)). -Intro; Rewrite H5; Apply C_maj. -Rewrite <- H5; Apply le_n_S. -Apply le_trans with (pred (minus N n)). -Apply H1. -Apply le_S_n. -Replace (S (pred (minus N n))) with (minus N n). -Apply le_trans with N. -Apply simpl_le_plus_l with n. -Rewrite <- le_plus_minus. -Apply le_plus_r. -Apply le_trans with (pred N). -Apply H0. -Apply le_pred_n. -Apply le_n_Sn. -Apply S_pred with O. -Apply simpl_lt_plus_l with n. -Rewrite <- le_plus_minus. -Replace (plus n (0)) with n; [Idtac | Ring]. -Apply le_lt_trans with (pred N). -Apply H0. -Apply lt_pred_n_n. -Apply H. -Apply le_trans with (pred N). -Apply H0. -Apply le_pred_n. -Apply INR_eq; Rewrite H4. -Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring. -Cut (S N) = (mult (2) (S N0)). -Intro. -Replace ``(C (S N) (S N0))/(INR (fact (S N)))`` with ``/(Rsqr (INR (fact (S N0))))``. -Rewrite H5; Rewrite div2_double. -Right; Reflexivity. -Unfold Rsqr C Rdiv. -Repeat Rewrite Rinv_Rmult. -Replace (minus (S N) (S N0)) with (S N0). -Rewrite (Rmult_sym (INR (fact (S N)))). -Repeat Rewrite Rmult_assoc. -Rewrite <- Rinv_r_sym. -Rewrite Rmult_1r; Reflexivity. -Apply INR_fact_neq_0. -Replace (S N) with (plus (S N0) (S N0)). -Symmetry; Apply minus_plus. -Rewrite H5; Ring. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Apply INR_eq; Rewrite H4; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring. -Unfold C Rdiv. -Rewrite (Rmult_sym (INR (fact (S N)))). -Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym. -Rewrite Rmult_1r; Rewrite Rinv_Rmult. -Reflexivity. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Unfold maj_Reste_E. -Unfold Rdiv; Rewrite (Rmult_sym ``4``). -Rewrite Rmult_assoc. -Apply Rle_monotony. -Apply pow_le. -Apply Rle_trans with R1. -Left; Apply Rlt_R0_R1. -Apply RmaxLess1. -Apply Rle_trans with (sum_f_R0 [k:nat]``(INR (minus N k))*/(Rsqr (INR (fact (div2 (S N)))))`` (pred N)). -Apply sum_Rle; Intros. -Rewrite sum_cte. -Replace (S (pred (minus N n))) with (minus N n). -Right; Apply Rmult_sym. -Apply S_pred with O. -Apply simpl_lt_plus_l with n. -Rewrite <- le_plus_minus. -Replace (plus n (0)) with n; [Idtac | Ring]. -Apply le_lt_trans with (pred N). -Apply H0. -Apply lt_pred_n_n. -Apply H. -Apply le_trans with (pred N). -Apply H0. -Apply le_pred_n. -Apply Rle_trans with (sum_f_R0 [k:nat]``(INR N)*/(Rsqr (INR (fact (div2 (S N)))))`` (pred N)). -Apply sum_Rle; Intros. -Do 2 Rewrite <- (Rmult_sym ``/(Rsqr (INR (fact (div2 (S N)))))``). -Apply Rle_monotony. -Left; Apply Rlt_Rinv; Apply Rsqr_pos_lt. -Apply INR_fact_neq_0. -Apply le_INR. -Apply simpl_le_plus_l with n. -Rewrite <- le_plus_minus. -Apply le_plus_r. -Apply le_trans with (pred N). -Apply H0. -Apply le_pred_n. -Rewrite sum_cte; Replace (S (pred N)) with N. -Cut (div2 (S N)) = (S (div2 (pred N))). -Intro; Rewrite H0. -Rewrite fact_simpl; Rewrite mult_sym; Rewrite mult_INR; Rewrite Rsqr_times. -Rewrite Rinv_Rmult. -Rewrite (Rmult_sym (INR N)); Repeat Rewrite Rmult_assoc; Apply Rle_monotony. -Left; Apply Rlt_Rinv; Apply Rsqr_pos_lt; Apply INR_fact_neq_0. -Rewrite <- H0. -Cut ``(INR N)<=(INR (mult (S (S O)) (div2 (S N))))``. -Intro; Apply Rle_monotony_contra with ``(Rsqr (INR (div2 (S N))))``. -Apply Rsqr_pos_lt. -Apply not_O_INR; Red; Intro. -Cut (lt (1) (S N)). -Intro; Assert H4 := (div2_not_R0 ? H3). -Rewrite H2 in H4; Elim (lt_n_O ? H4). -Apply lt_n_S; Apply H. -Repeat Rewrite <- Rmult_assoc. -Rewrite <- Rinv_r_sym. -Rewrite Rmult_1l. -Replace ``(INR N)*(INR N)`` with (Rsqr (INR N)); [Idtac | Reflexivity]. -Rewrite Rmult_assoc. -Rewrite Rmult_sym. -Replace ``4`` with (Rsqr ``2``); [Idtac | SqRing]. -Rewrite <- Rsqr_times. -Apply Rsqr_incr_1. -Replace ``2`` with (INR (2)). -Rewrite <- mult_INR; Apply H1. -Reflexivity. -Left; Apply lt_INR_0; Apply H. -Left; Apply Rmult_lt_pos. -Sup0. -Apply lt_INR_0; Apply div2_not_R0. -Apply lt_n_S; Apply H. -Cut (lt (1) (S N)). -Intro; Unfold Rsqr; Apply prod_neq_R0; Apply not_O_INR; Intro; Assert H4 := (div2_not_R0 ? H2); Rewrite H3 in H4; Elim (lt_n_O ? H4). -Apply lt_n_S; Apply H. -Assert H1 := (even_odd_cor N). -Elim H1; Intros N0 H2. -Elim H2; Intro. -Pattern 2 N; Rewrite H3. -Rewrite div2_S_double. -Right; Rewrite H3; Reflexivity. -Pattern 2 N; Rewrite H3. -Replace (S (S (mult (2) N0))) with (mult (2) (S N0)). -Rewrite div2_double. -Rewrite H3. -Rewrite S_INR; Do 2 Rewrite mult_INR. -Rewrite (S_INR N0). -Rewrite Rmult_Rplus_distr. -Apply Rle_compatibility. -Rewrite Rmult_1r. -Simpl. -Pattern 1 R1; Rewrite <- Rplus_Or; Apply Rle_compatibility; Left; Apply Rlt_R0_R1. -Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring. -Unfold Rsqr; Apply prod_neq_R0; Apply INR_fact_neq_0. -Unfold Rsqr; Apply prod_neq_R0; Apply not_O_INR; Discriminate. -Assert H0 := (even_odd_cor N). -Elim H0; Intros N0 H1. -Elim H1; Intro. -Cut (lt O N0). -Intro; Rewrite H2. -Rewrite div2_S_double. -Replace (mult (2) N0) with (S (S (mult (2) (pred N0)))). -Replace (pred (S (S (mult (2) (pred N0))))) with (S (mult (2) (pred N0))). -Rewrite div2_S_double. -Apply S_pred with O; Apply H3. -Reflexivity. -Replace N0 with (S (pred N0)). -Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring. -Symmetry; Apply S_pred with O; Apply H3. -Rewrite H2 in H. -Apply neq_O_lt. -Red; Intro. -Rewrite <- H3 in H. -Simpl in H. -Elim (lt_n_O ? H). -Rewrite H2. -Replace (pred (S (mult (2) N0))) with (mult (2) N0); [Idtac | Reflexivity]. -Replace (S (S (mult (2) N0))) with (mult (2) (S N0)). -Do 2 Rewrite div2_double. -Reflexivity. -Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring. -Apply S_pred with O; Apply H. +Lemma Reste_E_maj : + forall (x y:R) (N:nat), + (0 < N)%nat -> Rabs (Reste_E x y N) <= maj_Reste_E x y N. +intros; pose (M := Rmax 1 (Rmax (Rabs x) (Rabs y))). +apply Rle_trans with + (M ^ (2 * N) * + sum_f_R0 + (fun k:nat => + sum_f_R0 (fun l:nat => / Rsqr (INR (fact (div2 (S N))))) + (pred (N - k))) (pred N)). +unfold Reste_E in |- *. +apply Rle_trans with + (sum_f_R0 + (fun k:nat => + Rabs + (sum_f_R0 + (fun l:nat => + / INR (fact (S (l + k))) * x ^ S (l + k) * + (/ INR (fact (N - l)) * y ^ (N - l))) ( + pred (N - k)))) (pred N)). +apply + (Rsum_abs + (fun k:nat => + sum_f_R0 + (fun l:nat => + / INR (fact (S (l + k))) * x ^ S (l + k) * + (/ INR (fact (N - l)) * y ^ (N - l))) ( + pred (N - k))) (pred N)). +apply Rle_trans with + (sum_f_R0 + (fun k:nat => + sum_f_R0 + (fun l:nat => + Rabs + (/ INR (fact (S (l + k))) * x ^ S (l + k) * + (/ INR (fact (N - l)) * y ^ (N - l)))) ( + pred (N - k))) (pred N)). +apply sum_Rle; intros. +apply + (Rsum_abs + (fun l:nat => + / INR (fact (S (l + n))) * x ^ S (l + n) * + (/ INR (fact (N - l)) * y ^ (N - l)))). +apply Rle_trans with + (sum_f_R0 + (fun k:nat => + sum_f_R0 + (fun l:nat => + M ^ (2 * N) * / INR (fact (S l)) * / INR (fact (N - l))) + (pred (N - k))) (pred N)). +apply sum_Rle; intros. +apply sum_Rle; intros. +repeat rewrite Rabs_mult. +do 2 rewrite <- RPow_abs. +rewrite (Rabs_right (/ INR (fact (S (n0 + n))))). +rewrite (Rabs_right (/ INR (fact (N - n0)))). +replace + (/ INR (fact (S (n0 + n))) * Rabs x ^ S (n0 + n) * + (/ INR (fact (N - n0)) * Rabs y ^ (N - n0))) with + (/ INR (fact (N - n0)) * / INR (fact (S (n0 + n))) * Rabs x ^ S (n0 + n) * + Rabs y ^ (N - n0)); [ idtac | ring ]. +rewrite <- (Rmult_comm (/ INR (fact (N - n0)))). +repeat rewrite Rmult_assoc. +apply Rmult_le_compat_l. +left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. +apply Rle_trans with + (/ INR (fact (S n0)) * Rabs x ^ S (n0 + n) * Rabs y ^ (N - n0)). +rewrite (Rmult_comm (/ INR (fact (S (n0 + n))))); + rewrite (Rmult_comm (/ INR (fact (S n0)))); repeat rewrite Rmult_assoc; + apply Rmult_le_compat_l. +apply pow_le; apply Rabs_pos. +rewrite (Rmult_comm (/ INR (fact (S n0)))); apply Rmult_le_compat_l. +apply pow_le; apply Rabs_pos. +apply Rle_Rinv. +apply INR_fact_lt_0. +apply INR_fact_lt_0. +apply le_INR; apply fact_le; apply le_n_S. +apply le_plus_l. +rewrite (Rmult_comm (M ^ (2 * N))); rewrite Rmult_assoc; + apply Rmult_le_compat_l. +left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. +apply Rle_trans with (M ^ S (n0 + n) * Rabs y ^ (N - n0)). +do 2 rewrite <- (Rmult_comm (Rabs y ^ (N - n0))). +apply Rmult_le_compat_l. +apply pow_le; apply Rabs_pos. +apply pow_incr; split. +apply Rabs_pos. +apply Rle_trans with (Rmax (Rabs x) (Rabs y)). +apply RmaxLess1. +unfold M in |- *; apply RmaxLess2. +apply Rle_trans with (M ^ S (n0 + n) * M ^ (N - n0)). +apply Rmult_le_compat_l. +apply pow_le; apply Rle_trans with 1. +left; apply Rlt_0_1. +unfold M in |- *; apply RmaxLess1. +apply pow_incr; split. +apply Rabs_pos. +apply Rle_trans with (Rmax (Rabs x) (Rabs y)). +apply RmaxLess2. +unfold M in |- *; apply RmaxLess2. +rewrite <- pow_add; replace (S (n0 + n) + (N - n0))%nat with (N + S n)%nat. +apply Rle_pow. +unfold M in |- *; apply RmaxLess1. +replace (2 * N)%nat with (N + N)%nat; [ idtac | ring ]. +apply plus_le_compat_l. +replace N with (S (pred N)). +apply le_n_S; apply H0. +symmetry in |- *; apply S_pred with 0%nat; apply H. +apply INR_eq; do 2 rewrite plus_INR; do 2 rewrite S_INR; rewrite plus_INR; + rewrite minus_INR. +ring. +apply le_trans with (pred (N - n)). +apply H1. +apply le_S_n. +replace (S (pred (N - n))) with (N - n)%nat. +apply le_trans with N. +apply (fun p n m:nat => plus_le_reg_l n m p) with n. +rewrite <- le_plus_minus. +apply le_plus_r. +apply le_trans with (pred N). +apply H0. +apply le_pred_n. +apply le_n_Sn. +apply S_pred with 0%nat. +apply plus_lt_reg_l with n. +rewrite <- le_plus_minus. +replace (n + 0)%nat with n; [ idtac | ring ]. +apply le_lt_trans with (pred N). +apply H0. +apply lt_pred_n_n. +apply H. +apply le_trans with (pred N). +apply H0. +apply le_pred_n. +apply Rle_ge; left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. +apply Rle_ge; left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. +rewrite scal_sum. +apply sum_Rle; intros. +rewrite <- Rmult_comm. +rewrite scal_sum. +apply sum_Rle; intros. +rewrite (Rmult_comm (/ Rsqr (INR (fact (div2 (S N)))))). +rewrite Rmult_assoc; apply Rmult_le_compat_l. +apply pow_le. +apply Rle_trans with 1. +left; apply Rlt_0_1. +unfold M in |- *; apply RmaxLess1. +assert (H2 := even_odd_cor N). +elim H2; intros N0 H3. +elim H3; intro. +apply Rle_trans with (/ INR (fact n0) * / INR (fact (N - n0))). +do 2 rewrite <- (Rmult_comm (/ INR (fact (N - n0)))). +apply Rmult_le_compat_l. +left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. +apply Rle_Rinv. +apply INR_fact_lt_0. +apply INR_fact_lt_0. +apply le_INR. +apply fact_le. +apply le_n_Sn. +replace (/ INR (fact n0) * / INR (fact (N - n0))) with + (C N n0 / INR (fact N)). +pattern N at 1 in |- *; rewrite H4. +apply Rle_trans with (C N N0 / INR (fact N)). +unfold Rdiv in |- *; do 2 rewrite <- (Rmult_comm (/ INR (fact N))). +apply Rmult_le_compat_l. +left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. +rewrite H4. +apply C_maj. +rewrite <- H4; apply le_trans with (pred (N - n)). +apply H1. +apply le_S_n. +replace (S (pred (N - n))) with (N - n)%nat. +apply le_trans with N. +apply (fun p n m:nat => plus_le_reg_l n m p) with n. +rewrite <- le_plus_minus. +apply le_plus_r. +apply le_trans with (pred N). +apply H0. +apply le_pred_n. +apply le_n_Sn. +apply S_pred with 0%nat. +apply plus_lt_reg_l with n. +rewrite <- le_plus_minus. +replace (n + 0)%nat with n; [ idtac | ring ]. +apply le_lt_trans with (pred N). +apply H0. +apply lt_pred_n_n. +apply H. +apply le_trans with (pred N). +apply H0. +apply le_pred_n. +replace (C N N0 / INR (fact N)) with (/ Rsqr (INR (fact N0))). +rewrite H4; rewrite div2_S_double; right; reflexivity. +unfold Rsqr, C, Rdiv in |- *. +repeat rewrite Rinv_mult_distr. +rewrite (Rmult_comm (INR (fact N))). +repeat rewrite Rmult_assoc. +rewrite <- Rinv_r_sym. +rewrite Rmult_1_r; replace (N - N0)%nat with N0. +ring. +replace N with (N0 + N0)%nat. +symmetry in |- *; apply minus_plus. +rewrite H4. +apply INR_eq; rewrite plus_INR; rewrite mult_INR; do 2 rewrite S_INR; ring. +apply INR_fact_neq_0. +apply INR_fact_neq_0. +apply INR_fact_neq_0. +apply INR_fact_neq_0. +apply INR_fact_neq_0. +unfold C, Rdiv in |- *. +rewrite (Rmult_comm (INR (fact N))). +repeat rewrite Rmult_assoc. +rewrite <- Rinv_r_sym. +rewrite Rinv_mult_distr. +rewrite Rmult_1_r; ring. +apply INR_fact_neq_0. +apply INR_fact_neq_0. +apply INR_fact_neq_0. +replace (/ INR (fact (S n0)) * / INR (fact (N - n0))) with + (C (S N) (S n0) / INR (fact (S N))). +apply Rle_trans with (C (S N) (S N0) / INR (fact (S N))). +unfold Rdiv in |- *; do 2 rewrite <- (Rmult_comm (/ INR (fact (S N)))). +apply Rmult_le_compat_l. +left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. +cut (S N = (2 * S N0)%nat). +intro; rewrite H5; apply C_maj. +rewrite <- H5; apply le_n_S. +apply le_trans with (pred (N - n)). +apply H1. +apply le_S_n. +replace (S (pred (N - n))) with (N - n)%nat. +apply le_trans with N. +apply (fun p n m:nat => plus_le_reg_l n m p) with n. +rewrite <- le_plus_minus. +apply le_plus_r. +apply le_trans with (pred N). +apply H0. +apply le_pred_n. +apply le_n_Sn. +apply S_pred with 0%nat. +apply plus_lt_reg_l with n. +rewrite <- le_plus_minus. +replace (n + 0)%nat with n; [ idtac | ring ]. +apply le_lt_trans with (pred N). +apply H0. +apply lt_pred_n_n. +apply H. +apply le_trans with (pred N). +apply H0. +apply le_pred_n. +apply INR_eq; rewrite H4. +do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR; ring. +cut (S N = (2 * S N0)%nat). +intro. +replace (C (S N) (S N0) / INR (fact (S N))) with (/ Rsqr (INR (fact (S N0)))). +rewrite H5; rewrite div2_double. +right; reflexivity. +unfold Rsqr, C, Rdiv in |- *. +repeat rewrite Rinv_mult_distr. +replace (S N - S N0)%nat with (S N0). +rewrite (Rmult_comm (INR (fact (S N)))). +repeat rewrite Rmult_assoc. +rewrite <- Rinv_r_sym. +rewrite Rmult_1_r; reflexivity. +apply INR_fact_neq_0. +replace (S N) with (S N0 + S N0)%nat. +symmetry in |- *; apply minus_plus. +rewrite H5; ring. +apply INR_fact_neq_0. +apply INR_fact_neq_0. +apply INR_fact_neq_0. +apply INR_fact_neq_0. +apply INR_eq; rewrite H4; do 2 rewrite S_INR; do 2 rewrite mult_INR; + repeat rewrite S_INR; ring. +unfold C, Rdiv in |- *. +rewrite (Rmult_comm (INR (fact (S N)))). +rewrite Rmult_assoc; rewrite <- Rinv_r_sym. +rewrite Rmult_1_r; rewrite Rinv_mult_distr. +reflexivity. +apply INR_fact_neq_0. +apply INR_fact_neq_0. +apply INR_fact_neq_0. +unfold maj_Reste_E in |- *. +unfold Rdiv in |- *; rewrite (Rmult_comm 4). +rewrite Rmult_assoc. +apply Rmult_le_compat_l. +apply pow_le. +apply Rle_trans with 1. +left; apply Rlt_0_1. +apply RmaxLess1. +apply Rle_trans with + (sum_f_R0 (fun k:nat => INR (N - k) * / Rsqr (INR (fact (div2 (S N))))) + (pred N)). +apply sum_Rle; intros. +rewrite sum_cte. +replace (S (pred (N - n))) with (N - n)%nat. +right; apply Rmult_comm. +apply S_pred with 0%nat. +apply plus_lt_reg_l with n. +rewrite <- le_plus_minus. +replace (n + 0)%nat with n; [ idtac | ring ]. +apply le_lt_trans with (pred N). +apply H0. +apply lt_pred_n_n. +apply H. +apply le_trans with (pred N). +apply H0. +apply le_pred_n. +apply Rle_trans with + (sum_f_R0 (fun k:nat => INR N * / Rsqr (INR (fact (div2 (S N))))) (pred N)). +apply sum_Rle; intros. +do 2 rewrite <- (Rmult_comm (/ Rsqr (INR (fact (div2 (S N)))))). +apply Rmult_le_compat_l. +left; apply Rinv_0_lt_compat; apply Rsqr_pos_lt. +apply INR_fact_neq_0. +apply le_INR. +apply (fun p n m:nat => plus_le_reg_l n m p) with n. +rewrite <- le_plus_minus. +apply le_plus_r. +apply le_trans with (pred N). +apply H0. +apply le_pred_n. +rewrite sum_cte; replace (S (pred N)) with N. +cut (div2 (S N) = S (div2 (pred N))). +intro; rewrite H0. +rewrite fact_simpl; rewrite mult_comm; rewrite mult_INR; rewrite Rsqr_mult. +rewrite Rinv_mult_distr. +rewrite (Rmult_comm (INR N)); repeat rewrite Rmult_assoc; + apply Rmult_le_compat_l. +left; apply Rinv_0_lt_compat; apply Rsqr_pos_lt; apply INR_fact_neq_0. +rewrite <- H0. +cut (INR N <= INR (2 * div2 (S N))). +intro; apply Rmult_le_reg_l with (Rsqr (INR (div2 (S N)))). +apply Rsqr_pos_lt. +apply not_O_INR; red in |- *; intro. +cut (1 < S N)%nat. +intro; assert (H4 := div2_not_R0 _ H3). +rewrite H2 in H4; elim (lt_n_O _ H4). +apply lt_n_S; apply H. +repeat rewrite <- Rmult_assoc. +rewrite <- Rinv_r_sym. +rewrite Rmult_1_l. +replace (INR N * INR N) with (Rsqr (INR N)); [ idtac | reflexivity ]. +rewrite Rmult_assoc. +rewrite Rmult_comm. +replace 4 with (Rsqr 2); [ idtac | ring_Rsqr ]. +rewrite <- Rsqr_mult. +apply Rsqr_incr_1. +replace 2 with (INR 2). +rewrite <- mult_INR; apply H1. +reflexivity. +left; apply lt_INR_0; apply H. +left; apply Rmult_lt_0_compat. +prove_sup0. +apply lt_INR_0; apply div2_not_R0. +apply lt_n_S; apply H. +cut (1 < S N)%nat. +intro; unfold Rsqr in |- *; apply prod_neq_R0; apply not_O_INR; intro; + assert (H4 := div2_not_R0 _ H2); rewrite H3 in H4; + elim (lt_n_O _ H4). +apply lt_n_S; apply H. +assert (H1 := even_odd_cor N). +elim H1; intros N0 H2. +elim H2; intro. +pattern N at 2 in |- *; rewrite H3. +rewrite div2_S_double. +right; rewrite H3; reflexivity. +pattern N at 2 in |- *; rewrite H3. +replace (S (S (2 * N0))) with (2 * S N0)%nat. +rewrite div2_double. +rewrite H3. +rewrite S_INR; do 2 rewrite mult_INR. +rewrite (S_INR N0). +rewrite Rmult_plus_distr_l. +apply Rplus_le_compat_l. +rewrite Rmult_1_r. +simpl in |- *. +pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left; + apply Rlt_0_1. +apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR; + ring. +unfold Rsqr in |- *; apply prod_neq_R0; apply INR_fact_neq_0. +unfold Rsqr in |- *; apply prod_neq_R0; apply not_O_INR; discriminate. +assert (H0 := even_odd_cor N). +elim H0; intros N0 H1. +elim H1; intro. +cut (0 < N0)%nat. +intro; rewrite H2. +rewrite div2_S_double. +replace (2 * N0)%nat with (S (S (2 * pred N0))). +replace (pred (S (S (2 * pred N0)))) with (S (2 * pred N0)). +rewrite div2_S_double. +apply S_pred with 0%nat; apply H3. +reflexivity. +replace N0 with (S (pred N0)). +apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR; + ring. +symmetry in |- *; apply S_pred with 0%nat; apply H3. +rewrite H2 in H. +apply neq_O_lt. +red in |- *; intro. +rewrite <- H3 in H. +simpl in H. +elim (lt_n_O _ H). +rewrite H2. +replace (pred (S (2 * N0))) with (2 * N0)%nat; [ idtac | reflexivity ]. +replace (S (S (2 * N0))) with (2 * S N0)%nat. +do 2 rewrite div2_double. +reflexivity. +apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR; + ring. +apply S_pred with 0%nat; apply H. Qed. -Lemma maj_Reste_cv_R0 : (x,y:R) (Un_cv (maj_Reste_E x y) ``0``). -Intros; Assert H := (Majxy_cv_R0 x y). -Unfold Un_cv in H; Unfold Un_cv; Intros. -Cut ``0<eps/4``; [Intro | Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0]]. -Elim (H ? H1); Intros N0 H2. -Exists (max (mult (2) (S N0)) (2)); Intros. -Unfold R_dist in H2; Unfold R_dist; Rewrite minus_R0; Unfold Majxy in H2; Unfold maj_Reste_E. -Rewrite Rabsolu_right. -Apply Rle_lt_trans with ``4*(pow (Rmax 1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (S (S (S (S O)))) (S (div2 (pred n)))))/(INR (fact (div2 (pred n))))``. -Apply Rle_monotony. -Left; Sup0. -Unfold Rdiv Rsqr; Rewrite Rinv_Rmult. -Rewrite (Rmult_sym ``(pow (Rmax 1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (S (S O)) n))``); Rewrite (Rmult_sym ``(pow (Rmax 1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (S (S (S (S O)))) (S (div2 (pred n)))))``); Rewrite Rmult_assoc; Apply Rle_monotony. -Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. -Apply Rle_trans with ``(pow (Rmax 1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (S (S O)) n))``. -Rewrite Rmult_sym; Pattern 2 (pow (Rmax R1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (2) n)); Rewrite <- Rmult_1r; Apply Rle_monotony. -Apply pow_le; Apply Rle_trans with R1. -Left; Apply Rlt_R0_R1. -Apply RmaxLess1. -Apply Rle_monotony_contra with ``(INR (fact (div2 (pred n))))``. -Apply INR_fact_lt_0. -Rewrite Rmult_1r; Rewrite <- Rinv_r_sym. -Replace R1 with (INR (1)); [Apply le_INR | Reflexivity]. -Apply lt_le_S. -Apply INR_lt. -Apply INR_fact_lt_0. -Apply INR_fact_neq_0. -Apply Rle_pow. -Apply RmaxLess1. -Assert H4 := (even_odd_cor n). -Elim H4; Intros N1 H5. -Elim H5; Intro. -Cut (lt O N1). -Intro. -Rewrite H6. -Replace (pred (mult (2) N1)) with (S (mult (2) (pred N1))). -Rewrite div2_S_double. -Replace (S (pred N1)) with N1. -Apply INR_le. -Right. -Do 3 Rewrite mult_INR; Repeat Rewrite S_INR; Ring. -Apply S_pred with O; Apply H7. -Replace (mult (2) N1) with (S (S (mult (2) (pred N1)))). -Reflexivity. -Pattern 2 N1; Replace N1 with (S (pred N1)). -Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring. -Symmetry ; Apply S_pred with O; Apply H7. -Apply INR_lt. -Apply Rlt_monotony_contra with (INR (2)). -Simpl; Sup0. -Rewrite Rmult_Or; Rewrite <- mult_INR. -Apply lt_INR_0. -Rewrite <- H6. -Apply lt_le_trans with (2). -Apply lt_O_Sn. -Apply le_trans with (max (mult (2) (S N0)) (2)). -Apply le_max_r. -Apply H3. -Rewrite H6. -Replace (pred (S (mult (2) N1))) with (mult (2) N1). -Rewrite div2_double. -Replace (mult (4) (S N1)) with (mult (2) (mult (2) (S N1))). -Apply mult_le. -Replace (mult (2) (S N1)) with (S (S (mult (2) N1))). -Apply le_n_Sn. -Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring. -Ring. -Reflexivity. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Apply Rlt_monotony_contra with ``/4``. -Apply Rlt_Rinv; Sup0. -Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1l; Rewrite Rmult_sym. -Replace ``(pow (Rmax 1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (S (S (S (S O)))) (S (div2 (pred n)))))/(INR (fact (div2 (pred n))))`` with ``(Rabsolu ((pow (Rmax 1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (S (S (S (S O)))) (S (div2 (pred n)))))/(INR (fact (div2 (pred n))))-0))``. -Apply H2; Unfold ge. -Cut (le (mult (2) (S N0)) n). -Intro; Apply le_S_n. -Apply INR_le; Apply Rle_monotony_contra with (INR (2)). -Simpl; Sup0. -Do 2 Rewrite <- mult_INR; Apply le_INR. -Apply le_trans with n. -Apply H4. -Assert H5 := (even_odd_cor n). -Elim H5; Intros N1 H6. -Elim H6; Intro. -Cut (lt O N1). -Intro. -Rewrite H7. -Apply mult_le. -Replace (pred (mult (2) N1)) with (S (mult (2) (pred N1))). -Rewrite div2_S_double. -Replace (S (pred N1)) with N1. -Apply le_n. -Apply S_pred with O; Apply H8. -Replace (mult (2) N1) with (S (S (mult (2) (pred N1)))). -Reflexivity. -Pattern 2 N1; Replace N1 with (S (pred N1)). -Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring. -Symmetry; Apply S_pred with O; Apply H8. -Apply INR_lt. -Apply Rlt_monotony_contra with (INR (2)). -Simpl; Sup0. -Rewrite Rmult_Or; Rewrite <- mult_INR. -Apply lt_INR_0. -Rewrite <- H7. -Apply lt_le_trans with (2). -Apply lt_O_Sn. -Apply le_trans with (max (mult (2) (S N0)) (2)). -Apply le_max_r. -Apply H3. -Rewrite H7. -Replace (pred (S (mult (2) N1))) with (mult (2) N1). -Rewrite div2_double. -Replace (mult (2) (S N1)) with (S (S (mult (2) N1))). -Apply le_n_Sn. -Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring. -Reflexivity. -Apply le_trans with (max (mult (2) (S N0)) (2)). -Apply le_max_l. -Apply H3. -Rewrite minus_R0; Apply Rabsolu_right. -Apply Rle_sym1. -Unfold Rdiv; Repeat Apply Rmult_le_pos. -Apply pow_le. -Apply Rle_trans with R1. -Left; Apply Rlt_R0_R1. -Apply RmaxLess1. -Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. -DiscrR. -Apply Rle_sym1. -Unfold Rdiv; Apply Rmult_le_pos. -Left; Sup0. -Apply Rmult_le_pos. -Apply pow_le. -Apply Rle_trans with R1. -Left; Apply Rlt_R0_R1. -Apply RmaxLess1. -Left; Apply Rlt_Rinv; Apply Rsqr_pos_lt; Apply INR_fact_neq_0. +Lemma maj_Reste_cv_R0 : forall x y:R, Un_cv (maj_Reste_E x y) 0. +intros; assert (H := Majxy_cv_R0 x y). +unfold Un_cv in H; unfold Un_cv in |- *; intros. +cut (0 < eps / 4); + [ intro + | unfold Rdiv in |- *; apply Rmult_lt_0_compat; + [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. +elim (H _ H1); intros N0 H2. +exists (max (2 * S N0) 2); intros. +unfold R_dist in H2; unfold R_dist in |- *; rewrite Rminus_0_r; + unfold Majxy in H2; unfold maj_Reste_E in |- *. +rewrite Rabs_right. +apply Rle_lt_trans with + (4 * + (Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (4 * S (div2 (pred n))) / + INR (fact (div2 (pred n))))). +apply Rmult_le_compat_l. +left; prove_sup0. +unfold Rdiv, Rsqr in |- *; rewrite Rinv_mult_distr. +rewrite (Rmult_comm (Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (2 * n))); + rewrite + (Rmult_comm (Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (4 * S (div2 (pred n))))) + ; rewrite Rmult_assoc; apply Rmult_le_compat_l. +left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. +apply Rle_trans with (Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (2 * n)). +rewrite Rmult_comm; + pattern (Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (2 * n)) at 2 in |- *; + rewrite <- Rmult_1_r; apply Rmult_le_compat_l. +apply pow_le; apply Rle_trans with 1. +left; apply Rlt_0_1. +apply RmaxLess1. +apply Rmult_le_reg_l with (INR (fact (div2 (pred n)))). +apply INR_fact_lt_0. +rewrite Rmult_1_r; rewrite <- Rinv_r_sym. +replace 1 with (INR 1); [ apply le_INR | reflexivity ]. +apply lt_le_S. +apply INR_lt. +apply INR_fact_lt_0. +apply INR_fact_neq_0. +apply Rle_pow. +apply RmaxLess1. +assert (H4 := even_odd_cor n). +elim H4; intros N1 H5. +elim H5; intro. +cut (0 < N1)%nat. +intro. +rewrite H6. +replace (pred (2 * N1)) with (S (2 * pred N1)). +rewrite div2_S_double. +replace (S (pred N1)) with N1. +apply INR_le. +right. +do 3 rewrite mult_INR; repeat rewrite S_INR; ring. +apply S_pred with 0%nat; apply H7. +replace (2 * N1)%nat with (S (S (2 * pred N1))). +reflexivity. +pattern N1 at 2 in |- *; replace N1 with (S (pred N1)). +apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR; + ring. +symmetry in |- *; apply S_pred with 0%nat; apply H7. +apply INR_lt. +apply Rmult_lt_reg_l with (INR 2). +simpl in |- *; prove_sup0. +rewrite Rmult_0_r; rewrite <- mult_INR. +apply lt_INR_0. +rewrite <- H6. +apply lt_le_trans with 2%nat. +apply lt_O_Sn. +apply le_trans with (max (2 * S N0) 2). +apply le_max_r. +apply H3. +rewrite H6. +replace (pred (S (2 * N1))) with (2 * N1)%nat. +rewrite div2_double. +replace (4 * S N1)%nat with (2 * (2 * S N1))%nat. +apply (fun m n p:nat => mult_le_compat_l p n m). +replace (2 * S N1)%nat with (S (S (2 * N1))). +apply le_n_Sn. +apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR; + ring. +ring. +reflexivity. +apply INR_fact_neq_0. +apply INR_fact_neq_0. +apply Rmult_lt_reg_l with (/ 4). +apply Rinv_0_lt_compat; prove_sup0. +rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. +rewrite Rmult_1_l; rewrite Rmult_comm. +replace + (Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (4 * S (div2 (pred n))) / + INR (fact (div2 (pred n)))) with + (Rabs + (Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (4 * S (div2 (pred n))) / + INR (fact (div2 (pred n))) - 0)). +apply H2; unfold ge in |- *. +cut (2 * S N0 <= n)%nat. +intro; apply le_S_n. +apply INR_le; apply Rmult_le_reg_l with (INR 2). +simpl in |- *; prove_sup0. +do 2 rewrite <- mult_INR; apply le_INR. +apply le_trans with n. +apply H4. +assert (H5 := even_odd_cor n). +elim H5; intros N1 H6. +elim H6; intro. +cut (0 < N1)%nat. +intro. +rewrite H7. +apply (fun m n p:nat => mult_le_compat_l p n m). +replace (pred (2 * N1)) with (S (2 * pred N1)). +rewrite div2_S_double. +replace (S (pred N1)) with N1. +apply le_n. +apply S_pred with 0%nat; apply H8. +replace (2 * N1)%nat with (S (S (2 * pred N1))). +reflexivity. +pattern N1 at 2 in |- *; replace N1 with (S (pred N1)). +apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR; + ring. +symmetry in |- *; apply S_pred with 0%nat; apply H8. +apply INR_lt. +apply Rmult_lt_reg_l with (INR 2). +simpl in |- *; prove_sup0. +rewrite Rmult_0_r; rewrite <- mult_INR. +apply lt_INR_0. +rewrite <- H7. +apply lt_le_trans with 2%nat. +apply lt_O_Sn. +apply le_trans with (max (2 * S N0) 2). +apply le_max_r. +apply H3. +rewrite H7. +replace (pred (S (2 * N1))) with (2 * N1)%nat. +rewrite div2_double. +replace (2 * S N1)%nat with (S (S (2 * N1))). +apply le_n_Sn. +apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR; + ring. +reflexivity. +apply le_trans with (max (2 * S N0) 2). +apply le_max_l. +apply H3. +rewrite Rminus_0_r; apply Rabs_right. +apply Rle_ge. +unfold Rdiv in |- *; repeat apply Rmult_le_pos. +apply pow_le. +apply Rle_trans with 1. +left; apply Rlt_0_1. +apply RmaxLess1. +left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. +discrR. +apply Rle_ge. +unfold Rdiv in |- *; apply Rmult_le_pos. +left; prove_sup0. +apply Rmult_le_pos. +apply pow_le. +apply Rle_trans with 1. +left; apply Rlt_0_1. +apply RmaxLess1. +left; apply Rinv_0_lt_compat; apply Rsqr_pos_lt; apply INR_fact_neq_0. Qed. (**********) -Lemma Reste_E_cv : (x,y:R) (Un_cv (Reste_E x y) R0). -Intros; Assert H := (maj_Reste_cv_R0 x y). -Unfold Un_cv in H; Unfold Un_cv; Intros; Elim (H ? H0); Intros. -Exists (max x0 (1)); Intros. -Unfold R_dist; Rewrite minus_R0. -Apply Rle_lt_trans with (maj_Reste_E x y n). -Apply Reste_E_maj. -Apply lt_le_trans with (1). -Apply lt_O_Sn. -Apply le_trans with (max x0 (1)). -Apply le_max_r. -Apply H2. -Replace (maj_Reste_E x y n) with (R_dist (maj_Reste_E x y n) R0). -Apply H1. -Unfold ge; Apply le_trans with (max x0 (1)). -Apply le_max_l. -Apply H2. -Unfold R_dist; Rewrite minus_R0; Apply Rabsolu_right. -Apply Rle_sym1; Apply Rle_trans with (Rabsolu (Reste_E x y n)). -Apply Rabsolu_pos. -Apply Reste_E_maj. -Apply lt_le_trans with (1). -Apply lt_O_Sn. -Apply le_trans with (max x0 (1)). -Apply le_max_r. -Apply H2. +Lemma Reste_E_cv : forall x y:R, Un_cv (Reste_E x y) 0. +intros; assert (H := maj_Reste_cv_R0 x y). +unfold Un_cv in H; unfold Un_cv in |- *; intros; elim (H _ H0); intros. +exists (max x0 1); intros. +unfold R_dist in |- *; rewrite Rminus_0_r. +apply Rle_lt_trans with (maj_Reste_E x y n). +apply Reste_E_maj. +apply lt_le_trans with 1%nat. +apply lt_O_Sn. +apply le_trans with (max x0 1). +apply le_max_r. +apply H2. +replace (maj_Reste_E x y n) with (R_dist (maj_Reste_E x y n) 0). +apply H1. +unfold ge in |- *; apply le_trans with (max x0 1). +apply le_max_l. +apply H2. +unfold R_dist in |- *; rewrite Rminus_0_r; apply Rabs_right. +apply Rle_ge; apply Rle_trans with (Rabs (Reste_E x y n)). +apply Rabs_pos. +apply Reste_E_maj. +apply lt_le_trans with 1%nat. +apply lt_O_Sn. +apply le_trans with (max x0 1). +apply le_max_r. +apply H2. Qed. (**********) -Lemma exp_plus : (x,y:R) ``(exp (x+y))==(exp x)*(exp y)``. -Intros; Assert H0 := (E1_cvg x). -Assert H := (E1_cvg y). -Assert H1 := (E1_cvg ``x+y``). -EApply UL_sequence. -Apply H1. -Assert H2 := (CV_mult ? ? ? ? H0 H). -Assert H3 := (CV_minus ? ? ? ? H2 (Reste_E_cv x y)). -Unfold Un_cv; Unfold Un_cv in H3; Intros. -Elim (H3 ? H4); Intros. -Exists (S x0); Intros. -Rewrite <- (exp_form x y n). -Rewrite minus_R0 in H5. -Apply H5. -Unfold ge; Apply le_trans with (S x0). -Apply le_n_Sn. -Apply H6. -Apply lt_le_trans with (S x0). -Apply lt_O_Sn. -Apply H6. +Lemma exp_plus : forall x y:R, exp (x + y) = exp x * exp y. +intros; assert (H0 := E1_cvg x). +assert (H := E1_cvg y). +assert (H1 := E1_cvg (x + y)). +eapply UL_sequence. +apply H1. +assert (H2 := CV_mult _ _ _ _ H0 H). +assert (H3 := CV_minus _ _ _ _ H2 (Reste_E_cv x y)). +unfold Un_cv in |- *; unfold Un_cv in H3; intros. +elim (H3 _ H4); intros. +exists (S x0); intros. +rewrite <- (exp_form x y n). +rewrite Rminus_0_r in H5. +apply H5. +unfold ge in |- *; apply le_trans with (S x0). +apply le_n_Sn. +apply H6. +apply lt_le_trans with (S x0). +apply lt_O_Sn. +apply H6. Qed. (**********) -Lemma exp_pos_pos : (x:R) ``0<x`` -> ``0<(exp x)``. -Intros; Pose An := [N:nat]``/(INR (fact N))*(pow x N)``. -Cut (Un_cv [n:nat](sum_f_R0 An n) (exp x)). -Intro; Apply Rlt_le_trans with (sum_f_R0 An O). -Unfold An; Simpl; Rewrite Rinv_R1; Rewrite Rmult_1r; Apply Rlt_R0_R1. -Apply sum_incr. -Assumption. -Intro; Unfold An; Left; Apply Rmult_lt_pos. -Apply Rlt_Rinv; Apply INR_fact_lt_0. -Apply (pow_lt ? n H). -Unfold exp; Unfold projT1; Case (exist_exp x); Intro. -Unfold exp_in; Unfold infinit_sum Un_cv; Trivial. +Lemma exp_pos_pos : forall x:R, 0 < x -> 0 < exp x. +intros; pose (An := fun N:nat => / INR (fact N) * x ^ N). +cut (Un_cv (fun n:nat => sum_f_R0 An n) (exp x)). +intro; apply Rlt_le_trans with (sum_f_R0 An 0). +unfold An in |- *; simpl in |- *; rewrite Rinv_1; rewrite Rmult_1_r; + apply Rlt_0_1. +apply sum_incr. +assumption. +intro; unfold An in |- *; left; apply Rmult_lt_0_compat. +apply Rinv_0_lt_compat; apply INR_fact_lt_0. +apply (pow_lt _ n H). +unfold exp in |- *; unfold projT1 in |- *; case (exist_exp x); intro. +unfold exp_in in |- *; unfold infinit_sum, Un_cv in |- *; trivial. Qed. (**********) -Lemma exp_pos : (x:R) ``0<(exp x)``. -Intro; Case (total_order_T R0 x); Intro. -Elim s; Intro. -Apply (exp_pos_pos ? a). -Rewrite <- b; Rewrite exp_0; Apply Rlt_R0_R1. -Replace (exp x) with ``1/(exp (-x))``. -Unfold Rdiv; Apply Rmult_lt_pos. -Apply Rlt_R0_R1. -Apply Rlt_Rinv; Apply exp_pos_pos. -Apply (Rgt_RO_Ropp ? r). -Cut ``(exp (-x))<>0``. -Intro; Unfold Rdiv; Apply r_Rmult_mult with ``(exp (-x))``. -Rewrite Rmult_1l; Rewrite <- Rinv_r_sym. -Rewrite <- exp_plus. -Rewrite Rplus_Ropp_l; Rewrite exp_0; Reflexivity. -Apply H. -Apply H. -Assert H := (exp_plus x ``-x``). -Rewrite Rplus_Ropp_r in H; Rewrite exp_0 in H. -Red; Intro; Rewrite H0 in H. -Rewrite Rmult_Or in H. -Elim R1_neq_R0; Assumption. +Lemma exp_pos : forall x:R, 0 < exp x. +intro; case (total_order_T 0 x); intro. +elim s; intro. +apply (exp_pos_pos _ a). +rewrite <- b; rewrite exp_0; apply Rlt_0_1. +replace (exp x) with (1 / exp (- x)). +unfold Rdiv in |- *; apply Rmult_lt_0_compat. +apply Rlt_0_1. +apply Rinv_0_lt_compat; apply exp_pos_pos. +apply (Ropp_0_gt_lt_contravar _ r). +cut (exp (- x) <> 0). +intro; unfold Rdiv in |- *; apply Rmult_eq_reg_l with (exp (- x)). +rewrite Rmult_1_l; rewrite <- Rinv_r_sym. +rewrite <- exp_plus. +rewrite Rplus_opp_l; rewrite exp_0; reflexivity. +apply H. +apply H. +assert (H := exp_plus x (- x)). +rewrite Rplus_opp_r in H; rewrite exp_0 in H. +red in |- *; intro; rewrite H0 in H. +rewrite Rmult_0_r in H. +elim R1_neq_R0; assumption. Qed. (* ((exp h)-1)/h -> 0 quand h->0 *) -Lemma derivable_pt_lim_exp_0 : (derivable_pt_lim exp ``0`` ``1``). -Unfold derivable_pt_lim; Intros. -Pose fn := [N:nat][x:R]``(pow x N)/(INR (fact (S N)))``. -Cut (CVN_R fn). -Intro; Cut (x:R)(sigTT ? [l:R](Un_cv [N:nat](SP fn N x) l)). -Intro cv; Cut ((n:nat)(continuity (fn n))). -Intro; Cut (continuity (SFL fn cv)). -Intro; Unfold continuity in H1. -Assert H2 := (H1 R0). -Unfold continuity_pt in H2; Unfold continue_in in H2; Unfold limit1_in in H2; Unfold limit_in in H2; Simpl in H2; Unfold R_dist in H2. -Elim (H2 ? H); Intros alp H3. -Elim H3; Intros. -Exists (mkposreal ? H4); Intros. -Rewrite Rplus_Ol; Rewrite exp_0. -Replace ``((exp h)-1)/h`` with (SFL fn cv h). -Replace R1 with (SFL fn cv R0). -Apply H5. -Split. -Unfold D_x no_cond; Split. -Trivial. -Apply (not_sym ? ? H6). -Rewrite minus_R0; Apply H7. -Unfold SFL. -Case (cv ``0``); Intros. -EApply UL_sequence. -Apply u. -Unfold Un_cv SP. -Intros; Exists (1); Intros. -Unfold R_dist; Rewrite decomp_sum. -Rewrite (Rplus_sym (fn O R0)). -Replace (fn O R0) with R1. -Unfold Rminus; Rewrite Rplus_assoc; Rewrite Rplus_Ropp_r; Rewrite Rplus_Or. -Replace (sum_f_R0 [i:nat](fn (S i) ``0``) (pred n)) with R0. -Rewrite Rabsolu_R0; Apply H8. -Symmetry; Apply sum_eq_R0; Intros. -Unfold fn. -Simpl. -Unfold Rdiv; Do 2 Rewrite Rmult_Ol; Reflexivity. -Unfold fn; Simpl. -Unfold Rdiv; Rewrite Rinv_R1; Rewrite Rmult_1r; Reflexivity. -Apply lt_le_trans with (1); [Apply lt_n_Sn | Apply H9]. -Unfold SFL exp. -Unfold projT1. -Case (cv h); Case (exist_exp h); Intros. -EApply UL_sequence. -Apply u. -Unfold Un_cv; Intros. -Unfold exp_in in e. -Unfold infinit_sum in e. -Cut ``0<eps0*(Rabsolu h)``. -Intro; Elim (e ? H9); Intros N0 H10. -Exists N0; Intros. -Unfold R_dist. -Apply Rlt_monotony_contra with ``(Rabsolu h)``. -Apply Rabsolu_pos_lt; Assumption. -Rewrite <- Rabsolu_mult. -Rewrite Rminus_distr. -Replace ``h*(x-1)/h`` with ``(x-1)``. -Unfold R_dist in H10. -Replace ``h*(SP fn n h)-(x-1)`` with (Rminus (sum_f_R0 [i:nat]``/(INR (fact i))*(pow h i)`` (S n)) x). -Rewrite (Rmult_sym (Rabsolu h)). -Apply H10. -Unfold ge. -Apply le_trans with (S N0). -Apply le_n_Sn. -Apply le_n_S; Apply H11. -Rewrite decomp_sum. -Replace ``/(INR (fact O))*(pow h O)`` with R1. -Unfold Rminus. -Rewrite Ropp_distr1. -Rewrite Ropp_Ropp. -Rewrite <- (Rplus_sym ``-x``). -Rewrite <- (Rplus_sym ``-x+1``). -Rewrite Rplus_assoc; Repeat Apply Rplus_plus_r. -Replace (pred (S n)) with n; [Idtac | Reflexivity]. -Unfold SP. -Rewrite scal_sum. -Apply sum_eq; Intros. -Unfold fn. -Replace (pow h (S i)) with ``h*(pow h i)``. -Unfold Rdiv; Ring. -Simpl; Ring. -Simpl; Rewrite Rinv_R1; Rewrite Rmult_1r; Reflexivity. -Apply lt_O_Sn. -Unfold Rdiv. -Rewrite <- Rmult_assoc. -Symmetry; Apply Rinv_r_simpl_m. -Assumption. -Apply Rmult_lt_pos. -Apply H8. -Apply Rabsolu_pos_lt; Assumption. -Apply SFL_continuity; Assumption. -Intro; Unfold fn. -Replace [x:R]``(pow x n)/(INR (fact (S n)))`` with (div_fct (pow_fct n) (fct_cte (INR (fact (S n))))); [Idtac | Reflexivity]. -Apply continuity_div. -Apply derivable_continuous; Apply (derivable_pow n). -Apply derivable_continuous; Apply derivable_const. -Intro; Unfold fct_cte; Apply INR_fact_neq_0. -Apply (CVN_R_CVS ? X). -Assert H0 := Alembert_exp. -Unfold CVN_R. -Intro; Unfold CVN_r. -Apply Specif.existT with [N:nat]``(pow r N)/(INR (fact (S N)))``. -Cut (SigT ? [l:R](Un_cv [n:nat](sum_f_R0 [k:nat](Rabsolu ``(pow r k)/(INR (fact (S k)))``) n) l)). -Intro. -Elim X; Intros. -Exists x; Intros. -Split. -Apply p. -Unfold Boule; Intros. -Rewrite minus_R0 in H1. -Unfold fn. -Unfold Rdiv; Rewrite Rabsolu_mult. -Cut ``0<(INR (fact (S n)))``. -Intro. -Rewrite (Rabsolu_right ``/(INR (fact (S n)))``). -Do 2 Rewrite <- (Rmult_sym ``/(INR (fact (S n)))``). -Apply Rle_monotony. -Left; Apply Rlt_Rinv; Apply H2. -Rewrite <- Pow_Rabsolu. -Apply pow_maj_Rabs. -Rewrite Rabsolu_Rabsolu; Left; Apply H1. -Apply Rle_sym1; Left; Apply Rlt_Rinv; Apply H2. -Apply INR_fact_lt_0. -Cut (r::R)<>``0``. -Intro; Apply Alembert_C2. -Intro; Apply Rabsolu_no_R0. -Unfold Rdiv; Apply prod_neq_R0. -Apply pow_nonzero; Assumption. -Apply Rinv_neq_R0; Apply INR_fact_neq_0. -Unfold Un_cv in H0. -Unfold Un_cv; Intros. -Cut ``0<eps0/r``; [Intro | Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply (cond_pos r)]]. -Elim (H0 ? H3); Intros N0 H4. -Exists N0; Intros. -Cut (ge (S n) N0). -Intro hyp_sn. -Assert H6 := (H4 ? hyp_sn). -Unfold R_dist in H6; Rewrite minus_R0 in H6. -Rewrite Rabsolu_Rabsolu in H6. -Unfold R_dist; Rewrite minus_R0. -Rewrite Rabsolu_Rabsolu. -Replace ``(Rabsolu ((pow r (S n))/(INR (fact (S (S n))))))/ - (Rabsolu ((pow r n)/(INR (fact (S n)))))`` with ``r*/(INR (fact (S (S n))))*//(INR (fact (S n)))``. -Rewrite Rmult_assoc; Rewrite Rabsolu_mult. -Rewrite (Rabsolu_right r). -Apply Rlt_monotony_contra with ``/r``. -Apply Rlt_Rinv; Apply (cond_pos r). -Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1l; Rewrite <- (Rmult_sym eps0). -Apply H6. -Assumption. -Apply Rle_sym1; Left; Apply (cond_pos r). -Unfold Rdiv. -Repeat Rewrite Rabsolu_mult. -Repeat Rewrite Rabsolu_Rinv. -Rewrite Rinv_Rmult. -Repeat Rewrite Rabsolu_right. -Rewrite Rinv_Rinv. -Rewrite (Rmult_sym r). -Rewrite (Rmult_sym (pow r (S n))). -Repeat Rewrite Rmult_assoc. -Apply Rmult_mult_r. -Rewrite (Rmult_sym r). -Rewrite <- Rmult_assoc; Rewrite <- (Rmult_sym (INR (fact (S n)))). -Apply Rmult_mult_r. -Simpl. -Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym. -Ring. -Apply pow_nonzero; Assumption. -Apply INR_fact_neq_0. -Apply Rle_sym1; Left; Apply INR_fact_lt_0. -Apply Rle_sym1; Left; Apply pow_lt; Apply (cond_pos r). -Apply Rle_sym1; Left; Apply INR_fact_lt_0. -Apply Rle_sym1; Left; Apply pow_lt; Apply (cond_pos r). -Apply Rabsolu_no_R0; Apply pow_nonzero; Assumption. -Apply Rinv_neq_R0; Apply Rabsolu_no_R0; Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Unfold ge; Apply le_trans with n. -Apply H5. -Apply le_n_Sn. -Assert H1 := (cond_pos r); Red; Intro; Rewrite H2 in H1; Elim (Rlt_antirefl ? H1). +Lemma derivable_pt_lim_exp_0 : derivable_pt_lim exp 0 1. +unfold derivable_pt_lim in |- *; intros. +pose (fn := fun (N:nat) (x:R) => x ^ N / INR (fact (S N))). +cut (CVN_R fn). +intro; cut (forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l)). +intro cv; cut (forall n:nat, continuity (fn n)). +intro; cut (continuity (SFL fn cv)). +intro; unfold continuity in H1. +assert (H2 := H1 0). +unfold continuity_pt in H2; unfold continue_in in H2; unfold limit1_in in H2; + unfold limit_in in H2; simpl in H2; unfold R_dist in H2. +elim (H2 _ H); intros alp H3. +elim H3; intros. +exists (mkposreal _ H4); intros. +rewrite Rplus_0_l; rewrite exp_0. +replace ((exp h - 1) / h) with (SFL fn cv h). +replace 1 with (SFL fn cv 0). +apply H5. +split. +unfold D_x, no_cond in |- *; split. +trivial. +apply (sym_not_eq H6). +rewrite Rminus_0_r; apply H7. +unfold SFL in |- *. +case (cv 0); intros. +eapply UL_sequence. +apply u. +unfold Un_cv, SP in |- *. +intros; exists 1%nat; intros. +unfold R_dist in |- *; rewrite decomp_sum. +rewrite (Rplus_comm (fn 0%nat 0)). +replace (fn 0%nat 0) with 1. +unfold Rminus in |- *; rewrite Rplus_assoc; rewrite Rplus_opp_r; + rewrite Rplus_0_r. +replace (sum_f_R0 (fun i:nat => fn (S i) 0) (pred n)) with 0. +rewrite Rabs_R0; apply H8. +symmetry in |- *; apply sum_eq_R0; intros. +unfold fn in |- *. +simpl in |- *. +unfold Rdiv in |- *; do 2 rewrite Rmult_0_l; reflexivity. +unfold fn in |- *; simpl in |- *. +unfold Rdiv in |- *; rewrite Rinv_1; rewrite Rmult_1_r; reflexivity. +apply lt_le_trans with 1%nat; [ apply lt_n_Sn | apply H9 ]. +unfold SFL, exp in |- *. +unfold projT1 in |- *. +case (cv h); case (exist_exp h); intros. +eapply UL_sequence. +apply u. +unfold Un_cv in |- *; intros. +unfold exp_in in e. +unfold infinit_sum in e. +cut (0 < eps0 * Rabs h). +intro; elim (e _ H9); intros N0 H10. +exists N0; intros. +unfold R_dist in |- *. +apply Rmult_lt_reg_l with (Rabs h). +apply Rabs_pos_lt; assumption. +rewrite <- Rabs_mult. +rewrite Rmult_minus_distr_l. +replace (h * ((x - 1) / h)) with (x - 1). +unfold R_dist in H10. +replace (h * SP fn n h - (x - 1)) with + (sum_f_R0 (fun i:nat => / INR (fact i) * h ^ i) (S n) - x). +rewrite (Rmult_comm (Rabs h)). +apply H10. +unfold ge in |- *. +apply le_trans with (S N0). +apply le_n_Sn. +apply le_n_S; apply H11. +rewrite decomp_sum. +replace (/ INR (fact 0) * h ^ 0) with 1. +unfold Rminus in |- *. +rewrite Ropp_plus_distr. +rewrite Ropp_involutive. +rewrite <- (Rplus_comm (- x)). +rewrite <- (Rplus_comm (- x + 1)). +rewrite Rplus_assoc; repeat apply Rplus_eq_compat_l. +replace (pred (S n)) with n; [ idtac | reflexivity ]. +unfold SP in |- *. +rewrite scal_sum. +apply sum_eq; intros. +unfold fn in |- *. +replace (h ^ S i) with (h * h ^ i). +unfold Rdiv in |- *; ring. +simpl in |- *; ring. +simpl in |- *; rewrite Rinv_1; rewrite Rmult_1_r; reflexivity. +apply lt_O_Sn. +unfold Rdiv in |- *. +rewrite <- Rmult_assoc. +symmetry in |- *; apply Rinv_r_simpl_m. +assumption. +apply Rmult_lt_0_compat. +apply H8. +apply Rabs_pos_lt; assumption. +apply SFL_continuity; assumption. +intro; unfold fn in |- *. +replace (fun x:R => x ^ n / INR (fact (S n))) with + (pow_fct n / fct_cte (INR (fact (S n))))%F; [ idtac | reflexivity ]. +apply continuity_div. +apply derivable_continuous; apply (derivable_pow n). +apply derivable_continuous; apply derivable_const. +intro; unfold fct_cte in |- *; apply INR_fact_neq_0. +apply (CVN_R_CVS _ X). +assert (H0 := Alembert_exp). +unfold CVN_R in |- *. +intro; unfold CVN_r in |- *. +apply existT with (fun N:nat => r ^ N / INR (fact (S N))). +cut + (sigT + (fun l:R => + Un_cv + (fun n:nat => + sum_f_R0 (fun k:nat => Rabs (r ^ k / INR (fact (S k)))) n) l)). +intro. +elim X; intros. +exists x; intros. +split. +apply p. +unfold Boule in |- *; intros. +rewrite Rminus_0_r in H1. +unfold fn in |- *. +unfold Rdiv in |- *; rewrite Rabs_mult. +cut (0 < INR (fact (S n))). +intro. +rewrite (Rabs_right (/ INR (fact (S n)))). +do 2 rewrite <- (Rmult_comm (/ INR (fact (S n)))). +apply Rmult_le_compat_l. +left; apply Rinv_0_lt_compat; apply H2. +rewrite <- RPow_abs. +apply pow_maj_Rabs. +rewrite Rabs_Rabsolu; left; apply H1. +apply Rle_ge; left; apply Rinv_0_lt_compat; apply H2. +apply INR_fact_lt_0. +cut ((r:R) <> 0). +intro; apply Alembert_C2. +intro; apply Rabs_no_R0. +unfold Rdiv in |- *; apply prod_neq_R0. +apply pow_nonzero; assumption. +apply Rinv_neq_0_compat; apply INR_fact_neq_0. +unfold Un_cv in H0. +unfold Un_cv in |- *; intros. +cut (0 < eps0 / r); + [ intro + | unfold Rdiv in |- *; apply Rmult_lt_0_compat; + [ assumption | apply Rinv_0_lt_compat; apply (cond_pos r) ] ]. +elim (H0 _ H3); intros N0 H4. +exists N0; intros. +cut (S n >= N0)%nat. +intro hyp_sn. +assert (H6 := H4 _ hyp_sn). +unfold R_dist in H6; rewrite Rminus_0_r in H6. +rewrite Rabs_Rabsolu in H6. +unfold R_dist in |- *; rewrite Rminus_0_r. +rewrite Rabs_Rabsolu. +replace + (Rabs (r ^ S n / INR (fact (S (S n)))) / Rabs (r ^ n / INR (fact (S n)))) + with (r * / INR (fact (S (S n))) * / / INR (fact (S n))). +rewrite Rmult_assoc; rewrite Rabs_mult. +rewrite (Rabs_right r). +apply Rmult_lt_reg_l with (/ r). +apply Rinv_0_lt_compat; apply (cond_pos r). +rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. +rewrite Rmult_1_l; rewrite <- (Rmult_comm eps0). +apply H6. +assumption. +apply Rle_ge; left; apply (cond_pos r). +unfold Rdiv in |- *. +repeat rewrite Rabs_mult. +repeat rewrite Rabs_Rinv. +rewrite Rinv_mult_distr. +repeat rewrite Rabs_right. +rewrite Rinv_involutive. +rewrite (Rmult_comm r). +rewrite (Rmult_comm (r ^ S n)). +repeat rewrite Rmult_assoc. +apply Rmult_eq_compat_l. +rewrite (Rmult_comm r). +rewrite <- Rmult_assoc; rewrite <- (Rmult_comm (INR (fact (S n)))). +apply Rmult_eq_compat_l. +simpl in |- *. +rewrite Rmult_assoc; rewrite <- Rinv_r_sym. +ring. +apply pow_nonzero; assumption. +apply INR_fact_neq_0. +apply Rle_ge; left; apply INR_fact_lt_0. +apply Rle_ge; left; apply pow_lt; apply (cond_pos r). +apply Rle_ge; left; apply INR_fact_lt_0. +apply Rle_ge; left; apply pow_lt; apply (cond_pos r). +apply Rabs_no_R0; apply pow_nonzero; assumption. +apply Rinv_neq_0_compat; apply Rabs_no_R0; apply INR_fact_neq_0. +apply INR_fact_neq_0. +apply INR_fact_neq_0. +unfold ge in |- *; apply le_trans with n. +apply H5. +apply le_n_Sn. +assert (H1 := cond_pos r); red in |- *; intro; rewrite H2 in H1; + elim (Rlt_irrefl _ H1). Qed. (**********) -Lemma derivable_pt_lim_exp : (x:R) (derivable_pt_lim exp x (exp x)). -Intro; Assert H0 := derivable_pt_lim_exp_0. -Unfold derivable_pt_lim in H0; Unfold derivable_pt_lim; Intros. -Cut ``0<eps/(exp x)``; [Intro | Unfold Rdiv; Apply Rmult_lt_pos; [Apply H | Apply Rlt_Rinv; Apply exp_pos]]. -Elim (H0 ? H1); Intros del H2. -Exists del; Intros. -Assert H5 := (H2 ? H3 H4). -Rewrite Rplus_Ol in H5; Rewrite exp_0 in H5. -Replace ``((exp (x+h))-(exp x))/h-(exp x)`` with ``(exp x)*(((exp h)-1)/h-1)``. -Rewrite Rabsolu_mult; Rewrite (Rabsolu_right (exp x)). -Apply Rlt_monotony_contra with ``/(exp x)``. -Apply Rlt_Rinv; Apply exp_pos. -Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1l; Rewrite <- (Rmult_sym eps). -Apply H5. -Assert H6 := (exp_pos x); Red; Intro; Rewrite H7 in H6; Elim (Rlt_antirefl ? H6). -Apply Rle_sym1; Left; Apply exp_pos. -Rewrite Rminus_distr. -Rewrite Rmult_1r; Unfold Rdiv; Rewrite <- Rmult_assoc; Rewrite Rminus_distr. -Rewrite Rmult_1r; Rewrite exp_plus; Reflexivity. -Qed. +Lemma derivable_pt_lim_exp : forall x:R, derivable_pt_lim exp x (exp x). +intro; assert (H0 := derivable_pt_lim_exp_0). +unfold derivable_pt_lim in H0; unfold derivable_pt_lim in |- *; intros. +cut (0 < eps / exp x); + [ intro + | unfold Rdiv in |- *; apply Rmult_lt_0_compat; + [ apply H | apply Rinv_0_lt_compat; apply exp_pos ] ]. +elim (H0 _ H1); intros del H2. +exists del; intros. +assert (H5 := H2 _ H3 H4). +rewrite Rplus_0_l in H5; rewrite exp_0 in H5. +replace ((exp (x + h) - exp x) / h - exp x) with + (exp x * ((exp h - 1) / h - 1)). +rewrite Rabs_mult; rewrite (Rabs_right (exp x)). +apply Rmult_lt_reg_l with (/ exp x). +apply Rinv_0_lt_compat; apply exp_pos. +rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. +rewrite Rmult_1_l; rewrite <- (Rmult_comm eps). +apply H5. +assert (H6 := exp_pos x); red in |- *; intro; rewrite H7 in H6; + elim (Rlt_irrefl _ H6). +apply Rle_ge; left; apply exp_pos. +rewrite Rmult_minus_distr_l. +rewrite Rmult_1_r; unfold Rdiv in |- *; rewrite <- Rmult_assoc; + rewrite Rmult_minus_distr_l. +rewrite Rmult_1_r; rewrite exp_plus; reflexivity. +Qed.
\ No newline at end of file |