Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Rcomplete.v Sprache: Coq

Original von: Coq^©

(************************************************************************)
(*         *   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 Rseries.
Require Import SeqProp.
Require Import Max.
Local Open Scope R_scope.

(****************************************************)
(*              R is complete :                     *)
(*        Each sequence which satisfies             *)
(*       the Cauchy's criterion converges           *)
(*                                                  *)
(*    Proof with adjacent sequences (Vn and Wn)     *)
(****************************************************)

Theorem R_complete :
  forall Un:nat -> R, Cauchy_crit Un -> { l:R | Un_cv Un l } .
Proof.
  intros.
  set (Vn := sequence_minorant Un (cauchy_min Un H)).
  set (Wn := sequence_majorant Un (cauchy_maj Un H)).
  pose proof (maj_cv Un H) as (x,p).
  fold Wn in p.
  pose proof (min_cv Un H) as (x0,p0).
  fold Vn in p0.
  cut (x = x0).
  intros H2.
  exists x.
  rewrite <- H2 in p0.
  unfold Un_cv.
  intros.
  unfold Un_cv in p; unfold Un_cv in p0.
  cut (0 < eps / 3).
  intro H4.
  elim (p (eps / 3) H4); intros.
  elim (p0 (eps / 3) H4); intros.
  exists (max x1 x2).
  intros.
  unfold R_dist.
  apply Rle_lt_trans with (Rabs (Un n - Vn n) + Rabs (Vn n - x)).
  replace (Un n - x) with (Un n - Vn n + (Vn n - x));
  [ apply Rabs_triang | ring ].
  apply Rle_lt_trans with (Rabs (Wn n - Vn n) + Rabs (Vn n - x)).
  do 2 rewrite <- (Rplus_comm (Rabs (Vn n - x))).
  apply Rplus_le_compat_l.
  repeat rewrite Rabs_right.
  unfold Rminus; do 2 rewrite <- (Rplus_comm (- Vn n));
    apply Rplus_le_compat_l.
  assert (H8 := Vn_Un_Wn_order Un (cauchy_maj Un H) (cauchy_min Un H)).
  fold Vn Wn in H8.
  elim (H8 n); intros.
  assumption.
  apply Rle_ge.
  unfold Rminus; apply Rplus_le_reg_l with (Vn n).
  rewrite Rplus_0_r.
  replace (Vn n + (Wn n + - Vn n)) with (Wn n); [ idtac | ring ].
  assert (H8 := Vn_Un_Wn_order Un (cauchy_maj Un H) (cauchy_min Un H)).
  fold Vn Wn in H8.
  elim (H8 n); intros.
  apply Rle_trans with (Un n); assumption.
  apply Rle_ge.
  unfold Rminus; apply Rplus_le_reg_l with (Vn n).
  rewrite Rplus_0_r.
  replace (Vn n + (Un n + - Vn n)) with (Un n); [ idtac | ring ].
  assert (H8 := Vn_Un_Wn_order Un (cauchy_maj Un H) (cauchy_min Un H)).
  fold Vn Wn in H8.
  elim (H8 n); intros.
  assumption.
  apply Rle_lt_trans with (Rabs (Wn n - x) + Rabs (x - Vn n) + Rabs (Vn n - x)).
  do 2 rewrite <- (Rplus_comm (Rabs (Vn n - x))).
  apply Rplus_le_compat_l.
  replace (Wn n - Vn n) with (Wn n - x + (x - Vn n));
  [ apply Rabs_triang | ring ].
  apply Rlt_le_trans with (eps / 3 + eps / 3 + eps / 3).
  repeat apply Rplus_lt_compat.
  unfold R_dist in H1.
  apply H1.
  unfold ge; apply le_trans with (max x1 x2).
  apply le_max_l.
  assumption.
  rewrite <- Rabs_Ropp.
  replace (- (x - Vn n)) with (Vn n - x); [ idtac | ring ].
  unfold R_dist in H3.
  apply H3.
  unfold ge; apply le_trans with (max x1 x2).
  apply le_max_r.
  assumption.
  unfold R_dist in H3.
  apply H3.
  unfold ge; apply le_trans with (max x1 x2).
  apply le_max_r.
  assumption.
  right.
  pattern eps at 4; replace eps with (3 * (eps / 3)).
  ring.
  unfold Rdiv; rewrite <- Rmult_assoc; apply Rinv_r_simpl_m; discrR.
  unfold Rdiv; apply Rmult_lt_0_compat;
    [ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
  apply cond_eq.
  intros.
  cut (0 < eps / 5).
  intro.
  unfold Un_cv in p; unfold Un_cv in p0.
  unfold R_dist in p; unfold R_dist in p0.
  elim (p (eps / 5) H1); intros N1 H4.
  elim (p0 (eps / 5) H1); intros N2 H5.
  unfold Cauchy_crit in H.
  unfold R_dist in H.
  elim (H (eps / 5) H1); intros N3 H6.
  set (N := max (max N1 N2) N3).
  apply Rle_lt_trans with (Rabs (x - Wn N) + Rabs (Wn N - x0)).
  replace (x - x0) with (x - Wn N + (Wn N - x0)); [ apply Rabs_triang | ring ].
  apply Rle_lt_trans with
    (Rabs (x - Wn N) + Rabs (Wn N - Vn N) + Rabs (Vn N - x0)).
  rewrite Rplus_assoc.
  apply Rplus_le_compat_l.
  replace (Wn N - x0) with (Wn N - Vn N + (Vn N - x0));
  [ apply Rabs_triang | ring ].
  replace eps with (eps / 5 + 3 * (eps / 5) + eps / 5).
  repeat apply Rplus_lt_compat.
  rewrite <- Rabs_Ropp.
  replace (- (x - Wn N)) with (Wn N - x); [ apply H4 | ring ].
  unfold ge, N.
  apply le_trans with (max N1 N2); apply le_max_l.
  unfold Wn, Vn.
  unfold sequence_majorant, sequence_minorant.
  assert
    (H7 :=
      approx_maj (fun k:nat => Un (N + k)%nat) (maj_ss Un N (cauchy_maj Un H))).
  assert
    (H8 :=
      approx_min (fun k:nat => Un (N + k)%nat) (min_ss Un N (cauchy_min Un H))).
  cut
    (Wn N =
      majorant (fun k:nat => Un (N + k)%nat) (maj_ss Un N (cauchy_maj Un H))).
  cut
    (Vn N =
      minorant (fun k:nat => Un (N + k)%nat) (min_ss Un N (cauchy_min Un H))).
  intros H9 H10.
  rewrite <- H9 in H8 |- *.
  rewrite <- H10 in H7 |- *.
  elim (H7 (eps / 5) H1); intros k2 H11.
  elim (H8 (eps / 5) H1); intros k1 H12.
  apply Rle_lt_trans with
    (Rabs (Wn N - Un (N + k2)%nat) + Rabs (Un (N + k2)%nat - Vn N)).
  replace (Wn N - Vn N) with
  (Wn N - Un (N + k2)%nat + (Un (N + k2)%nat - Vn N));
  [ apply Rabs_triang | ring ].
  apply Rle_lt_trans with
    (Rabs (Wn N - Un (N + k2)%nat) + Rabs (Un (N + k2)%nat - Un (N + k1)%nat) +
      Rabs (Un (N + k1)%nat - Vn N)).
  rewrite Rplus_assoc.
  apply Rplus_le_compat_l.
  replace (Un (N + k2)%nat - Vn N) with
  (Un (N + k2)%nat - Un (N + k1)%nat + (Un (N + k1)%nat - Vn N));
  [ apply Rabs_triang | ring ].
  replace (3 * (eps / 5)) with (eps / 5 + eps / 5 + eps / 5);
  [ repeat apply Rplus_lt_compat | ring ].
  assumption.
  apply H6.
  unfold ge.
  apply le_trans with N.
  unfold N; apply le_max_r.
  apply le_plus_l.
  unfold ge.
  apply le_trans with N.
  unfold N; apply le_max_r.
  apply le_plus_l.
  rewrite <- Rabs_Ropp.
  replace (- (Un (N + k1)%nat - Vn N)) with (Vn N - Un (N + k1)%nat);
  [ assumption | ring ].
  reflexivity.
  reflexivity.
  apply H5.
  unfold ge; apply le_trans with (max N1 N2).
  apply le_max_r.
  unfold N; apply le_max_l.
  pattern eps at 4; replace eps with (5 * (eps / 5)).
  ring.
  unfold Rdiv; rewrite <- Rmult_assoc; apply Rinv_r_simpl_m.
  discrR.
  unfold Rdiv; apply Rmult_lt_0_compat.
  assumption.
  apply Rinv_0_lt_compat.
  prove_sup0; try apply lt_O_Sn.
Qed.

¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.