diff options
Diffstat (limited to 'theories/Reals/Ratan.v')
| -rw-r--r-- | theories/Reals/Ratan.v | 27 |
1 files changed, 18 insertions, 9 deletions
diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v index 096c75fe..68718db0 100644 --- a/theories/Reals/Ratan.v +++ b/theories/Reals/Ratan.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -18,6 +18,7 @@ Require Import SeqProp. Require Import Ranalysis5. Require Import SeqSeries. Require Import PartSum. +Require Import Omega. Local Open Scope R_scope. @@ -449,9 +450,9 @@ fourier. Qed. Definition frame_tan y : {x | 0 < x < PI/2 /\ Rabs y < tan x}. -destruct (total_order_T (Rabs y) 1). - assert (yle1 : Rabs y <= 1) by (destruct s; fourier). - clear s; exists 1; split;[split; [exact Rlt_0_1 | exact PI2_1] | ]. +destruct (total_order_T (Rabs y) 1) as [Hs|Hgt]. + assert (yle1 : Rabs y <= 1) by (destruct Hs; fourier). + clear Hs; exists 1; split;[split; [exact Rlt_0_1 | exact PI2_1] | ]. apply Rle_lt_trans with (1 := yle1); exact tan_1_gt_1. assert (0 < / (Rabs y + 1)). apply Rinv_0_lt_compat; fourier. @@ -529,7 +530,7 @@ split. assumption. replace (/(Rabs y + 1)) with (2 * u). fourier. - unfold u; field; apply Rgt_not_eq; clear -r; fourier. + unfold u; field; apply Rgt_not_eq; clear -Hgt; fourier. solve[discrR]. apply Rgt_not_eq; assumption. unfold tan. @@ -735,6 +736,16 @@ replace (Rsqr x) with (x ^ 2) by (unfold Rsqr; ring). reflexivity. Qed. +Lemma derivable_pt_lim_atan : + forall x, derivable_pt_lim atan x (/(1 + x^2)). +Proof. +intros x. +apply derive_pt_eq_1 with (derivable_pt_atan x). +replace (x ^ 2) with (x * x) by ring. +rewrite <- (Rmult_1_l (Rinv _)). +apply derive_pt_atan. +Qed. + (** * Definition of the arctangent function as the sum of the arctan power series *) (* Proof taken from Guillaume Melquiond's interval package for Coq *) @@ -818,13 +829,11 @@ intros x Hx eps Heps. apply Rle_lt_trans with (/ INR (2 * N + 1))%R. unfold Rdiv. rewrite Rmult_1_l. - apply Rle_Rinv. + apply Rinv_le_contravar. apply lt_INR_0. omega. - replace 0 with (INR 0) by intuition. - apply lt_INR. + apply le_INR. omega. - intuition. rewrite <- (Rinv_involutive eps). apply Rinv_lt_contravar. apply Rmult_lt_0_compat. |