|
(************************************************************************)
(* * 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 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
Require Import Rbase.
Require Import Rfunctions.
Require Import Ranalysis1.
Require Import R_sqrt.
Local Open Scope R_scope.
(**********)
Lemma sqrt_var_maj :
forall h:R, Rabs h <= 1 -> Rabs (sqrt (1 + h) - 1) <= Rabs h.
Proof.
intros; cut (0 <= 1 + h).
intro; apply Rle_trans with (Rabs (sqrt (Rsqr (1 + h)) - 1)).
destruct (total_order_T h 0) as [[Hlt|Heq]|Hgt].
repeat rewrite Rabs_left.
unfold Rminus; do 2 rewrite <- (Rplus_comm (-1)).
change (-1) with (-(1)).
do 2 rewrite Ropp_plus_distr; rewrite Ropp_involutive;
apply Rplus_le_compat_l.
apply Ropp_le_contravar; apply sqrt_le_1.
apply Rle_0_sqr.
apply H0.
pattern (1 + h) at 2; rewrite <- Rmult_1_r; unfold Rsqr;
apply Rmult_le_compat_l.
apply H0.
pattern 1 at 2; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left;
assumption.
apply Rplus_lt_reg_l with 1; rewrite Rplus_0_r; rewrite Rplus_comm;
unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_l;
rewrite Rplus_0_r.
pattern 1 at 2; rewrite <- sqrt_1; apply sqrt_lt_1.
apply Rle_0_sqr.
left; apply Rlt_0_1.
pattern 1 at 2; rewrite <- Rsqr_1; apply Rsqr_incrst_1.
pattern 1 at 2; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l;
assumption.
apply H0.
left; apply Rlt_0_1.
apply Rplus_lt_reg_l with 1; rewrite Rplus_0_r; rewrite Rplus_comm;
unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_l;
rewrite Rplus_0_r.
pattern 1 at 2; rewrite <- sqrt_1; apply sqrt_lt_1.
apply H0.
left; apply Rlt_0_1.
pattern 1 at 2; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l;
assumption.
rewrite Heq; rewrite Rplus_0_r; rewrite Rsqr_1; rewrite sqrt_1; right;
reflexivity.
repeat rewrite Rabs_right.
unfold Rminus; do 2 rewrite <- (Rplus_comm (-1));
apply Rplus_le_compat_l.
apply sqrt_le_1.
apply H0.
apply Rle_0_sqr.
pattern (1 + h) at 1; rewrite <- Rmult_1_r; unfold Rsqr;
apply Rmult_le_compat_l.
apply H0.
pattern 1 at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left;
assumption.
apply Rle_ge; apply Rplus_le_reg_l with 1.
rewrite Rplus_0_r; rewrite Rplus_comm; unfold Rminus;
rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r.
pattern 1 at 1; rewrite <- sqrt_1; apply sqrt_le_1.
left; apply Rlt_0_1.
apply Rle_0_sqr.
pattern 1 at 1; rewrite <- Rsqr_1; apply Rsqr_incr_1.
pattern 1 at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left;
assumption.
left; apply Rlt_0_1.
apply H0.
apply Rle_ge; left; apply Rplus_lt_reg_l with 1.
rewrite Rplus_0_r; rewrite Rplus_comm; unfold Rminus;
rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r.
pattern 1 at 1; rewrite <- sqrt_1; apply sqrt_lt_1.
left; apply Rlt_0_1.
apply H0.
pattern 1 at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l;
assumption.
rewrite sqrt_Rsqr.
replace (1 + h - 1) with h; [ right; reflexivity | ring ].
apply H0.
destruct (total_order_T h 0) as [[Hlt|Heq]|Hgt].
rewrite (Rabs_left h Hlt) in H.
apply Rplus_le_reg_l with (- h).
rewrite Rplus_0_r; rewrite Rplus_comm; rewrite Rplus_assoc;
rewrite Rplus_opp_r; rewrite Rplus_0_r; exact H.
left; rewrite Heq; rewrite Rplus_0_r; apply Rlt_0_1.
left; apply Rplus_lt_0_compat.
apply Rlt_0_1.
apply Hgt.
Qed.
(** sqrt is continuous in 1 *)
Lemma sqrt_continuity_pt_R1 : continuity_pt sqrt 1.
Proof.
unfold continuity_pt; unfold continue_in;
unfold limit1_in; unfold limit_in;
unfold dist; simpl; unfold R_dist;
intros.
set (alpha := Rmin eps 1).
exists alpha; intros.
split.
unfold alpha; unfold Rmin; case (Rle_dec eps 1); intro.
assumption.
apply Rlt_0_1.
intros; elim H0; intros.
rewrite sqrt_1; replace x with (1 + (x - 1)); [ idtac | ring ];
apply Rle_lt_trans with (Rabs (x - 1)).
apply sqrt_var_maj.
apply Rle_trans with alpha.
left; apply H2.
unfold alpha; apply Rmin_r.
apply Rlt_le_trans with alpha;
[ apply H2 | unfold alpha; apply Rmin_l ].
Qed.
(** sqrt is continuous forall x>0 *)
Lemma sqrt_continuity_pt : forall x:R, 0 < x -> continuity_pt sqrt x.
Proof.
intros; generalize sqrt_continuity_pt_R1.
unfold continuity_pt; unfold continue_in;
unfold limit1_in; unfold limit_in;
unfold dist; simpl; unfold R_dist;
intros.
cut (0 < eps / sqrt x).
intro; elim (H0 _ H2); intros alp_1 H3.
elim H3; intros.
set (alpha := alp_1 * x).
exists (Rmin alpha x); intros.
split.
change (0 < Rmin alpha x); unfold Rmin;
case (Rle_dec alpha x); intro.
unfold alpha; apply Rmult_lt_0_compat; assumption.
apply H.
intros; replace x0 with (x + (x0 - x)); [ idtac | ring ];
replace (sqrt (x + (x0 - x)) - sqrt x) with
(sqrt x * (sqrt (1 + (x0 - x) / x) - sqrt 1)).
rewrite Rabs_mult; rewrite (Rabs_right (sqrt x)).
apply Rmult_lt_reg_l with (/ sqrt x).
apply Rinv_0_lt_compat; apply sqrt_lt_R0; assumption.
rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym.
rewrite Rmult_1_l; rewrite Rmult_comm.
unfold Rdiv in H5.
case (Req_dec x x0); intro.
rewrite H7; unfold Rminus, Rdiv; rewrite Rplus_opp_r;
rewrite Rmult_0_l; rewrite Rplus_0_r; rewrite Rplus_opp_r;
rewrite Rabs_R0.
apply Rmult_lt_0_compat.
assumption.
apply Rinv_0_lt_compat; rewrite <- H7; apply sqrt_lt_R0; assumption.
apply H5.
split.
unfold D_x, no_cond.
split.
trivial.
red; intro.
cut ((x0 - x) * / x = 0).
intro.
elim (Rmult_integral _ _ H9); intro.
elim H7.
apply (Rminus_diag_uniq_sym _ _ H10).
assert (H11 := Rmult_eq_0_compat_r _ x H10).
rewrite <- Rinv_l_sym in H11.
elim R1_neq_R0; exact H11.
red; intro; rewrite H12 in H; elim (Rlt_irrefl _ H).
symmetry ; apply Rplus_eq_reg_l with 1; rewrite Rplus_0_r;
unfold Rdiv in H8; exact H8.
unfold Rminus; rewrite Rplus_comm; rewrite <- Rplus_assoc;
rewrite Rplus_opp_l; rewrite Rplus_0_l; elim H6; intros.
unfold Rdiv; rewrite Rabs_mult.
rewrite Rabs_Rinv.
rewrite (Rabs_right x).
rewrite Rmult_comm; apply Rmult_lt_reg_l with x.
apply H.
rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym.
rewrite Rmult_1_l; rewrite Rmult_comm; fold alpha.
apply Rlt_le_trans with (Rmin alpha x).
apply H9.
apply Rmin_l.
red; intro; rewrite H10 in H; elim (Rlt_irrefl _ H).
apply Rle_ge; left; apply H.
red; intro; rewrite H10 in H; elim (Rlt_irrefl _ H).
assert (H7 := sqrt_lt_R0 x H).
red; intro; rewrite H8 in H7; elim (Rlt_irrefl _ H7).
apply Rle_ge; apply sqrt_positivity.
left; apply H.
unfold Rminus; rewrite Rmult_plus_distr_l;
rewrite Ropp_mult_distr_r_reverse; repeat rewrite <- sqrt_mult.
rewrite Rmult_1_r; rewrite Rmult_plus_distr_l; rewrite Rmult_1_r;
unfold Rdiv; rewrite Rmult_comm; rewrite Rmult_assoc;
rewrite <- Rinv_l_sym.
rewrite Rmult_1_r; reflexivity.
red; intro; rewrite H7 in H; elim (Rlt_irrefl _ H).
left; apply H.
left; apply Rlt_0_1.
left; apply H.
elim H6; intros.
destruct (Rcase_abs (x0 - x)) as [Hlt|Hgt].
rewrite (Rabs_left (x0 - x) Hlt) in H8.
rewrite Rplus_comm.
apply Rplus_le_reg_l with (- ((x0 - x) / x)).
rewrite Rplus_0_r; rewrite <- Rplus_assoc; rewrite Rplus_opp_l;
rewrite Rplus_0_l; unfold Rdiv; rewrite <- Ropp_mult_distr_l_reverse.
apply Rmult_le_reg_l with x.
apply H.
rewrite Rmult_1_r; rewrite Rmult_comm; rewrite Rmult_assoc;
rewrite <- Rinv_l_sym.
rewrite Rmult_1_r; left; apply Rlt_le_trans with (Rmin alpha x).
apply H8.
apply Rmin_r.
red; intro; rewrite H9 in H; elim (Rlt_irrefl _ H).
apply Rplus_le_le_0_compat.
left; apply Rlt_0_1.
unfold Rdiv; apply Rmult_le_pos.
apply Rge_le; exact Hgt.
left; apply Rinv_0_lt_compat; apply H.
unfold Rdiv; apply Rmult_lt_0_compat.
apply H1.
apply Rinv_0_lt_compat; apply sqrt_lt_R0; apply H.
Qed.
(** sqrt is derivable for all x>0 *)
Lemma derivable_pt_lim_sqrt :
forall x:R, 0 < x -> derivable_pt_lim sqrt x (/ (2 * sqrt x)).
Proof.
intros; set (g := fun h:R => sqrt x + sqrt (x + h)).
cut (continuity_pt g 0).
intro; cut (g 0 <> 0).
intro; assert (H2 := continuity_pt_inv g 0 H0 H1).
unfold derivable_pt_lim; intros; unfold continuity_pt in H2;
unfold continue_in in H2; unfold limit1_in in H2;
unfold limit_in in H2; simpl in H2; unfold R_dist in H2.
elim (H2 eps H3); intros alpha H4.
elim H4; intros.
set (alpha1 := Rmin alpha x).
cut (0 < alpha1).
intro; exists (mkposreal alpha1 H7); intros.
replace ((sqrt (x + h) - sqrt x) / h) with (/ (sqrt x + sqrt (x + h))).
unfold inv_fct, g in H6; replace (2 * sqrt x) with (sqrt x + sqrt (x + 0)).
apply H6.
split.
unfold D_x, no_cond.
split.
trivial.
apply (not_eq_sym (A:=R)); exact H8.
unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r;
apply Rlt_le_trans with alpha1.
exact H9.
unfold alpha1; apply Rmin_l.
rewrite Rplus_0_r; ring.
cut (0 <= x + h).
intro; cut (0 < sqrt x + sqrt (x + h)).
intro; apply Rmult_eq_reg_l with (sqrt x + sqrt (x + h)).
rewrite <- Rinv_r_sym.
rewrite Rplus_comm; unfold Rdiv; rewrite <- Rmult_assoc;
rewrite Rsqr_plus_minus; repeat rewrite Rsqr_sqrt.
rewrite Rplus_comm; unfold Rminus; rewrite Rplus_assoc;
rewrite Rplus_opp_r; rewrite Rplus_0_r; rewrite <- Rinv_r_sym.
reflexivity.
apply H8.
left; apply H.
assumption.
red; intro; rewrite H12 in H11; elim (Rlt_irrefl _ H11).
red; intro; rewrite H12 in H11; elim (Rlt_irrefl _ H11).
apply Rplus_lt_le_0_compat.
apply sqrt_lt_R0; apply H.
apply sqrt_positivity; apply H10.
destruct (Rcase_abs h) as [Hlt|Hgt].
rewrite (Rabs_left h Hlt) in H9.
apply Rplus_le_reg_l with (- h).
rewrite Rplus_0_r; rewrite Rplus_comm; rewrite Rplus_assoc;
rewrite Rplus_opp_r; rewrite Rplus_0_r; left; apply Rlt_le_trans with alpha1.
apply H9.
unfold alpha1; apply Rmin_r.
apply Rplus_le_le_0_compat.
left; assumption.
apply Rge_le; apply Hgt.
unfold alpha1; unfold Rmin; case (Rle_dec alpha x); intro.
apply H5.
apply H.
unfold g; rewrite Rplus_0_r.
cut (0 < sqrt x + sqrt x).
intro; red; intro; rewrite H2 in H1; elim (Rlt_irrefl _ H1).
apply Rplus_lt_0_compat; apply sqrt_lt_R0; apply H.
replace g with (fct_cte (sqrt x) + comp sqrt (fct_cte x + id))%F;
[ idtac | reflexivity ].
apply continuity_pt_plus.
apply continuity_pt_const; unfold constant, fct_cte; intro;
reflexivity.
apply continuity_pt_comp.
apply continuity_pt_plus.
apply continuity_pt_const; unfold constant, fct_cte; intro;
reflexivity.
apply derivable_continuous_pt; apply derivable_pt_id.
apply sqrt_continuity_pt.
unfold plus_fct, fct_cte, id; rewrite Rplus_0_r; apply H.
Qed.
(**********)
Lemma derivable_pt_sqrt : forall x:R, 0 < x -> derivable_pt sqrt x.
Proof.
unfold derivable_pt; intros.
exists (/ (2 * sqrt x)).
apply derivable_pt_lim_sqrt; assumption.
Qed.
(**********)
Lemma derive_pt_sqrt :
forall (x:R) (pr:0 < x),
derive_pt sqrt x (derivable_pt_sqrt _ pr) = / (2 * sqrt x).
Proof.
intros.
apply derive_pt_eq_0.
apply derivable_pt_lim_sqrt; assumption.
Qed.
(** We show that sqrt is continuous for all x>=0 *)
(** Remark : by definition of sqrt (as extension of Rsqrt on |R),
we could also show that sqrt is continuous for all x *)
Lemma continuity_pt_sqrt : forall x:R, 0 <= x -> continuity_pt sqrt x.
Proof.
intros; case (Rtotal_order 0 x); intro.
apply (sqrt_continuity_pt x H0).
elim H0; intro.
unfold continuity_pt; unfold continue_in;
unfold limit1_in; unfold limit_in;
simpl; unfold R_dist; intros.
exists (Rsqr eps); intros.
split.
change (0 < Rsqr eps); apply Rsqr_pos_lt.
red; intro; rewrite H3 in H2; elim (Rlt_irrefl _ H2).
intros; elim H3; intros.
rewrite <- H1; rewrite sqrt_0; unfold Rminus; rewrite Ropp_0;
rewrite Rplus_0_r; rewrite <- H1 in H5; unfold Rminus in H5;
rewrite Ropp_0 in H5; rewrite Rplus_0_r in H5.
destruct (Rcase_abs x0) as [Hlt|Hgt] eqn:Heqs.
unfold sqrt. rewrite Heqs.
rewrite Rabs_R0; apply H2.
rewrite Rabs_right.
apply Rsqr_incrst_0.
rewrite Rsqr_sqrt.
rewrite (Rabs_right x0 Hgt) in H5; apply H5.
apply Rge_le; exact Hgt.
apply sqrt_positivity; apply Rge_le; exact Hgt.
left; exact H2.
apply Rle_ge; apply sqrt_positivity; apply Rge_le; exact Hgt.
elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H1 H)).
Qed.
¤ Dauer der Verarbeitung: 0.23 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
