# Library Coq.Reals.PSeries_reg

Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
Require Import Ranalysis1.
Require Import Max.
Require Import Even. Open Local Scope R_scope.

Definition Boule (x:R) (r:posreal) (y:R) : Prop := Rabs (y - x) < r.

Definition CVU (fn:nat -> R -> R) (f:R -> R) (x:R)
(r:posreal) : Prop :=
forall eps:R,
0 < eps ->
exists N : nat,
(forall (n:nat) (y:R),
(N <= n)%nat -> Boule x r y -> Rabs (f y - fn n y) < eps).

Definition CVN_r (fn:nat -> R -> R) (r:posreal) : Type :=
sigT
(fun An:nat -> R =>
sigT
(fun l:R =>
Un_cv (fun n:nat => sum_f_R0 (fun k:nat => Rabs (An k)) n) l /\
(forall (n:nat) (y:R), Boule 0 r y -> Rabs (fn n y) <= An n))).

Definition CVN_R (fn:nat -> R -> R) : Type := forall r:posreal, CVN_r fn r.

Definition SFL (fn:nat -> R -> R)
(cv:forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l))
(y:R) : R := match cv y with
| existT a b => a
end.

Lemma CVN_CVU :
forall (fn:nat -> R -> R)
(cv:forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l))
(r:posreal), CVN_r fn r -> CVU (fun n:nat => SP fn n) (SFL fn cv) 0 r.
intros; unfold CVU in |- *; intros.
unfold CVN_r in X.
elim X; intros An X0.
elim X0; intros s H0.
elim H0; intros.
cut (Un_cv (fun n:nat => sum_f_R0 (fun k:nat => Rabs (An k)) n - s) 0).
intro; unfold Un_cv in H3.
elim (H3 eps H); intros N0 H4.
exists N0; intros.
apply Rle_lt_trans with (Rabs (sum_f_R0 (fun k:nat => Rabs (An k)) n - s)).
rewrite <- (Rabs_Ropp (sum_f_R0 (fun k:nat => Rabs (An k)) n - s));
rewrite Ropp_minus_distr';
rewrite (Rabs_right (s - sum_f_R0 (fun k:nat => Rabs (An k)) n)).
eapply sum_maj1.
unfold SFL in |- *; case (cv y); intro.
trivial.
apply H1.
intro; elim H0; intros.
rewrite (Rabs_right (An n0)).
apply H8; apply H6.
apply Rle_ge; apply Rle_trans with (Rabs (fn n0 y)).
apply Rabs_pos.
apply H8; apply H6.
apply Rle_ge;
apply Rplus_le_reg_l with (sum_f_R0 (fun k:nat => Rabs (An k)) n).
rewrite Rplus_0_r; unfold Rminus in |- *; rewrite (Rplus_comm s);
rewrite <- Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_l;
apply sum_incr.
apply H1.
intro; apply Rabs_pos.
unfold R_dist in H4; unfold Rminus in H4; rewrite Ropp_0 in H4.
assert (H7:= H4 n H5).
rewrite Rplus_0_r in H7; apply H7.
unfold Un_cv in H1; unfold Un_cv in |- *; intros.
elim (H1 _ H3); intros.
exists x; intros.
unfold R_dist in |- *; unfold R_dist in H4.
rewrite Rminus_0_r; apply H4; assumption.
Qed.

Lemma CVU_continuity :
forall (fn:nat -> R -> R) (f:R -> R) (x:R) (r:posreal),
CVU fn f x r ->
(forall (n:nat) (y:R), Boule x r y -> continuity_pt (fn n) y) ->
forall y:R, Boule x r y -> continuity_pt f y.
intros; unfold continuity_pt in |- *; unfold continue_in in |- *;
unfold limit1_in in |- *; unfold limit_in in |- *;
simpl in |- *; unfold R_dist in |- *; intros.
unfold CVU in H.
cut (0 < eps / 3);
[ intro
| unfold Rdiv in |- *; apply Rmult_lt_0_compat;
[ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ].
elim (H _ H3); intros N0 H4.
assert (H5:= H0 N0 y H1).
cut (exists del : posreal, (forall h:R, Rabs h < del -> Boule x r (y + h))).
intro.
elim H6; intros del1 H7.
unfold continuity_pt in H5; unfold continue_in in H5; unfold limit1_in in H5;
unfold limit_in in H5; simpl in H5; unfold R_dist in H5.
elim (H5 _ H3); intros del2 H8.
set (del:= Rmin del1 del2).
exists del; intros.
split.
unfold del in |- *; unfold Rmin in |- *; case (Rle_dec del1 del2); intro.
apply (cond_pos del1).
elim H8; intros; assumption.
intros;
apply Rle_lt_trans with (Rabs (f x0 - fn N0 x0) + Rabs (fn N0 x0 - f y)).
replace (f x0 - f y) with (f x0 - fn N0 x0 + (fn N0 x0 - f y));
[ apply Rabs_triang | ring ].
apply Rle_lt_trans with
(Rabs (f x0 - fn N0 x0) + Rabs (fn N0 x0 - fn N0 y) + Rabs (fn N0 y - f y)).
rewrite Rplus_assoc; apply Rplus_le_compat_l.
replace (fn N0 x0 - f y) with (fn N0 x0 - fn N0 y + (fn N0 y - f y));
[ apply Rabs_triang | ring ].
replace eps with (eps / 3 + eps / 3 + eps / 3).
repeat apply Rplus_lt_compat.
apply H4.
apply le_n.
replace x0 with (y + (x0 - y)); [ idtac | ring ]; apply H7.
elim H9; intros.
apply Rlt_le_trans with del.
assumption.
unfold del in |- *; apply Rmin_l.
elim H8; intros.
apply H11.
split.
elim H9; intros; assumption.
elim H9; intros; apply Rlt_le_trans with del.
assumption.
unfold del in |- *; apply Rmin_r.
rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr'; apply H4.
apply le_n.
assumption.
apply Rmult_eq_reg_l with 3.
do 2 rewrite Rmult_plus_distr_l; unfold Rdiv in |- *; rewrite <- Rmult_assoc;
rewrite Rinv_r_simpl_m.
ring.
discrR.
discrR.
cut (0 < r - Rabs (x - y)).
intro; exists (mkposreal _ H6).
simpl in |- *; intros.
unfold Boule in |- *; replace (y + h - x) with (h + (y - x));
[ idtac | ring ]; apply Rle_lt_trans with (Rabs h + Rabs (y - x)).
apply Rabs_triang.
apply Rplus_lt_reg_r with (- Rabs (x - y)).
rewrite <- (Rabs_Ropp (y - x)); rewrite Ropp_minus_distr'.
replace (- Rabs (x - y) + r) with (r - Rabs (x - y)).
replace (- Rabs (x - y) + (Rabs h + Rabs (x - y))) with (Rabs h).
apply H7.
ring.
ring.
unfold Boule in H1; rewrite <- (Rabs_Ropp (x - y)); rewrite Ropp_minus_distr';
apply Rplus_lt_reg_r with (Rabs (y - x)).
rewrite Rplus_0_r; replace (Rabs (y - x) + (r - Rabs (y - x))) with (pos r);
[ apply H1 | ring ].
Qed.

Lemma continuity_pt_finite_SF :
forall (fn:nat -> R -> R) (N:nat) (x:R),
(forall n:nat, (n <= N)%nat -> continuity_pt (fn n) x) ->
continuity_pt (fun y:R => sum_f_R0 (fun k:nat => fn k y) N) x.
intros; induction N as [| N HrecN].
simpl in |- *; apply (H 0%nat); apply le_n.
simpl in |- *;
replace (fun y:R => sum_f_R0 (fun k:nat => fn k y) N + fn (S N) y) with
((fun y:R => sum_f_R0 (fun k:nat => fn k y) N) + (fun y:R => fn (S N) y))%F;
[ idtac | reflexivity ].
apply continuity_pt_plus.
apply HrecN.
intros; apply H.
apply le_trans with N; [ assumption | apply le_n_Sn ].
apply (H (S N)); apply le_n.
Qed.

Lemma SFL_continuity_pt :
forall (fn:nat -> R -> R)
(cv:forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l))
(r:posreal),
CVN_r fn r ->
(forall (n:nat) (y:R), Boule 0 r y -> continuity_pt (fn n) y) ->
forall y:R, Boule 0 r y -> continuity_pt (SFL fn cv) y.
intros; eapply CVU_continuity.
apply CVN_CVU.
apply X.
intros; unfold SP in |- *; apply continuity_pt_finite_SF.
intros; apply H.
apply H1.
apply H0.
Qed.

Lemma SFL_continuity :
forall (fn:nat -> R -> R)
(cv:forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l)),
CVN_R fn -> (forall n:nat, continuity (fn n)) -> continuity (SFL fn cv).
intros; unfold continuity in |- *; intro.
cut (0 < Rabs x + 1);
[ intro | apply Rplus_le_lt_0_compat; [ apply Rabs_pos | apply Rlt_0_1 ] ].
cut (Boule 0 (mkposreal _ H0) x).
intro; eapply SFL_continuity_pt with (mkposreal _ H0).
apply X.
intros; apply (H n y).
apply H1.
unfold Boule in |- *; simpl in |- *; rewrite Rminus_0_r;
pattern (Rabs x) at 1 in |- *; rewrite <- Rplus_0_r;
apply Rplus_lt_compat_l; apply Rlt_0_1.
Qed.

Lemma CVN_R_CVS :
forall fn:nat -> R -> R,
CVN_R fn -> forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l).
intros; apply R_complete.
unfold SP in |- *; set (An:= fun N:nat => fn N x).
change (Cauchy_crit_series An) in |- *.
apply cauchy_abs.
unfold Cauchy_crit_series in |- *; apply CV_Cauchy.
unfold CVN_R in X; cut (0 < Rabs x + 1).
intro; assert (H0:= X (mkposreal _ H)).
unfold CVN_r in H0; elim H0; intros Bn H1.
elim H1; intros l H2.
elim H2; intros.
apply Rseries_CV_comp with Bn.
intro; split.
apply Rabs_pos.
unfold An in |- *; apply H4; unfold Boule in |- *; simpl in |- *;
rewrite Rminus_0_r.
pattern (Rabs x) at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l;
apply Rlt_0_1.
apply existT with l.
cut (forall n:nat, 0 <= Bn n).
intro; unfold Un_cv in H3; unfold Un_cv in |- *; intros.
elim (H3 _ H6); intros.
exists x0; intros.
replace (sum_f_R0 Bn n) with (sum_f_R0 (fun k:nat => Rabs (Bn k)) n).
apply H7; assumption.
apply sum_eq; intros; apply Rabs_right; apply Rle_ge; apply H5.
intro; apply Rle_trans with (Rabs (An n)).
apply Rabs_pos.
unfold An in |- *; apply H4; unfold Boule in |- *; simpl in |- *;
rewrite Rminus_0_r; pattern (Rabs x) at 1 in |- *;
rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; apply Rlt_0_1.
apply Rplus_le_lt_0_compat; [ apply Rabs_pos | apply Rlt_0_1 ].
Qed.

Index
This page has been generated by coqdoc