Require Import Reals.
Require Import Rsequence_def.
Require Import Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_sums Rpser_cv_facts.
Require Import Rinterval Ranalysis_def Rfunction_facts.
Require Import Ass_handling.

Section Functions_extensionality.

Variables f g : R → R.
Hypothesis fg_ext : f == g.

Lemma continuity_ext : continuity f → continuity g.
Proof.
intros f_cont x eps eps_pos.
 destruct (f_cont x _ eps_pos) as [delta [delta_pos Hdelta]].
 ∃ delta ; split ; [assumption |].
 intros ; do 2 rewrite <- fg_ext ; auto.
Qed.

Lemma derivable_pt_lim_ext : ∀ x l, derivable_pt_lim f x l →
  derivable_pt_lim g x l.
Proof.
intros x l Hl eps eps_pos ; destruct (Hl _ eps_pos) as [delta Hdelta] ;
 ∃ delta ; intros ; do 2 rewrite <- fg_ext ; auto.
Qed.

Lemma derivable_pt_ext : ∀ x, derivable_pt f x →
  derivable_pt g x.
Proof.
intros x [df Hdf] ; ∃ df ; apply derivable_pt_lim_ext ; trivial.
Qed.

Lemma derivable_ext : derivable f → derivable g.
Proof.
intros f_deriv x ; apply derivable_pt_ext ; auto.
Qed.

Lemma derive_pt_ext (x : R) (prf : derivable_pt f x) (prg : derivable_pt g x) :
  derive_pt f x prf = derive_pt g x prg.
Proof.
apply pr_nu_var2 ; assumption.
Qed.

Lemma derive_ext (prf : derivable f) (prg : derivable g) :
  derive f prf == derive g prg.
Proof.
intro x ; unfold derive ; apply derive_pt_ext.
Qed.

End Functions_extensionality.

Section Rpser_extensionality.

Variables An Bn : Rseq.
Hypothesis AnBn_ext : (An == Bn)%Rseq.

Lemma sum_f_R0_ext : (sum_f_R0 An == sum_f_R0 Bn)%Rseq.
Proof.
intro n ; induction n ; simpl ; rewrite AnBn_ext ;
 [| rewrite IHn] ; reflexivity.
Qed.

Lemma Pser_ext : ∀ x l, Pser An x l ↔ Pser Bn x l.
Proof.
intros x l ; split ; intros HP eps eps_pos ; destruct (HP _ eps_pos) as [N HN] ;
 ∃ N ; intros n n_lb ;
 [rewrite (sum_eq _ (fun n ⇒ An n × x ^ n)%R) |
 rewrite (sum_eq _ (fun n ⇒ Bn n × x ^ n)%R)] ;
 ((apply HN ; assumption) || (intros ; rewrite AnBn_ext ; reflexivity)).
Qed.

Lemma weaksum_r_ext : ∀ (r : R) (rAn : Cv_radius_weak An r)
 (rBn : Cv_radius_weak Bn r),
 weaksum_r An r rAn == weaksum_r Bn r rBn.
Proof.
intros r rAn rBn x.
 unfold weaksum_r ; destruct (Rlt_le_dec (Rabs x) r) ; trivial.
 destruct (Rpser_abel _ _ rAn x r0) as [l1 Hl1] ; copy Hl1 ;
  rewrite Pser_ext in Hl0.
 destruct (Rpser_abel _ _ rBn x r0) as [l2 Hl2].
 simpl ; eapply Rpser_unique ; eassumption.
Qed.

Lemma sum_r_ext : ∀ (r : R) (rAn : finite_cv_radius An r)
 (rBn : finite_cv_radius Bn r),
 sum_r An r rAn == sum_r Bn r rBn.
Proof.
intros r rAn rBn x.
 unfold sum_r ; destruct (Rlt_le_dec (Rabs x) r) ; trivial ;
  apply weaksum_r_ext.
Qed.

Lemma sum_ext : ∀ (rAn : infinite_cv_radius An)
  (rBn : infinite_cv_radius Bn),
  sum An rAn == sum Bn rBn.
intros rAn rBn x ; unfold sum ; apply weaksum_r_ext.
Qed.

End Rpser_extensionality.