diff options
Diffstat (limited to 'theories7/Reals/Rpower.v')
| -rw-r--r-- | theories7/Reals/Rpower.v | 560 |
1 files changed, 0 insertions, 560 deletions
diff --git a/theories7/Reals/Rpower.v b/theories7/Reals/Rpower.v deleted file mode 100644 index 0acfa8d2..00000000 --- a/theories7/Reals/Rpower.v +++ /dev/null @@ -1,560 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: Rpower.v,v 1.1.2.1 2004/07/16 19:31:35 herbelin Exp $ i*) -(*i Due to L.Thery i*) - -(************************************************************) -(* Definitions of log and Rpower : R->R->R; main properties *) -(************************************************************) - -Require Rbase. -Require Rfunctions. -Require SeqSeries. -Require Rtrigo. -Require Ranalysis1. -Require Exp_prop. -Require Rsqrt_def. -Require R_sqrt. -Require MVT. -Require Ranalysis4. -V7only [Import R_scope.]. Open Local Scope R_scope. - -Lemma P_Rmin: (P : R -> Prop) (x, y : R) (P x) -> (P y) -> (P (Rmin x y)). -Intros P x y H1 H2; Unfold Rmin; Case (total_order_Rle x y); Intro; Assumption. -Qed. - -Lemma exp_le_3 : ``(exp 1)<=3``. -Assert exp_1 : ``(exp 1)<>0``. -Assert H0 := (exp_pos R1); Red; Intro; Rewrite H in H0; Elim (Rlt_antirefl ? H0). -Apply Rle_monotony_contra with ``/(exp 1)``. -Apply Rlt_Rinv; Apply exp_pos. -Rewrite <- Rinv_l_sym. -Apply Rle_monotony_contra with ``/3``. -Apply Rlt_Rinv; Sup0. -Rewrite Rmult_1r; Rewrite <- (Rmult_sym ``3``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1l; Replace ``/(exp 1)`` with ``(exp (-1))``. -Unfold exp; Case (exist_exp ``-1``); Intros; Simpl; Unfold exp_in in e; Assert H := (alternated_series_ineq [i:nat]``/(INR (fact i))`` x (S O)). -Cut ``(sum_f_R0 (tg_alt [([i:nat]``/(INR (fact i))``)]) (S (mult (S (S O)) (S O)))) <= x <= (sum_f_R0 (tg_alt [([i:nat]``/(INR (fact i))``)]) (mult (S (S O)) (S O)))``. -Intro; Elim H0; Clear H0; Intros H0 _; Simpl in H0; Unfold tg_alt in H0; Simpl in H0. -Replace ``/3`` with ``1*/1+ -1*1*/1+ -1*( -1*1)*/2+ -1*( -1*( -1*1))*/(2+1+1+1+1)``. -Apply H0. -Repeat Rewrite Rinv_R1; Repeat Rewrite Rmult_1r; Rewrite Ropp_mul1; Rewrite Rmult_1l; Rewrite Ropp_Ropp; Rewrite Rplus_Ropp_r; Rewrite Rmult_1r; Rewrite Rplus_Ol; Rewrite Rmult_1l; Apply r_Rmult_mult with ``6``. -Rewrite Rmult_Rplus_distr; Replace ``2+1+1+1+1`` with ``6``. -Rewrite <- (Rmult_sym ``/6``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym. -Rewrite Rmult_1l; Replace ``6`` with ``2*3``. -Do 2 Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym. -Rewrite Rmult_1r; Rewrite (Rmult_sym ``3``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym. -Ring. -DiscrR. -DiscrR. -Ring. -DiscrR. -Ring. -DiscrR. -Apply H. -Unfold Un_decreasing; Intros; Apply Rle_monotony_contra with ``(INR (fact n))``. -Apply INR_fact_lt_0. -Apply Rle_monotony_contra with ``(INR (fact (S n)))``. -Apply INR_fact_lt_0. -Rewrite <- Rinv_r_sym. -Rewrite Rmult_1r; Rewrite Rmult_sym; Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1r; Apply le_INR; Apply fact_growing; Apply le_n_Sn. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Assert H0 := (cv_speed_pow_fact R1); Unfold Un_cv; Unfold Un_cv in H0; Intros; Elim (H0 ? H1); Intros; Exists x0; Intros; Unfold R_dist in H2; Unfold R_dist; Replace ``/(INR (fact n))`` with ``(pow 1 n)/(INR (fact n))``. -Apply (H2 ? H3). -Unfold Rdiv; Rewrite pow1; Rewrite Rmult_1l; Reflexivity. -Unfold infinit_sum in e; Unfold Un_cv tg_alt; Intros; Elim (e ? H0); Intros; Exists x0; Intros; Replace (sum_f_R0 ([i:nat]``(pow ( -1) i)*/(INR (fact i))``) n) with (sum_f_R0 ([i:nat]``/(INR (fact i))*(pow ( -1) i)``) n). -Apply (H1 ? H2). -Apply sum_eq; Intros; Apply Rmult_sym. -Apply r_Rmult_mult with ``(exp 1)``. -Rewrite <- exp_plus; Rewrite Rplus_Ropp_r; Rewrite exp_0; Rewrite <- Rinv_r_sym. -Reflexivity. -Assumption. -Assumption. -DiscrR. -Assumption. -Qed. - -(******************************************************************) -(* Properties of Exp *) -(******************************************************************) - -Theorem exp_increasing: (x, y : R) ``x<y`` -> ``(exp x)<(exp y)``. -Intros x y H. -Assert H0 : (derivable exp). -Apply derivable_exp. -Assert H1 := (positive_derivative ? H0). -Unfold strict_increasing in H1. -Apply H1. -Intro. -Replace (derive_pt exp x0 (H0 x0)) with (exp x0). -Apply exp_pos. -Symmetry; Apply derive_pt_eq_0. -Apply (derivable_pt_lim_exp x0). -Apply H. -Qed. - -Theorem exp_lt_inv: (x, y : R) ``(exp x)<(exp y)`` -> ``x<y``. -Intros x y H; Case (total_order x y); [Intros H1 | Intros [H1|H1]]. -Assumption. -Rewrite H1 in H; Elim (Rlt_antirefl ? H). -Assert H2 := (exp_increasing ? ? H1). -Elim (Rlt_antirefl ? (Rlt_trans ? ? ? H H2)). -Qed. - -Lemma exp_ineq1 : (x:R) ``0<x`` -> ``1+x < (exp x)``. -Intros; Apply Rlt_anti_compatibility with ``-(exp 0)``; Rewrite <- (Rplus_sym (exp x)); Assert H0 := (MVT_cor1 exp R0 x derivable_exp H); Elim H0; Intros; Elim H1; Intros; Unfold Rminus in H2; Rewrite H2; Rewrite Ropp_O; Rewrite Rplus_Or; Replace (derive_pt exp x0 (derivable_exp x0)) with (exp x0). -Rewrite exp_0; Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Ol; Pattern 1 x; Rewrite <- Rmult_1r; Rewrite (Rmult_sym (exp x0)); Apply Rlt_monotony. -Apply H. -Rewrite <- exp_0; Apply exp_increasing; Elim H3; Intros; Assumption. -Symmetry; Apply derive_pt_eq_0; Apply derivable_pt_lim_exp. -Qed. - -Lemma ln_exists1 : (y:R) ``0<y``->``1<=y``->(sigTT R [z:R]``y==(exp z)``). -Intros; Pose f := [x:R]``(exp x)-y``; Cut ``(f 0)<=0``. -Intro; Cut (continuity f). -Intro; Cut ``0<=(f y)``. -Intro; Cut ``(f 0)*(f y)<=0``. -Intro; Assert X := (IVT_cor f R0 y H2 (Rlt_le ? ? H) H4); Elim X; Intros t H5; Apply existTT with t; Elim H5; Intros; Unfold f in H7; Apply Rminus_eq_right; Exact H7. -Pattern 2 R0; Rewrite <- (Rmult_Or (f y)); Rewrite (Rmult_sym (f R0)); Apply Rle_monotony; Assumption. -Unfold f; Apply Rle_anti_compatibility with y; Left; Apply Rlt_trans with ``1+y``. -Rewrite <- (Rplus_sym y); Apply Rlt_compatibility; Apply Rlt_R0_R1. -Replace ``y+((exp y)-y)`` with (exp y); [Apply (exp_ineq1 y H) | Ring]. -Unfold f; Change (continuity (minus_fct exp (fct_cte y))); Apply continuity_minus; [Apply derivable_continuous; Apply derivable_exp | Apply derivable_continuous; Apply derivable_const]. -Unfold f; Rewrite exp_0; Apply Rle_anti_compatibility with y; Rewrite Rplus_Or; Replace ``y+(1-y)`` with R1; [Apply H0 | Ring]. -Qed. - -(**********) -Lemma ln_exists : (y:R) ``0<y`` -> (sigTT R [z:R]``y==(exp z)``). -Intros; Case (total_order_Rle R1 y); Intro. -Apply (ln_exists1 ? H r). -Assert H0 : ``1<=/y``. -Apply Rle_monotony_contra with y. -Apply H. -Rewrite <- Rinv_r_sym. -Rewrite Rmult_1r; Left; Apply (not_Rle ? ? n). -Red; Intro; Rewrite H0 in H; Elim (Rlt_antirefl ? H). -Assert H1 : ``0</y``. -Apply Rlt_Rinv; Apply H. -Assert H2 := (ln_exists1 ? H1 H0); Elim H2; Intros; Apply existTT with ``-x``; Apply r_Rmult_mult with ``(exp x)/y``. -Unfold Rdiv; Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1r; Rewrite <- (Rmult_sym ``/y``); Rewrite Rmult_assoc; Rewrite <- exp_plus; Rewrite Rplus_Ropp_r; Rewrite exp_0; Rewrite Rmult_1r; Symmetry; Apply p. -Red; Intro; Rewrite H3 in H; Elim (Rlt_antirefl ? H). -Unfold Rdiv; Apply prod_neq_R0. -Assert H3 := (exp_pos x); Red; Intro; Rewrite H4 in H3; Elim (Rlt_antirefl ? H3). -Apply Rinv_neq_R0; Red; Intro; Rewrite H3 in H; Elim (Rlt_antirefl ? H). -Qed. - -(* Definition of log R+* -> R *) -Definition Rln [y:posreal] : R := Cases (ln_exists (pos y) (RIneq.cond_pos y)) of (existTT a b) => a end. - -(* Extension on R *) -Definition ln : R->R := [x:R](Cases (total_order_Rlt R0 x) of - (leftT a) => (Rln (mkposreal x a)) - | (rightT a) => R0 end). - -Lemma exp_ln : (x : R) ``0<x`` -> (exp (ln x)) == x. -Intros; Unfold ln; Case (total_order_Rlt R0 x); Intro. -Unfold Rln; Case (ln_exists (mkposreal x r) (RIneq.cond_pos (mkposreal x r))); Intros. -Simpl in e; Symmetry; Apply e. -Elim n; Apply H. -Qed. - -Theorem exp_inv: (x, y : R) (exp x) == (exp y) -> x == y. -Intros x y H; Case (total_order x y); [Intros H1 | Intros [H1|H1]]; Auto; Assert H2 := (exp_increasing ? ? H1); Rewrite H in H2; Elim (Rlt_antirefl ? H2). -Qed. - -Theorem exp_Ropp: (x : R) ``(exp (-x)) == /(exp x)``. -Intros x; Assert H : ``(exp x)<>0``. -Assert H := (exp_pos x); Red; Intro; Rewrite H0 in H; Elim (Rlt_antirefl ? H). -Apply r_Rmult_mult with r := (exp x). -Rewrite <- exp_plus; Rewrite Rplus_Ropp_r; Rewrite exp_0. -Apply Rinv_r_sym. -Apply H. -Apply H. -Qed. - -(******************************************************************) -(* Properties of Ln *) -(******************************************************************) - -Theorem ln_increasing: - (x, y : R) ``0<x`` -> ``x<y`` -> ``(ln x) < (ln y)``. -Intros x y H H0; Apply exp_lt_inv. -Repeat Rewrite exp_ln. -Apply H0. -Apply Rlt_trans with x; Assumption. -Apply H. -Qed. - -Theorem ln_exp: (x : R) (ln (exp x)) == x. -Intros x; Apply exp_inv. -Apply exp_ln. -Apply exp_pos. -Qed. - -Theorem ln_1: ``(ln 1) == 0``. -Rewrite <- exp_0; Rewrite ln_exp; Reflexivity. -Qed. - -Theorem ln_lt_inv: - (x, y : R) ``0<x`` -> ``0<y`` -> ``(ln x)<(ln y)`` -> ``x<y``. -Intros x y H H0 H1; Rewrite <- (exp_ln x); Try Rewrite <- (exp_ln y). -Apply exp_increasing; Apply H1. -Assumption. -Assumption. -Qed. - -Theorem ln_inv: (x, y : R) ``0<x`` -> ``0<y`` -> (ln x) == (ln y) -> x == y. -Intros x y H H0 H'0; Case (total_order x y); [Intros H1 | Intros [H1|H1]]; Auto. -Assert H2 := (ln_increasing ? ? H H1); Rewrite H'0 in H2; Elim (Rlt_antirefl ? H2). -Assert H2 := (ln_increasing ? ? H0 H1); Rewrite H'0 in H2; Elim (Rlt_antirefl ? H2). -Qed. - -Theorem ln_mult: (x, y : R) ``0<x`` -> ``0<y`` -> ``(ln (x*y)) == (ln x)+(ln y)``. -Intros x y H H0; Apply exp_inv. -Rewrite exp_plus. -Repeat Rewrite exp_ln. -Reflexivity. -Assumption. -Assumption. -Apply Rmult_lt_pos; Assumption. -Qed. - -Theorem ln_Rinv: (x : R) ``0<x`` -> ``(ln (/x)) == -(ln x)``. -Intros x H; Apply exp_inv; Repeat (Rewrite exp_ln Orelse Rewrite exp_Ropp). -Reflexivity. -Assumption. -Apply Rlt_Rinv; Assumption. -Qed. - -Theorem ln_continue: - (y : R) ``0<y`` -> (continue_in ln [x : R] (Rlt R0 x) y). -Intros y H. -Unfold continue_in limit1_in limit_in; Intros eps Heps. -Cut (Rlt R1 (exp eps)); [Intros H1 | Idtac]. -Cut (Rlt (exp (Ropp eps)) R1); [Intros H2 | Idtac]. -Exists - (Rmin (Rmult y (Rminus (exp eps) R1)) (Rmult y (Rminus R1 (exp (Ropp eps))))); - Split. -Red; Apply P_Rmin. -Apply Rmult_lt_pos. -Assumption. -Apply Rlt_anti_compatibility with R1. -Rewrite Rplus_Or; Replace ``(1+((exp eps)-1))`` with (exp eps); [Apply H1 | Ring]. -Apply Rmult_lt_pos. -Assumption. -Apply Rlt_anti_compatibility with ``(exp (-eps))``. -Rewrite Rplus_Or; Replace ``(exp ( -eps))+(1-(exp ( -eps)))`` with R1; [Apply H2 | Ring]. -Unfold dist R_met R_dist; Simpl. -Intros x ((H3, H4), H5). -Cut (Rmult y (Rmult x (Rinv y))) == x. -Intro Hxyy. -Replace (Rminus (ln x) (ln y)) with (ln (Rmult x (Rinv y))). -Case (total_order x y); [Intros Hxy | Intros [Hxy|Hxy]]. -Rewrite Rabsolu_left. -Apply Ropp_Rlt; Rewrite Ropp_Ropp. -Apply exp_lt_inv. -Rewrite exp_ln. -Apply Rlt_monotony_contra with z := y. -Apply H. -Rewrite Hxyy. -Apply Ropp_Rlt. -Apply Rlt_anti_compatibility with r := y. -Replace (Rplus y (Ropp (Rmult y (exp (Ropp eps))))) - with (Rmult y (Rminus R1 (exp (Ropp eps)))); [Idtac | Ring]. -Replace (Rplus y (Ropp x)) with (Rabsolu (Rminus x y)); [Idtac | Ring]. -Apply Rlt_le_trans with 1 := H5; Apply Rmin_r. -Rewrite Rabsolu_left; [Ring | Idtac]. -Apply (Rlt_minus ? ? Hxy). -Apply Rmult_lt_pos; [Apply H3 | Apply (Rlt_Rinv ? H)]. -Rewrite <- ln_1. -Apply ln_increasing. -Apply Rmult_lt_pos; [Apply H3 | Apply (Rlt_Rinv ? H)]. -Apply Rlt_monotony_contra with z := y. -Apply H. -Rewrite Hxyy; Rewrite Rmult_1r; Apply Hxy. -Rewrite Hxy; Rewrite Rinv_r. -Rewrite ln_1; Rewrite Rabsolu_R0; Apply Heps. -Red; Intro; Rewrite H0 in H; Elim (Rlt_antirefl ? H). -Rewrite Rabsolu_right. -Apply exp_lt_inv. -Rewrite exp_ln. -Apply Rlt_monotony_contra with z := y. -Apply H. -Rewrite Hxyy. -Apply Rlt_anti_compatibility with r := (Ropp y). -Replace (Rplus (Ropp y) (Rmult y (exp eps))) - with (Rmult y (Rminus (exp eps) R1)); [Idtac | Ring]. -Replace (Rplus (Ropp y) x) with (Rabsolu (Rminus x y)); [Idtac | Ring]. -Apply Rlt_le_trans with 1 := H5; Apply Rmin_l. -Rewrite Rabsolu_right; [Ring | Idtac]. -Left; Apply (Rgt_minus ? ? Hxy). -Apply Rmult_lt_pos; [Apply H3 | Apply (Rlt_Rinv ? H)]. -Rewrite <- ln_1. -Apply Rgt_ge; Red; Apply ln_increasing. -Apply Rlt_R0_R1. -Apply Rlt_monotony_contra with z := y. -Apply H. -Rewrite Hxyy; Rewrite Rmult_1r; Apply Hxy. -Rewrite ln_mult. -Rewrite ln_Rinv. -Ring. -Assumption. -Assumption. -Apply Rlt_Rinv; Assumption. -Rewrite (Rmult_sym x); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym. -Ring. -Red; Intro; Rewrite H0 in H; Elim (Rlt_antirefl ? H). -Apply Rlt_monotony_contra with (exp eps). -Apply exp_pos. -Rewrite <- exp_plus; Rewrite Rmult_1r; Rewrite Rplus_Ropp_r; Rewrite exp_0; Apply H1. -Rewrite <- exp_0. -Apply exp_increasing; Apply Heps. -Qed. - -(******************************************************************) -(* Definition of Rpower *) -(******************************************************************) - -Definition Rpower := [x : R] [y : R] ``(exp (y*(ln x)))``. - -Infix Local "^R" Rpower (at level 2, left associativity) : R_scope. - -(******************************************************************) -(* Properties of Rpower *) -(******************************************************************) - -Theorem Rpower_plus: - (x, y, z : R) ``(Rpower z (x+y)) == (Rpower z x)*(Rpower z y)``. -Intros x y z; Unfold Rpower. -Rewrite Rmult_Rplus_distrl; Rewrite exp_plus; Auto. -Qed. - -Theorem Rpower_mult: - (x, y, z : R) ``(Rpower (Rpower x y) z) == (Rpower x (y*z))``. -Intros x y z; Unfold Rpower. -Rewrite ln_exp. -Replace (Rmult z (Rmult y (ln x))) with (Rmult (Rmult y z) (ln x)). -Reflexivity. -Ring. -Qed. - -Theorem Rpower_O: (x : R) ``0<x`` -> ``(Rpower x 0) == 1``. -Intros x H; Unfold Rpower. -Rewrite Rmult_Ol; Apply exp_0. -Qed. - -Theorem Rpower_1: (x : R) ``0<x`` -> ``(Rpower x 1) == x``. -Intros x H; Unfold Rpower. -Rewrite Rmult_1l; Apply exp_ln; Apply H. -Qed. - -Theorem Rpower_pow: - (n : nat) (x : R) ``0<x`` -> (Rpower x (INR n)) == (pow x n). -Intros n; Elim n; Simpl; Auto; Fold INR. -Intros x H; Apply Rpower_O; Auto. -Intros n1; Case n1. -Intros H x H0; Simpl; Rewrite Rmult_1r; Apply Rpower_1; Auto. -Intros n0 H x H0; Rewrite Rpower_plus; Rewrite H; Try Rewrite Rpower_1; Try Apply Rmult_sym Orelse Assumption. -Qed. - -Theorem Rpower_lt: (x, y, z : R) ``1<x`` -> ``0<=y`` -> ``y<z`` -> ``(Rpower x y) < (Rpower x z)``. -Intros x y z H H0 H1. -Unfold Rpower. -Apply exp_increasing. -Apply Rlt_monotony_r. -Rewrite <- ln_1; Apply ln_increasing. -Apply Rlt_R0_R1. -Apply H. -Apply H1. -Qed. - -Theorem Rpower_sqrt: (x : R) ``0<x`` -> ``(Rpower x (/2)) == (sqrt x)``. -Intros x H. -Apply ln_inv. -Unfold Rpower; Apply exp_pos. -Apply sqrt_lt_R0; Apply H. -Apply r_Rmult_mult with (INR (S (S O))). -Apply exp_inv. -Fold Rpower. -Cut (Rpower (Rpower x (Rinv (Rplus R1 R1))) (INR (S (S O)))) == (Rpower (sqrt x) (INR (S (S O)))). -Unfold Rpower; Auto. -Rewrite Rpower_mult. -Rewrite Rinv_l. -Replace R1 with (INR (S O)); Auto. -Repeat Rewrite Rpower_pow; Simpl. -Pattern 1 x; Rewrite <- (sqrt_sqrt x (Rlt_le ? ? H)). -Ring. -Apply sqrt_lt_R0; Apply H. -Apply H. -Apply not_O_INR; Discriminate. -Apply not_O_INR; Discriminate. -Qed. - -Theorem Rpower_Ropp: (x, y : R) ``(Rpower x (-y)) == /(Rpower x y)``. -Unfold Rpower. -Intros x y; Rewrite Ropp_mul1. -Apply exp_Ropp. -Qed. - -Theorem Rle_Rpower: (e,n,m : R) ``1<e`` -> ``0<=n`` -> ``n<=m`` -> ``(Rpower e n)<=(Rpower e m)``. -Intros e n m H H0 H1; Case H1. -Intros H2; Left; Apply Rpower_lt; Assumption. -Intros H2; Rewrite H2; Right; Reflexivity. -Qed. - -Theorem ln_lt_2: ``/2<(ln 2)``. -Apply Rlt_monotony_contra with z := (Rplus R1 R1). -Sup0. -Rewrite Rinv_r. -Apply exp_lt_inv. -Apply Rle_lt_trans with 1 := exp_le_3. -Change (Rlt (Rplus R1 (Rplus R1 R1)) (Rpower (Rplus R1 R1) (Rplus R1 R1))). -Repeat Rewrite Rpower_plus; Repeat Rewrite Rpower_1. -Repeat Rewrite Rmult_Rplus_distrl; Repeat Rewrite Rmult_Rplus_distr; - Repeat Rewrite Rmult_1l. -Pattern 1 ``3``; Rewrite <- Rplus_Or; Replace ``2+2`` with ``3+1``; [Apply Rlt_compatibility; Apply Rlt_R0_R1 | Ring]. -Sup0. -DiscrR. -Qed. - -(**************************************) -(* Differentiability of Ln and Rpower *) -(**************************************) - -Theorem limit1_ext: (f, g : R -> R)(D : R -> Prop)(l, x : R) ((x : R) (D x) -> (f x) == (g x)) -> (limit1_in f D l x) -> (limit1_in g D l x). -Intros f g D l x H; Unfold limit1_in limit_in. -Intros H0 eps H1; Case (H0 eps); Auto. -Intros x0 (H2, H3); Exists x0; Split; Auto. -Intros x1 (H4, H5); Rewrite <- H; Auto. -Qed. - -Theorem limit1_imp: (f : R -> R)(D, D1 : R -> Prop)(l, x : R) ((x : R) (D1 x) -> (D x)) -> (limit1_in f D l x) -> (limit1_in f D1 l x). -Intros f D D1 l x H; Unfold limit1_in limit_in. -Intros H0 eps H1; Case (H0 eps H1); Auto. -Intros alpha (H2, H3); Exists alpha; Split; Auto. -Intros d (H4, H5); Apply H3; Split; Auto. -Qed. - -Theorem Rinv_Rdiv: (x, y : R) ``x<>0`` -> ``y<>0`` -> ``/(x/y) == y/x``. -Intros x y H1 H2; Unfold Rdiv; Rewrite Rinv_Rmult. -Rewrite Rinv_Rinv. -Apply Rmult_sym. -Assumption. -Assumption. -Apply Rinv_neq_R0; Assumption. -Qed. - -Theorem Dln: (y : R) ``0<y`` -> (D_in ln Rinv [x:R]``0<x`` y). -Intros y Hy; Unfold D_in. -Apply limit1_ext with f := [x : R](Rinv (Rdiv (Rminus (exp (ln x)) (exp (ln y))) (Rminus (ln x) (ln y)))). -Intros x (HD1, HD2); Repeat Rewrite exp_ln. -Unfold Rdiv; Rewrite Rinv_Rmult. -Rewrite Rinv_Rinv. -Apply Rmult_sym. -Apply Rminus_eq_contra. -Red; Intros H2; Case HD2. -Symmetry; Apply (ln_inv ? ? HD1 Hy H2). -Apply Rminus_eq_contra; Apply (not_sym ? ? HD2). -Apply Rinv_neq_R0; Apply Rminus_eq_contra; Red; Intros H2; Case HD2; Apply ln_inv; Auto. -Assumption. -Assumption. -Apply limit_inv with f := [x : R] (Rdiv (Rminus (exp (ln x)) (exp (ln y))) (Rminus (ln x) (ln y))). -Apply limit1_imp with f := [x : R] ([x : R] (Rdiv (Rminus (exp x) (exp (ln y))) (Rminus x (ln y))) (ln x)) D := (Dgf (D_x [x : R] (Rlt R0 x) y) (D_x [x : R] True (ln y)) ln). -Intros x (H1, H2); Split. -Split; Auto. -Split; Auto. -Red; Intros H3; Case H2; Apply ln_inv; Auto. -Apply limit_comp with l := (ln y) g := [x : R] (Rdiv (Rminus (exp x) (exp (ln y))) (Rminus x (ln y))) f := ln. -Apply ln_continue; Auto. -Assert H0 := (derivable_pt_lim_exp (ln y)); Unfold derivable_pt_lim in H0; Unfold limit1_in; Unfold limit_in; Simpl; Unfold R_dist; Intros; Elim (H0 ? H); Intros; Exists (pos x); Split. -Apply (RIneq.cond_pos x). -Intros; Pattern 3 y; Rewrite <- exp_ln. -Pattern 1 x0; Replace x0 with ``(ln y)+(x0-(ln y))``; [Idtac | Ring]. -Apply H1. -Elim H2; Intros H3 _; Unfold D_x in H3; Elim H3; Clear H3; Intros _ H3; Apply Rminus_eq_contra; Apply not_sym; Apply H3. -Elim H2; Clear H2; Intros _ H2; Apply H2. -Assumption. -Red; Intro; Rewrite H in Hy; Elim (Rlt_antirefl ? Hy). -Qed. - -Lemma derivable_pt_lim_ln : (x:R) ``0<x`` -> (derivable_pt_lim ln x ``/x``). -Intros; Assert H0 := (Dln x H); Unfold D_in in H0; Unfold limit1_in in H0; Unfold limit_in in H0; Simpl in H0; Unfold R_dist in H0; Unfold derivable_pt_lim; Intros; Elim (H0 ? H1); Intros; Elim H2; Clear H2; Intros; Pose alp := (Rmin x0 ``x/2``); Assert H4 : ``0<alp``. -Unfold alp; Unfold Rmin; Case (total_order_Rle x0 ``x/2``); Intro. -Apply H2. -Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0]. -Exists (mkposreal ? H4); Intros; Pattern 2 h; Replace h with ``(x+h)-x``; [Idtac | Ring]. -Apply H3; Split. -Unfold D_x; Split. -Case (case_Rabsolu h); Intro. -Assert H7 : ``(Rabsolu h)<x/2``. -Apply Rlt_le_trans with alp. -Apply H6. -Unfold alp; Apply Rmin_r. -Apply Rlt_trans with ``x/2``. -Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0]. -Rewrite Rabsolu_left in H7. -Apply Rlt_anti_compatibility with ``-h-x/2``. -Replace ``-h-x/2+x/2`` with ``-h``; [Idtac | Ring]. -Pattern 2 x; Rewrite double_var. -Replace ``-h-x/2+(x/2+x/2+h)`` with ``x/2``; [Apply H7 | Ring]. -Apply r. -Apply gt0_plus_ge0_is_gt0; [Assumption | Apply Rle_sym2; Apply r]. -Apply not_sym; Apply Rminus_not_eq; Replace ``x+h-x`` with h; [Apply H5 | Ring]. -Replace ``x+h-x`` with h; [Apply Rlt_le_trans with alp; [Apply H6 | Unfold alp; Apply Rmin_l] | Ring]. -Qed. - -Theorem D_in_imp: (f, g : R -> R)(D, D1 : R -> Prop)(x : R) ((x : R) (D1 x) -> (D x)) -> (D_in f g D x) -> (D_in f g D1 x). -Intros f g D D1 x H; Unfold D_in. -Intros H0; Apply limit1_imp with D := (D_x D x); Auto. -Intros x1 (H1, H2); Split; Auto. -Qed. - -Theorem D_in_ext: (f, g, h : R -> R)(D : R -> Prop) (x : R) (f x) == (g x) -> (D_in h f D x) -> (D_in h g D x). -Intros f g h D x H; Unfold D_in. -Rewrite H; Auto. -Qed. - -Theorem Dpower: (y, z : R) ``0<y`` -> (D_in [x:R](Rpower x z) [x:R](Rmult z (Rpower x (Rminus z R1))) [x:R]``0<x`` y). -Intros y z H; Apply D_in_imp with D := (Dgf [x : R] (Rlt R0 x) [x : R] True ln). -Intros x H0; Repeat Split. -Assumption. -Apply D_in_ext with f := [x : R] (Rmult (Rinv x) (Rmult z (exp (Rmult z (ln x))))). -Unfold Rminus; Rewrite Rpower_plus; Rewrite Rpower_Ropp; Rewrite (Rpower_1 ? H); Ring. -Apply Dcomp with f := ln g := [x : R] (exp (Rmult z x)) df := Rinv dg := [x : R] (Rmult z (exp (Rmult z x))). -Apply (Dln ? H). -Apply D_in_imp with D := (Dgf [x : R] True [x : R] True [x : R] (Rmult z x)). -Intros x H1; Repeat Split; Auto. -Apply (Dcomp [_ : R] True [_ : R] True [x : ?] z exp [x : R] (Rmult z x) exp); Simpl. -Apply D_in_ext with f := [x : R] (Rmult z R1). -Apply Rmult_1r. -Apply (Dmult_const [x : ?] True [x : ?] x [x : ?] R1); Apply Dx. -Assert H0 := (derivable_pt_lim_D_in exp exp ``z*(ln y)``); Elim H0; Clear H0; Intros _ H0; Apply H0; Apply derivable_pt_lim_exp. -Qed. - -Theorem derivable_pt_lim_power: (x, y : R) (Rlt R0 x) -> (derivable_pt_lim [x : ?] (Rpower x y) x (Rmult y (Rpower x (Rminus y R1)))). -Intros x y H. -Unfold Rminus; Rewrite Rpower_plus. -Rewrite Rpower_Ropp. -Rewrite Rpower_1; Auto. -Rewrite <- Rmult_assoc. -Unfold Rpower. -Apply derivable_pt_lim_comp with f1 := ln f2 := [x : ?] (exp (Rmult y x)). -Apply derivable_pt_lim_ln; Assumption. -Rewrite (Rmult_sym y). -Apply derivable_pt_lim_comp with f1 := [x : ?] (Rmult y x) f2 := exp. -Pattern 2 y; Replace y with (Rplus (Rmult R0 (ln x)) (Rmult y R1)). -Apply derivable_pt_lim_mult with f1 := [x : R] y f2 := [x : R] x. -Apply derivable_pt_lim_const with a := y. -Apply derivable_pt_lim_id. -Ring. -Apply derivable_pt_lim_exp. -Qed. |