diff options
| -rw-r--r-- | theories/Reals/Alembert.v | 15 | ||||
| -rw-r--r-- | theories/Reals/Ranalysis1.v | 119 | ||||
| -rw-r--r-- | theories/Reals/Ranalysis4.v | 58 | ||||
| -rw-r--r-- | theories/Reals/Rtrigo_def.v | 35 |
4 files changed, 140 insertions, 87 deletions
diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index f1ed4cc69e..10ebfc0c5e 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -16,26 +16,22 @@ Require Rbase. Require Rseries. Require Rtrigo_fun. -Axiom fct_eq : (A:Type)(f1,f2:A->R) ((x:A)(f1 x)==(f2 x)) -> f1 == f2. - -Definition SigT := Specif.sigT. +(*********************) +(* Lemmes techniques *) +(*********************) Lemma not_sym : (r1,r2:R) ``r1<>r2`` -> ``r2<>r1``. Intros; Red; Intro H0; Rewrite H0 in H; Elim H; Reflexivity. Qed. Lemma Rgt_2_0 : ``0<2``. -Cut ~(O=(2)); [Intro H0; Generalize (lt_INR_0 (2) (neq_O_lt (2) H0)); Unfold INR; Intro H; Assumption | Discriminate]. +Sup0. Qed. Lemma Rgt_3_0 : ``0<3``. -Cut ~(O=(3)); [Intro H0; Generalize (lt_INR_0 (3) (neq_O_lt (3) H0)); Rewrite INR_eq_INR2; Unfold INR2; Intro H; Assumption | Discriminate]. +Sup0. Qed. -(*********************) -(* Lemmes techniques *) -(*********************) - Lemma tech1 : (An:nat->R;N:nat) ((n:nat)``(le n N)``->``0<(An n)``) -> ``0 < (sum_f_R0 An N)``. Intros; Induction N. Simpl; Apply H. @@ -382,6 +378,7 @@ Replace ``k+(1-k)`` with R1; [Assumption | Ring]. Apply Rlt_Rinv; Apply Rgt_2_0. Qed. +Definition SigT := Specif.sigT. (*************************************************) (* Différentes versions du critère de D'Alembert *) diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v index 490940e73b..cb7b2b6edd 100644 --- a/theories/Reals/Ranalysis1.v +++ b/theories/Reals/Ranalysis1.v @@ -339,9 +339,18 @@ Intros. Apply unicite_step3. Assert H1 := (unicite_step2 ? ? ? H). Assert H2 := (unicite_step2 ? ? ? H0). -Unfold plus_fct; Replace [h:R]``((f1 (x+h))+(f2 (x+h))-((f1 x)+(f2 x)))/h`` with [h:R](Rplus ([h':R]``((f1 (x+h'))-(f1 x))/h'`` h) ([h':R]``((f2 (x+h'))-(f2 x))/h'`` h)). -Apply (limit_plus [h':R]``((f1 (x+h'))-(f1 x))/h'`` [h':R]``((f2 (x+h'))-(f2 x))/h'`` [h:R]``h <> 0`` l1 l2 ``0`` H1 H2). -Apply fct_eq; Intro; Unfold Rdiv; Ring. +Unfold plus_fct. +Cut (h:R)``((f1 (x+h))+(f2 (x+h))-((f1 x)+(f2 x)))/h``==``((f1 (x+h))-(f1 x))/h+((f2 (x+h))-(f2 x))/h``. +Intro. +Generalize(limit_plus [h':R]``((f1 (x+h'))-(f1 x))/h'`` [h':R]``((f2 (x+h'))-(f2 x))/h'`` [h:R]``h <> 0`` l1 l2 ``0`` H1 H2). +Unfold limit1_in; Unfold limit_in; Unfold dist; Simpl; Unfold R_dist; Intros. +Elim (H4 eps H5); Intros. +Exists x0. +Elim H6; Intros. +Split. +Assumption. +Intros; Rewrite H3; Apply H8; Assumption. +Intro; Unfold Rdiv; Ring. Qed. Lemma derivable_pt_lim_opp : (f:R->R;x,l:R) (derivable_pt_lim f x l) -> (derivable_pt_lim (opp_fct f) x (Ropp l)). @@ -349,9 +358,17 @@ Intros. Apply unicite_step3. Assert H1 := (unicite_step2 ? ? ? H). Unfold opp_fct. -Replace [h:R]``( -(f (x+h))- -(f x))/h`` with [h:R](Ropp ``((f (x+h))-(f x))/h``). -Apply (limit_Ropp [h:R]``((f (x+h))-(f x))/h``[h:R]``h <> 0`` l ``0`` H1). -Apply fct_eq; Intro; Unfold Rdiv; Ring. +Cut (h:R) ``( -(f (x+h))- -(f x))/h``==(Ropp ``((f (x+h))-(f x))/h``). +Intro. +Generalize (limit_Ropp [h:R]``((f (x+h))-(f x))/h``[h:R]``h <> 0`` l ``0`` H1). +Unfold limit1_in; Unfold limit_in; Unfold dist; Simpl; Unfold R_dist; Intros. +Elim (H2 eps H3); Intros. +Exists x0. +Elim H4; Intros. +Split. +Assumption. +Intros; Rewrite H0; Apply H6; Assumption. +Intro; Unfold Rdiv; Ring. Qed. Lemma derivable_pt_lim_minus : (f1,f2:R->R;x,l1,l2:R) (derivable_pt_lim f1 x l1) -> (derivable_pt_lim f2 x l2) -> (derivable_pt_lim (minus_fct f1 f2) x ``l1-l2``). @@ -360,9 +377,17 @@ Apply unicite_step3. Assert H1 := (unicite_step2 ? ? ? H). Assert H2 := (unicite_step2 ? ? ? H0). Unfold minus_fct. -Replace [h:R]``((f1 (x+h))-(f2 (x+h)) - ((f1 x)-(f2 x)))/h`` with [h:R](Rminus ([h':R]``((f1 (x+h'))-(f1 x))/h'`` h) ([h':R]``((f2 (x+h'))-(f2 x))/h'`` h)). -Apply (limit_minus [h':R]``((f1 (x+h'))-(f1 x))/h'`` [h':R]``((f2 (x+h'))-(f2 x))/h'`` [h:R]``h <> 0`` l1 l2 ``0`` H1 H2). -Apply fct_eq; Intro; Unfold Rdiv; Ring. +Cut (h:R)``((f1 (x+h))-(f1 x))/h-((f2 (x+h))-(f2 x))/h``==``((f1 (x+h))-(f2 (x+h))-((f1 x)-(f2 x)))/h``. +Intro. +Generalize (limit_minus [h':R]``((f1 (x+h'))-(f1 x))/h'`` [h':R]``((f2 (x+h'))-(f2 x))/h'`` [h:R]``h <> 0`` l1 l2 ``0`` H1 H2). +Unfold limit1_in; Unfold limit_in; Unfold dist; Simpl; Unfold R_dist; Intros. +Elim (H4 eps H5); Intros. +Exists x0. +Elim H6; Intros. +Split. +Assumption. +Intros; Rewrite <- H3; Apply H8; Assumption. +Intro; Unfold Rdiv; Ring. Qed. Lemma derivable_pt_lim_mult : (f1,f2:R->R;x,l1,l2:R) (derivable_pt_lim f1 x l1) -> (derivable_pt_lim f2 x l2) -> (derivable_pt_lim (mult_fct f1 f2) x ``l1*(f2 x)+(f1 x)*l2``). @@ -449,19 +474,22 @@ Axiom derivable_pt_lim_sqrt : (x:R) ``0<x`` -> (derivable_pt_lim sqrt x ``/(2*(s Axiom derivable_pt_lim_sin : (x:R) (derivable_pt_lim sin x (cos x)). Lemma derivable_pt_lim_cos : (x:R) (derivable_pt_lim cos x ``-(sin x)``). -Intro; Cut (comp sin (plus_fct id (fct_cte ``PI/2``)))==cos. -Intro; Rewrite <- H. -Replace ``-(sin x)`` with (Rmult (cos ``x+PI/2``) (Rplus R1 R0)). -Apply derivable_pt_lim_comp. +Intro; Cut (h:R)``(sin (h+PI/2))``==(cos h). +Intro; Replace ``-(sin x)`` with (Rmult (cos ``x+PI/2``) (Rplus R1 R0)). +Generalize (derivable_pt_lim_comp (plus_fct id (fct_cte ``PI/2``)) sin); Intros. +Cut (derivable_pt_lim (plus_fct id (fct_cte ``PI/2``)) x ``1+0``). +Cut (derivable_pt_lim sin (plus_fct id (fct_cte ``PI/2``) x) ``(cos (x+PI/2))``). +Intros; Generalize (H0 ? ? ? H2 H1); Replace (comp sin (plus_fct id (fct_cte ``PI/2``))) with [x:R]``(sin (x+PI/2))``; [Idtac | Reflexivity]. +Unfold derivable_pt_lim; Intros. +Elim (H3 eps H4); Intros. +Exists x0. +Intros; Rewrite <- (H ``x+h``); Rewrite <- (H x); Apply H5; Assumption. +Apply derivable_pt_lim_sin. Apply derivable_pt_lim_plus. Apply derivable_pt_lim_id. Apply derivable_pt_lim_const. -Replace (plus_fct id (fct_cte ``PI/2``) x) with ``x+PI/2``. -Apply derivable_pt_lim_sin. -Unfold plus_fct id fct_cte; Reflexivity. -Rewrite Rplus_Or; Rewrite Rmult_1r; Rewrite sin_cos; Rewrite Ropp_Ropp; Rewrite Rplus_sym; Reflexivity. -Unfold comp plus_fct id fct_cte; Apply fct_eq; Intro. -Rewrite cos_sin; Rewrite Rplus_sym; Reflexivity. +Rewrite sin_cos; Rewrite <- (Rplus_sym x); Ring. +Intro; Rewrite cos_sin; Rewrite Rplus_sym; Reflexivity. Qed. Lemma derivable_pt_plus : (f1,f2:R->R;x:R) (derivable_pt f1 x) -> (derivable_pt f2 x) -> (derivable_pt (plus_fct f1 f2) x). @@ -1088,26 +1116,30 @@ Unfold increasing decreasing opp_fct; Intros; Generalize (H x y H0); Intro; Appl Qed. (**********) -Lemma opp_opp_fct : (f:R->R) (opp_fct (opp_fct f))==f. -Intro; Unfold opp_fct; Apply fct_eq; Intro; Rewrite Ropp_Ropp; Reflexivity. -Qed. - - - -(**********) Lemma nonpos_derivative_1 : (f:R->R;pr:(derivable f)) ((x:R) ``(derive_pt f x (pr x))<=0``) -> (decreasing f). -Intros; Rewrite <- (opp_opp_fct f); Apply increasing_decreasing_opp. +Intros. +Cut (h:R)``-(-(f h))==(f h)``. +Intro. +Generalize (increasing_decreasing_opp (opp_fct f)). +Unfold decreasing. +Unfold opp_fct. +Intros. +Rewrite <- (H0 x); Rewrite <- (H0 y). +Apply H1. Cut (x:R)``0<=(derive_pt (opp_fct f) x ((derivable_opp f pr) x))``. Intros. -Apply (nonneg_derivative_1 (opp_fct f) (derivable_opp f pr) H0). +Replace [x:R]``-(f x)`` with (opp_fct f); [Idtac | Reflexivity]. +Apply (nonneg_derivative_1 (opp_fct f) (derivable_opp f pr) H3). Intro. -Assert H0 := (derive_pt_opp f x (pr x)). -Cut ``(derive_pt (opp_fct f) x (derivable_pt_opp f x (pr x)))==(derive_pt (opp_fct f) x (derivable_opp f pr x))``. +Assert H3 := (derive_pt_opp f x0 (pr x0)). +Cut ``(derive_pt (opp_fct f) x0 (derivable_pt_opp f x0 (pr x0)))==(derive_pt (opp_fct f) x0 (derivable_opp f pr x0))``. Intro. -Rewrite <- H1. -Rewrite H0. -Rewrite <- Ropp_O; Apply Rge_Ropp; Apply Rle_sym1; Apply (H x). +Rewrite <- H4. +Rewrite H3. +Rewrite <- Ropp_O; Apply Rge_Ropp; Apply Rle_sym1; Apply (H x0). Apply pr_nu. +Assumption. +Intro; Ring. Qed. (**********) @@ -1121,16 +1153,25 @@ Qed. (**********) Lemma negative_derivative : (f:R->R;pr:(derivable f)) ((x:R) ``(derive_pt f x (pr x))<0``)->(strict_decreasing f). -Intros; Rewrite <- (opp_opp_fct f); Apply strictincreasing_strictdecreasing_opp. +Intros. +Cut (h:R)``- (-(f h))==(f h)``. +Intros. +Generalize (strictincreasing_strictdecreasing_opp (opp_fct f)). +Unfold strict_decreasing opp_fct. +Intros. +Rewrite <- (H0 x). +Rewrite <- (H0 y). +Apply H1; [Idtac | Assumption]. Cut (x:R)``0<(derive_pt (opp_fct f) x (derivable_opp f pr x))``. -Intros; EApply positive_derivative; Apply H0. +Intros; EApply positive_derivative; Apply H3. Intro. -Assert H0 := (derive_pt_opp f x (pr x)). -Cut ``(derive_pt (opp_fct f) x (derivable_pt_opp f x (pr x)))==(derive_pt (opp_fct f) x (derivable_opp f pr x))``. +Assert H3 := (derive_pt_opp f x0 (pr x0)). +Cut ``(derive_pt (opp_fct f) x0 (derivable_pt_opp f x0 (pr x0)))==(derive_pt (opp_fct f) x0 (derivable_opp f pr x0))``. Intro. -Rewrite <- H1; Rewrite H0. -Rewrite <- Ropp_O; Apply Rlt_Ropp; Apply (H x). +Rewrite <- H4; Rewrite H3. +Rewrite <- Ropp_O; Apply Rlt_Ropp; Apply (H x0). Apply pr_nu. +Intro; Ring. Qed. (**********) diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v index 10913dc40e..a3ce1e4d1f 100644 --- a/theories/Reals/Ranalysis4.v +++ b/theories/Reals/Ranalysis4.v @@ -27,8 +27,8 @@ Apply derivable_pt_div. Apply derivable_pt_const. Assumption. Assumption. -Unfold div_fct inv_fct fct_cte; Intro. -Replace [x:R]``/(f x)`` with [x:R]``1/(f x)``; [Assumption | Apply fct_eq; Intro; Unfold Rdiv; Rewrite Rmult_1l; Reflexivity]. +Unfold div_fct inv_fct fct_cte; Intro; Elim X0; Intros; Unfold derivable_pt; Apply Specif.existT with x0; Unfold derivable_pt_abs; Unfold derivable_pt_lim; Unfold derivable_pt_abs in p; Unfold derivable_pt_lim in p; Intros; Elim (p eps H0); Intros; Exists x1; Intros; Unfold Rdiv in H1; Unfold Rdiv; Rewrite <- (Rmult_1l ``/(f x)``); Rewrite <- (Rmult_1l ``/(f (x+h))``). +Apply H1; Assumption. Qed. (**********) @@ -42,6 +42,26 @@ Apply unicite_limite with g x; Assumption. Qed. (**********) +Lemma pr_nu_var2 : (f,g:R->R;x:R;pr1:(derivable_pt f x);pr2:(derivable_pt g x)) ((h:R)(f h)==(g h)) -> (derive_pt f x pr1) == (derive_pt g x pr2). +Unfold derivable_pt derive_pt; Intros. +Elim pr1; Intros. +Elim pr2; Intros. +Simpl. +Assert H0 := (unicite_step2 ? ? ? p). +Assert H1 := (unicite_step2 ? ? ? p0). +Cut (limit1_in [h:R]``((f (x+h))-(f x))/h`` [h:R]``h <> 0`` x1 ``0``). +Intro; Assert H3 := (unicite_step1 ? ? ? ? H0 H2). +Assumption. +Unfold limit1_in; Unfold limit_in; Unfold dist; Simpl; Unfold R_dist; Unfold limit1_in in H1; Unfold limit_in in H1; Unfold dist in H1; Simpl in H1; Unfold R_dist in H1. +Intros; Elim (H1 eps H2); Intros. +Elim H3; Intros. +Exists x2. +Split. +Assumption. +Intros; Do 2 Rewrite H; Apply H5; Assumption. +Qed. + +(**********) Lemma derivable_inv : (f:R->R) ((x:R)``(f x)<>0``)->(derivable f)->(derivable (inv_fct f)). Intros. Unfold derivable; Intro. @@ -53,9 +73,9 @@ Qed. Lemma derive_pt_inv : (f:R->R;x:R;pr:(derivable_pt f x);na:``(f x)<>0``) (derive_pt (inv_fct f) x (derivable_pt_inv f x na pr)) == ``-(derive_pt f x pr)/(Rsqr (f x))``. Intros; Replace (derive_pt (inv_fct f) x (derivable_pt_inv f x na pr)) with (derive_pt (div_fct (fct_cte R1) f) x (derivable_pt_div (fct_cte R1) f x (derivable_pt_const R1 x) pr na)). Rewrite derive_pt_div; Rewrite derive_pt_const; Unfold fct_cte; Rewrite Rmult_Ol; Rewrite Rmult_1r; Unfold Rminus; Rewrite Rplus_Ol; Reflexivity. -Apply pr_nu_var. -Unfold div_fct fct_cte inv_fct; Apply fct_eq. -Intro; Unfold Rdiv; Rewrite Rmult_1l; Reflexivity. +Apply pr_nu_var2. +Intro; Unfold div_fct fct_cte inv_fct. +Unfold Rdiv; Ring. Qed. (* Regularity of hyperbolic functions *) @@ -63,38 +83,34 @@ Axiom derivable_pt_lim_exp : (x:R) (derivable_pt_lim exp x (exp x)). Lemma derivable_pt_lim_cosh : (x:R) (derivable_pt_lim cosh x ``(sinh x)``). Intro. -Unfold cosh sinh. -Replace [x0:R]``((exp x0)+(exp ( -x0)))/2`` with (plus_fct (mult_real_fct ``/2`` exp) (mult_real_fct ``/2`` (comp exp (opp_fct id)))). -Replace ``((exp x)-(exp ( -x)))/2`` with ``/2*(exp x)+/2*((exp (-x))*-1)``. +Unfold cosh sinh; Unfold Rdiv. +Replace [x0:R]``((exp x0)+(exp ( -x0)))*/2`` with (mult_fct (plus_fct exp (comp exp (opp_fct id))) (fct_cte ``/2``)); [Idtac | Reflexivity]. +Replace ``((exp x)-(exp ( -x)))*/2`` with ``((exp x)+((exp (-x))*-1))*((fct_cte (Rinv 2)) x)+((plus_fct exp (comp exp (opp_fct id))) x)*0``. +Apply derivable_pt_lim_mult. Apply derivable_pt_lim_plus. -Apply derivable_pt_lim_scal. Apply derivable_pt_lim_exp. -Apply derivable_pt_lim_scal. Apply derivable_pt_lim_comp. Apply derivable_pt_lim_opp. Apply derivable_pt_lim_id. Apply derivable_pt_lim_exp. -Unfold Rdiv; Ring. -Unfold plus_fct mult_real_fct comp opp_fct id; Apply fct_eq. -Intro; Unfold Rdiv; Ring. +Apply derivable_pt_lim_const. +Unfold plus_fct mult_real_fct comp opp_fct id fct_cte; Ring. Qed. Lemma derivable_pt_lim_sinh : (x:R) (derivable_pt_lim sinh x ``(cosh x)``). Intro. -Unfold cosh sinh. -Replace [x0:R]``((exp x0)-(exp ( -x0)))/2`` with (minus_fct (mult_real_fct ``/2`` exp) (mult_real_fct ``/2`` (comp exp (opp_fct id)))). -Replace ``((exp x)+(exp ( -x)))/2`` with ``/2*(exp x)-/2*((exp (-x))*-1)``. +Unfold cosh sinh; Unfold Rdiv. +Replace [x0:R]``((exp x0)-(exp ( -x0)))*/2`` with (mult_fct (minus_fct exp (comp exp (opp_fct id))) (fct_cte ``/2``)); [Idtac | Reflexivity]. +Replace ``((exp x)+(exp ( -x)))*/2`` with ``((exp x)-((exp (-x))*-1))*((fct_cte (Rinv 2)) x)+((minus_fct exp (comp exp (opp_fct id))) x)*0``. +Apply derivable_pt_lim_mult. Apply derivable_pt_lim_minus. -Apply derivable_pt_lim_scal. Apply derivable_pt_lim_exp. -Apply derivable_pt_lim_scal. Apply derivable_pt_lim_comp. Apply derivable_pt_lim_opp. Apply derivable_pt_lim_id. Apply derivable_pt_lim_exp. -Unfold Rdiv; Ring. -Unfold minus_fct mult_real_fct comp opp_fct id; Apply fct_eq. -Intro; Unfold Rdiv; Ring. +Apply derivable_pt_lim_const. +Unfold plus_fct mult_real_fct comp opp_fct id fct_cte; Ring. Qed. Lemma derivable_pt_exp : (x:R) (derivable_pt exp x). diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 8fc69e0385..b1377776de 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -74,16 +74,13 @@ Unfold exp_in; Unfold infinit_sum; Intros. Exists O. Intros; Replace (sum_f_R0 ([i:nat]``/(INR (fact i))*(pow R0 i)``) n) with R1. Unfold R_dist; Replace ``1-1`` with R0; [Rewrite Rabsolu_R0; Assumption | Ring]. -Replace [i:nat]``/(INR (fact i))*(pow 0 i)`` with [i:nat](Cases i of O => R1 | _ => R0 end). Induction n. -Simpl; Reflexivity. -Simpl; Rewrite <- Hrecn; [Ring | Unfold ge; Apply le_O_n]. -Apply fct_eq. -Intro; Case x. -Unfold fact; Rewrite pow_O. -Replace (INR (S O)) with R1; [Idtac | Reflexivity]. -Rewrite Rinv_R1; Ring. -Intro; Rewrite pow_i; [Ring | Apply lt_O_Sn]. +Simpl; Rewrite Rinv_R1; Ring. +Rewrite tech5. +Rewrite <- Hrecn. +Simpl. +Ring. +Unfold ge; Apply le_O_n. Defined. Lemma exp_0 : ``(exp 0)==1``. @@ -403,16 +400,18 @@ Qed. Lemma exist_cos0 : (SigT R [l:R](cos_in R0 l)). Apply Specif.existT with R1. Unfold cos_in; Unfold infinit_sum; Intros; Exists O. -Intros; Replace (sum_f_R0 ([i:nat]``(cos_n i)*(pow R0 i)``) n) with R1. -Unfold R_dist; Replace ``1-1`` with R0; [Idtac | Ring]. -Rewrite Rabsolu_R0; Assumption. -Replace [i:nat]``(cos_n i)*(pow 0 i)`` with [i:nat](Cases i of O => R1 | _ => R0 end). +Intros. +Unfold R_dist. Induction n. -Simpl; Reflexivity. -Simpl; Rewrite <- Hrecn; [Ring | Unfold ge; Apply le_O_n]. -Apply fct_eq; Intro; Induction x. -Unfold cos_n; Repeat Rewrite pow_O; Replace (mult (S (S O)) O) with O; [Idtac | Ring]; Unfold fact; Replace (INR (S O)) with R1; [Idtac | Reflexivity]; Unfold Rdiv; Rewrite Rinv_R1; Ring. -Rewrite pow_i; [Ring | Apply lt_O_Sn]. +Unfold cos_n; Simpl. +Unfold Rdiv; Rewrite Rinv_R1. +Do 2 Rewrite Rmult_1r. +Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Assumption. +Rewrite tech5. +Replace ``(cos_n (S n))*(pow 0 (S n))`` with R0. +Rewrite Rplus_Or. +Apply Hrecn; Unfold ge; Apply le_O_n. +Simpl; Ring. Defined. (* Calcul de (cos 0) *) |