diff options
Diffstat (limited to 'theories/Reals/Rpower.v')
| -rw-r--r-- | theories/Reals/Rpower.v | 79 |
1 files changed, 41 insertions, 38 deletions
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index b3ce6fa3..c6fac951 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (*i Due to L.Thery i*) @@ -55,25 +57,8 @@ Proof. simpl in H0. replace (/ 3) with (1 * / 1 + -1 * 1 * / 1 + -1 * (-1 * 1) * / 2 + - -1 * (-1 * (-1 * 1)) * / (2 + 1 + 1 + 1 + 1)). + -1 * (-1 * (-1 * 1)) * / (2 + 1 + 1 + 1 + 1)) by field. apply H0. - repeat rewrite Rinv_1; repeat rewrite Rmult_1_r; - rewrite Ropp_mult_distr_l_reverse; rewrite Rmult_1_l; - rewrite Ropp_involutive; rewrite Rplus_opp_r; rewrite Rmult_1_r; - rewrite Rplus_0_l; rewrite Rmult_1_l; apply Rmult_eq_reg_l with 6. - rewrite Rmult_plus_distr_l; replace (2 + 1 + 1 + 1 + 1) with 6. - rewrite <- (Rmult_comm (/ 6)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym. - rewrite Rmult_1_l; replace 6 with 6. - do 2 rewrite Rmult_assoc; rewrite <- Rinv_r_sym. - rewrite Rmult_1_r; rewrite (Rmult_comm 3); rewrite <- Rmult_assoc; - rewrite <- Rinv_r_sym. - ring. - discrR. - discrR. - ring. - discrR. - ring. - discrR. apply H. unfold Un_decreasing; intros; apply Rmult_le_reg_l with (INR (fact n)). @@ -448,9 +433,9 @@ Proof. Qed. Theorem Rpower_lt : - forall x y z:R, 1 < x -> 0 <= y -> y < z -> x ^R y < x ^R z. + forall x y z:R, 1 < x -> y < z -> x ^R y < x ^R z. Proof. - intros x y z H H0 H1. + intros x y z H H1. unfold Rpower. apply exp_increasing. apply Rmult_lt_compat_r. @@ -473,7 +458,7 @@ Proof. unfold Rpower; auto. rewrite Rpower_mult. rewrite Rinv_l. - replace 1 with (INR 1); auto. + change 1 with (INR 1). repeat rewrite Rpower_pow; simpl. pattern x at 1; rewrite <- (sqrt_sqrt x (Rlt_le _ _ H)). ring. @@ -490,12 +475,28 @@ Proof. apply exp_Ropp. Qed. +Lemma powerRZ_Rpower x z : (0 < x)%R -> powerRZ x z = Rpower x (IZR z). +Proof. + intros Hx. + assert (x <> 0)%R + by now intros Habs; rewrite Habs in Hx; apply (Rlt_irrefl 0). + destruct (intP z). + - now rewrite Rpower_O. + - rewrite <- pow_powerRZ, <- Rpower_pow by assumption. + now rewrite INR_IZR_INZ. + - rewrite opp_IZR, Rpower_Ropp. + rewrite powerRZ_neg, powerRZ_inv by assumption. + now rewrite <- pow_powerRZ, <- INR_IZR_INZ, Rpower_pow. +Qed. + Theorem Rle_Rpower : - forall e n m:R, 1 < e -> 0 <= n -> n <= m -> e ^R n <= e ^R m. + forall e n m:R, 1 <= e -> n <= m -> e ^R n <= e ^R m. Proof. - intros e n m H H0 H1; case H1. - intros H2; left; apply Rpower_lt; assumption. - intros H2; rewrite H2; right; reflexivity. + intros e n m [H | H]; intros H1. + case H1. + intros H2; left; apply Rpower_lt; assumption. + intros H2; rewrite H2; right; reflexivity. + now rewrite <- H; unfold Rpower; rewrite ln_1, !Rmult_0_r; apply Rle_refl. Qed. Theorem ln_lt_2 : / 2 < ln 2. @@ -505,12 +506,9 @@ Proof. rewrite Rinv_r. apply exp_lt_inv. apply Rle_lt_trans with (1 := exp_le_3). - change (3 < 2 ^R 2). + change (3 < 2 ^R (1 + 1)). repeat rewrite Rpower_plus; repeat rewrite Rpower_1. - repeat rewrite Rmult_plus_distr_r; repeat rewrite Rmult_plus_distr_l; - repeat rewrite Rmult_1_l. - pattern 3 at 1; rewrite <- Rplus_0_r; replace (2 + 2) with (3 + 1); - [ apply Rplus_lt_compat_l; apply Rlt_0_1 | ring ]. + now apply (IZR_lt 3 4). prove_sup0. discrR. Qed. @@ -713,13 +711,18 @@ intros x y z x0 y0; unfold Rpower. rewrite <- exp_plus, ln_mult, Rmult_plus_distr_l; auto. Qed. -Lemma Rle_Rpower_l a b c: 0 <= c -> 0 < a <= b -> Rpower a c <= Rpower b c. +Lemma Rlt_Rpower_l a b c: 0 < c -> 0 < a < b -> a ^R c < b ^R c. +Proof. +intros c0 [a0 ab]; apply exp_increasing. +now apply Rmult_lt_compat_l; auto; apply ln_increasing; fourier. +Qed. + +Lemma Rle_Rpower_l a b c: 0 <= c -> 0 < a <= b -> a ^R c <= b ^R c. Proof. intros [c0 | c0]; [ | intros; rewrite <- c0, !Rpower_O; [apply Rle_refl | |] ]. intros [a0 [ab|ab]]. - left; apply exp_increasing. - now apply Rmult_lt_compat_l; auto; apply ln_increasing; fourier. + now apply Rlt_le, Rlt_Rpower_l;[ | split]; fourier. rewrite ab; apply Rle_refl. apply Rlt_le_trans with a; tauto. tauto. @@ -732,7 +735,7 @@ Definition arcsinh x := ln (x + sqrt (x ^ 2 + 1)). Lemma arcsinh_sinh : forall x, arcsinh (sinh x) = x. intros x; unfold sinh, arcsinh. assert (Rminus_eq_0 : forall r, r - r = 0) by (intros; ring). -pattern 1 at 5; rewrite <- exp_0, <- (Rminus_eq_0 x); unfold Rminus. +rewrite <- exp_0, <- (Rminus_eq_0 x); unfold Rminus. rewrite exp_plus. match goal with |- context[sqrt ?a] => replace a with (((exp x + exp(-x))/2)^2) by field |