Regularites de pow et des sommes finies / MAJ Reg

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2904 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 173 insertions, 14 deletions

diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v
index 735687caa..a2fbac997 100644
--- a/theories/Reals/Ranalysis4.v
+++ b/theories/Reals/Ranalysis4.v
@@ -150,6 +150,154 @@ Intros; Rewrite H; Rewrite Rabsolu_R0; Unfold Rminus; Rewrite Ropp_O; Rewrite Rp
 Apply derivable_continuous_pt; Apply (derivable_pt_Rabsolu x H).
 Qed.
 
+(* Pow *)
+Lemma derivable_pt_lim_pow_pos : (x:R;n:nat) (lt O n) -> (derivable_pt_lim [y:R](pow y n) x ``(INR n)*(pow x (pred n))``).
+Intros.
+Induction n.
+Elim (lt_n_n ? H).
+Cut n=O\/(lt O n).
+Intro; Elim H0; Intro.
+Rewrite H1; Simpl.
+Replace [y:R]``y*1`` with (mult_fct id (fct_cte R1)).
+Replace ``1*1`` with ``1*(fct_cte R1 x)+(id x)*0``.
+Apply derivable_pt_lim_mult.
+Apply derivable_pt_lim_id.
+Apply derivable_pt_lim_const.
+Unfold fct_cte id; Ring.
+Reflexivity.
+Replace [y:R](pow y (S n)) with [y:R]``y*(pow y n)``.
+Replace (pred (S n)) with n; [Idtac | Reflexivity].
+Replace [y:R]``y*(pow y n)`` with (mult_fct id [y:R](pow y n)).
+Pose f := [y:R](pow y n).
+Replace ``(INR (S n))*(pow x n)`` with (Rplus (Rmult R1 (f x)) (Rmult (id x) (Rmult (INR n) (pow x (pred n))))).
+Apply derivable_pt_lim_mult.
+Apply derivable_pt_lim_id.
+Unfold f; Apply Hrecn; Assumption.
+Unfold f.
+Pattern 1 5 n; Replace n with (S (pred n)).
+Unfold id; Rewrite S_INR; Simpl.
+Ring.
+Symmetry; Apply S_pred with O; Assumption.
+Unfold mult_fct id; Reflexivity.
+Reflexivity.
+Inversion H.
+Left; Reflexivity.
+Right.
+Apply lt_le_trans with (1).
+Apply lt_O_Sn.
+Assumption.
+Qed.
+
+Lemma derivable_pt_lim_pow : (x:R; n:nat) (derivable_pt_lim [y:R](pow y n) x ``(INR n)*(pow x (pred n))``).
+Intros.
+Induction n.
+Simpl.
+Rewrite Rmult_Ol.
+Replace [_:R]``1`` with (fct_cte R1); [Apply derivable_pt_lim_const | Reflexivity].
+Apply derivable_pt_lim_pow_pos.
+Apply lt_O_Sn.
+Qed.
+
+Lemma derivable_pt_pow : (n:nat;x:R) (derivable_pt [y:R](pow y n) x).
+Intros; Unfold derivable_pt.
+Apply Specif.existT with ``(INR n)*(pow x (pred n))``.
+Apply derivable_pt_lim_pow.
+Qed.
+
+Lemma derivable_pow : (n:nat) (derivable [y:R](pow y n)).
+Intro; Unfold derivable; Intro; Apply derivable_pt_pow.
+Qed.
+
+Lemma derive_pt_pow : (n:nat;x:R) (derive_pt [y:R](pow y n) x (derivable_pt_pow n x))==``(INR n)*(pow x (pred n))``.
+Intros; Apply derive_pt_eq_0.
+Apply derivable_pt_lim_pow.
+Qed.
+
+(* Finite sums : Sum a_k x^k *)
+Lemma continuity_finite_sum : (An:nat->R;N:nat) (continuity [y:R](sum_f_R0 [k:nat]``(An k)*(pow y k)`` N)).
+Intros; Unfold continuity; Intro.
+Induction N.
+Simpl.
+Apply continuity_pt_const.
+Unfold constant; Intros; Reflexivity.
+Replace [y:R](sum_f_R0 [k:nat]``(An k)*(pow y k)`` (S N)) with (plus_fct [y:R](sum_f_R0 [k:nat]``(An k)*(pow y k)`` N) [y:R]``(An (S N))*(pow y (S N))``).
+Apply continuity_pt_plus.
+Apply HrecN.
+Replace [y:R]``(An (S N))*(pow y (S N))`` with (mult_real_fct (An (S N)) [y:R](pow y (S N))).
+Apply continuity_pt_scal.
+Apply derivable_continuous_pt.
+Apply derivable_pt_pow.
+Reflexivity.
+Reflexivity.
+Qed.
+
+Lemma derivable_pt_lim_fs : (An:nat->R;x:R;N:nat) (lt O N) -> (derivable_pt_lim [y:R](sum_f_R0 [k:nat]``(An k)*(pow y k)`` N) x (sum_f_R0 [k:nat]``(INR (S k))*(An (S k))*(pow x k)`` (pred N))).
+Intros; Induction N.
+Elim (lt_n_n ? H).
+Cut N=O\/(lt O N).
+Intro; Elim H0; Intro.
+Rewrite H1.
+Simpl.
+Replace [y:R]``(An O)*1+(An (S O))*(y*1)`` with (plus_fct (fct_cte ``(An O)*1``) (mult_real_fct ``(An (S O))`` (mult_fct id (fct_cte R1)))).
+Replace ``1*(An (S O))*1`` with ``0+(An (S O))*(1*(fct_cte R1 x)+(id x)*0)``.
+Apply derivable_pt_lim_plus.
+Apply derivable_pt_lim_const.
+Apply derivable_pt_lim_scal.
+Apply derivable_pt_lim_mult.
+Apply derivable_pt_lim_id.
+Apply derivable_pt_lim_const.
+Unfold fct_cte id; Ring.
+Reflexivity.
+Replace [y:R](sum_f_R0 [k:nat]``(An k)*(pow y k)`` (S N)) with (plus_fct [y:R](sum_f_R0 [k:nat]``(An k)*(pow y k)`` N) [y:R]``(An (S N))*(pow y (S N))``).
+Replace (sum_f_R0 [k:nat]``(INR (S k))*(An (S k))*(pow x k)`` (pred (S N))) with (Rplus (sum_f_R0 [k:nat]``(INR (S k))*(An (S k))*(pow x k)`` (pred N)) ``(An (S N))*((INR (S (pred (S N))))*(pow x (pred (S N))))``).
+Apply derivable_pt_lim_plus.
+Apply HrecN.
+Assumption.
+Replace [y:R]``(An (S N))*(pow y (S N))`` with (mult_real_fct (An (S N)) [y:R](pow y (S N))).
+Apply derivable_pt_lim_scal.
+Replace (pred (S N)) with N; [Idtac | Reflexivity].
+Pattern 3 N; Replace N with (pred (S N)).
+Apply derivable_pt_lim_pow.
+Reflexivity.
+Reflexivity.
+Cut (pred (S N)) = (S (pred N)).
+Intro; Rewrite H2.
+Rewrite tech5.
+Apply Rplus_plus_r.
+Rewrite <- H2.
+Replace (pred (S N)) with N; [Idtac | Reflexivity].
+Ring.
+Simpl.
+Apply S_pred with O; Assumption.
+Unfold plus_fct.
+Simpl; Reflexivity.
+Inversion H.
+Left; Reflexivity.
+Right; Apply lt_le_trans with (1); [Apply lt_O_Sn | Assumption].
+Qed.
+
+Lemma derivable_pt_lim_finite_sum : (An:(nat->R); x:R; N:nat) (derivable_pt_lim [y:R](sum_f_R0 [k:nat]``(An k)*(pow y k)`` N) x (Cases N of O => R0 | _ => (sum_f_R0 [k:nat]``(INR (S k))*(An (S k))*(pow x k)`` (pred N)) end)).
+Intros.
+Induction N.
+Simpl.
+Rewrite Rmult_1r.
+Replace [_:R]``(An O)`` with (fct_cte (An O)); [Apply derivable_pt_lim_const | Reflexivity].
+Apply derivable_pt_lim_fs; Apply lt_O_Sn.
+Qed.
+
+Lemma derivable_pt_finite_sum : (An:nat->R;N:nat;x:R) (derivable_pt [y:R](sum_f_R0 [k:nat]``(An k)*(pow y k)`` N) x).
+Intros.
+Unfold derivable_pt.
+Assert H := (derivable_pt_lim_finite_sum An x N).
+Induction N.
+Apply Specif.existT with R0; Apply H.
+Apply Specif.existT with (sum_f_R0 [k:nat]``(INR (S k))*(An (S k))*(pow x k)`` (pred (S N))); Apply H.
+Qed.
+
+Lemma derivable_finite_sum : (An:nat->R;N:nat) (derivable [y:R](sum_f_R0 [k:nat]``(An k)*(pow y k)`` N)).
+Intros; Unfold derivable; Intro; Apply derivable_pt_finite_sum.
+Qed.
+
 (* Regularity of hyperbolic functions *)
 Axiom derivable_pt_lim_exp : (x:R) (derivable_pt_lim exp x (exp x)).   
 
@@ -234,6 +382,8 @@ Apply derivable_pt_lim_sinh.
 Qed.
 
 
+Definition pow_fct [n:nat] : R->R := [y:R](pow y n).
+
 (**********)
 Tactic Definition IntroHypG trm :=
 Match trm With
@@ -392,6 +542,7 @@ Match Context With
  |[|-(derivable cosh)] -> Apply derivable_cosh
  |[|-(derivable sinh)] -> Apply derivable_sinh
  |[|-(derivable exp)] -> Apply derivable_exp
+ |[|-(derivable (pow_fct ?))] -> Unfold pow_fct; Apply derivable_pow
   (* regles de differentiabilite *)
   (* PLUS *)
  |[|-(derivable (plus_fct ?1 ?2))] -> Apply (derivable_plus ?1 ?2); IsDiff_glob
@@ -404,14 +555,14 @@ Match Context With
   (* MULTIPLICATION *)
  |[|-(derivable (mult_fct ?1 ?2))] -> Apply (derivable_mult ?1 ?2); IsDiff_glob
   (* DIVISION *)
- |[|-(derivable (div_fct ?1 ?2))] -> Apply (derivable_div ?1 ?2); [IsDiff_glob | IsDiff_glob | Try Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp]
+ |[|-(derivable (div_fct ?1 ?2))] -> Apply (derivable_div ?1 ?2); [IsDiff_glob | IsDiff_glob | Try Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp pow_fct]
   (* INVERSION *)
- |[|-(derivable (inv_fct ?1))] -> Apply (derivable_inv ?1); [Try Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp | IsDiff_glob]
+ |[|-(derivable (inv_fct ?1))] -> Apply (derivable_inv ?1); [Try Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp pow_fct | IsDiff_glob]
   (* COMPOSITION *)
  |[|-(derivable (comp ?1 ?2))] -> Apply (derivable_comp ?2 ?1); IsDiff_glob
  |[_:(derivable ?1)|-(derivable ?1)] -> Assumption
  |[|-True->(derivable ?)] -> Intro HypTruE; Clear HypTruE; IsDiff_glob
- | _ -> Try Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp.
+ | _ -> Try Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp pow_fct.
  
 (**********)
 Recursive Tactic Definition IsDiff_pt :=
@@ -425,8 +576,9 @@ Match Context With
 |[|-(derivable_pt sinh ?)] -> Apply derivable_pt_sinh
 |[|-(derivable_pt cosh ?)] -> Apply derivable_pt_cosh
 |[|-(derivable_pt exp ?)] -> Apply derivable_pt_exp
-|[|-(derivable_pt sqrt ?1)] -> Apply (derivable_pt_sqrt ?1); Assumption Orelse Unfold plus_fct minus_fct opp_fct mult_fct div_fct inv_fct comp id fct_cte
-|[|-(derivable_pt Rabsolu ?1)] -> Apply (derivable_pt_Rabsolu ?1); Assumption Orelse Unfold plus_fct minus_fct opp_fct mult_fct div_fct inv_fct comp id fct_cte
+|[|-(derivable_pt (pow_fct ?) ?)] -> Unfold pow_fct; Apply derivable_pt_pow
+|[|-(derivable_pt sqrt ?1)] -> Apply (derivable_pt_sqrt ?1); Assumption Orelse Unfold plus_fct minus_fct opp_fct mult_fct div_fct inv_fct comp id fct_cte pow_fct
+|[|-(derivable_pt Rabsolu ?1)] -> Apply (derivable_pt_Rabsolu ?1); Assumption Orelse Unfold plus_fct minus_fct opp_fct mult_fct div_fct inv_fct comp id fct_cte pow_fct
  (* regles de differentiabilite *)
  (* PLUS *)
 |[|-(derivable_pt (plus_fct ?1 ?2) ?3)] -> Apply (derivable_pt_plus ?1 ?2 ?3); IsDiff_pt
@@ -439,15 +591,15 @@ Match Context With
  (* MULTIPLICATION *)
 |[|-(derivable_pt (mult_fct ?1 ?2) ?3)] -> Apply (derivable_pt_mult ?1 ?2 ?3); IsDiff_pt
   (* DIVISION *)
- |[|-(derivable_pt (div_fct ?1 ?2) ?3)] -> Apply (derivable_pt_div ?1 ?2 ?3); [IsDiff_pt | IsDiff_pt | Try Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct comp id fct_cte]
+ |[|-(derivable_pt (div_fct ?1 ?2) ?3)] -> Apply (derivable_pt_div ?1 ?2 ?3); [IsDiff_pt | IsDiff_pt | Try Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct comp pow_fct id fct_cte]
   (* INVERSION *)
- |[|-(derivable_pt (inv_fct ?1) ?2)] -> Apply (derivable_pt_inv ?1 ?2); [Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct comp id fct_cte | IsDiff_pt]
+ |[|-(derivable_pt (inv_fct ?1) ?2)] -> Apply (derivable_pt_inv ?1 ?2); [Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct comp pow_fct id fct_cte | IsDiff_pt]
  (* COMPOSITION *)
 |[|-(derivable_pt (comp ?1 ?2) ?3)] -> Apply (derivable_pt_comp ?2 ?1 ?3); IsDiff_pt
 |[_:(derivable_pt ?1 ?2)|-(derivable_pt ?1 ?2)] -> Assumption
 |[_:(derivable ?1) |- (derivable_pt ?1 ?2)] -> Cut (derivable ?1); [Intro HypDDPT; Apply HypDDPT | Assumption]
 |[|-True->(derivable_pt ? ?)] -> Intro HypTruE; Clear HypTruE; IsDiff_pt
-| _ -> Try Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp.
+| _ -> Try Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp pow_fct.
 
 (**********)
 Recursive Tactic Definition IsCont_glob :=
@@ -459,6 +611,7 @@ Match Context With
  |[|-(continuity sin)] -> Apply derivable_continuous; Apply derivable_sin
  |[|-(continuity cos)] -> Apply derivable_continuous; Apply derivable_cos
  |[|-(continuity exp)] -> Apply derivable_continuous; Apply derivable_exp
+ |[|-(continuity (pow_fct ?))] -> Unfold pow_fct; Apply derivable_continuous; Apply derivable_pow
  |[|-(continuity sinh)] -> Apply derivable_continuous; Apply derivable_sinh
  |[|-(continuity cosh)] -> Apply derivable_continuous; Apply derivable_cosh
  |[|-(continuity Rabsolu)] -> Apply continuity_Rabsolu
@@ -476,13 +629,13 @@ Match Context With
  (* MULTIPLICATION *)
 |[|-(continuity (mult_fct ?1 ?2))] -> Apply (continuity_mult ?1 ?2); Try IsCont_glob Orelse Assumption
   (* DIVISION *)
- |[|-(continuity (div_fct ?1 ?2))] -> Apply (continuity_div ?1 ?2); [Try IsCont_glob Orelse Assumption | Try IsCont_glob Orelse Assumption | Try Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte]
+ |[|-(continuity (div_fct ?1 ?2))] -> Apply (continuity_div ?1 ?2); [Try IsCont_glob Orelse Assumption | Try IsCont_glob Orelse Assumption | Try Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte pow_fct]
   (* COMPOSITION *)
  |[|-(continuity (comp ?1 ?2))] -> Apply (continuity_comp ?2 ?1); Try IsCont_glob Orelse Assumption
  |[_:(continuity ?1)|-(continuity ?1)] -> Assumption
  |[|-True->(continuity ?)] -> Intro HypTruE; Clear HypTruE; IsCont_glob
  |[_:(derivable ?1)|-(continuity ?1)] -> Apply derivable_continuous; Assumption
- | _ -> Try Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp.
+ | _ -> Try Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp pow_fct.
 
 (**********)
 Recursive Tactic Definition IsCont_pt :=
@@ -496,7 +649,8 @@ Match Context With
 |[|-(continuity_pt sinh ?)] -> Apply derivable_continuous_pt; Apply derivable_pt_sinh
 |[|-(continuity_pt cosh ?)] -> Apply derivable_continuous_pt; Apply derivable_pt_cosh
 |[|-(continuity_pt exp ?)] -> Apply derivable_continuous_pt; Apply derivable_pt_exp
-|[|-(continuity_pt sqrt ?1)] -> Apply continuity_pt_sqrt; Assumption Orelse Unfold plus_fct minus_fct opp_fct mult_fct div_fct inv_fct comp id fct_cte
+|[|-(continuity_pt (pow_fct ?) ?)] -> Unfold pow_fct; Apply derivable_continuous_pt; Apply derivable_pt_pow
+|[|-(continuity_pt sqrt ?1)] -> Apply continuity_pt_sqrt; Assumption Orelse Unfold plus_fct minus_fct opp_fct mult_fct div_fct inv_fct comp id fct_cte pow_fct
 |[|-(continuity_pt Rabsolu ?1)] -> Apply (continuity_Rabsolu ?1)
  (* regles de differentiabilite *)
  (* PLUS *)
@@ -510,9 +664,9 @@ Match Context With
  (* MULTIPLICATION *)
 |[|-(continuity_pt (mult_fct ?1 ?2) ?3)] -> Apply (continuity_pt_mult ?1 ?2 ?3); IsCont_pt
   (* DIVISION *)
- |[|-(continuity_pt (div_fct ?1 ?2) ?3)] -> Apply (continuity_pt_div ?1 ?2 ?3); [IsCont_pt | IsCont_pt | Try Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct comp id fct_cte]
+ |[|-(continuity_pt (div_fct ?1 ?2) ?3)] -> Apply (continuity_pt_div ?1 ?2 ?3); [IsCont_pt | IsCont_pt | Try Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct comp id fct_cte pow_fct]
   (* INVERSION *)
- |[|-(continuity_pt (inv_fct ?1) ?2)] -> Apply (continuity_pt_inv ?1 ?2); [IsCont_pt | Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct comp id fct_cte]
+ |[|-(continuity_pt (inv_fct ?1) ?2)] -> Apply (continuity_pt_inv ?1 ?2); [IsCont_pt | Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct comp id fct_cte pow_fct]
  (* COMPOSITION *)
 |[|-(continuity_pt (comp ?1 ?2) ?3)] -> Apply (continuity_pt_comp ?2 ?1 ?3); IsCont_pt
 |[_:(continuity_pt ?1 ?2)|-(continuity_pt ?1 ?2)] -> Assumption
@@ -520,7 +674,7 @@ Match Context With
 |[_:(derivable_pt ?1 ?2)|-(continuity_pt ?1 ?2)] -> Apply derivable_continuous_pt; Assumption
 |[_:(derivable ?1)|-(continuity_pt ?1 ?2)] -> Cut (continuity ?1); [Intro HypDDPT; Apply HypDDPT | Apply derivable_continuous; Assumption]
 |[|-True->(continuity_pt ? ?)] -> Intro HypTruE; Clear HypTruE; IsCont_pt
-| _ -> Try Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp.
+| _ -> Try Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp pow_fct.
 
 (**********)
 Recursive Tactic Definition RewTerm trm :=
@@ -580,6 +734,11 @@ Match trm With
  | [(fct_cte ?3)] -> '(fct_cte (?1 ?3))
  | _ -> '(comp ?1 p))
 | [PI] -> 'id
+| [(pow PI ?1)] -> '(pow_fct ?1)
+| [(pow ?1 ?2)] -> Let p = (RewTerm ?1) In 
+ (Match p With
+ | [(fct_cte ?3)] -> '(fct_cte (pow_fct ?2 ?3))
+ | _ -> '(comp (pow_fct ?2) p))
 | [?1]-> '(fct_cte ?1).
 
 (**********)