proposition: Lemma sum_maj1 : forall (fn : nat -> C -> C) (An : nat -> R) (x l1: C) (l2 : R) (N : nat), Cseq_cv (fun n : nat => CFpartial_sum (fun n => fn n x) n) l1 -> Rseq_cv (fun n : nat => sum_f_R0 An n) l2 -> (forall n : nat, Cnorm (fn n x) <= An n) -> Cnorm (l1 - CFpartial_sum (fun n => fn n x) N) <= l2 - sum_f_R0 An N.
proof: Proof. intros fn An x l1 l2 N fn_cv An_cv fn_bd ; cut { l:C | Cseq_cv (fun n => sum_f_C0 (fun l => fn (S N + l)%nat x) n) l }. intro X; cut { l:R | Rseq_cv (fun n => sum_f_R0 (fun l => An (S N + l)%nat) n) l }. intro X0; elim X; intros l1N H2. elim X0; intros l2N H3. cut (l1 - CFpartial_sum (fun n => fn n x) N = l1N). intro Temp; cut (Rminus l2 (sum_f_R0 An N) = l2N). intro Temp2; rewrite Temp, Temp2. apply sum_cv_maj with (fun n => An (S N + n)%nat) (fun I => fn (S N + I)%nat) x. assumption. assumption. intro n ; apply fn_bd. symmetry ; eapply Rseq_cv_unique. apply H3. unfold Rseq_cv in An_cv |-* ; intros eps eps_pos ; destruct (An_cv _ eps_pos) as [N' HN'] ; exists N' ; intros n n_lb. unfold R_dist ; replace (sum_f_R0 (fun l:nat => An (S N + l)%nat) n - (l2 - sum_f_R0 An N))%R with (sum_f_R0 An N + sum_f_R0 (fun l:nat => An (S N + l)%nat) n - l2)%R; [| ring ]. replace (sum_f_R0 An N + sum_f_R0 (fun l:nat => An (S N + l)%nat) n)%R with (sum_f_R0 An (S (N + n)))%R. apply HN' ; intuition lia. assert (N_pos : (0 <= N)%nat) by intuition. assert (N_ub : (N < S (N + n))%nat) by intuition. intros; assert (H := sigma_split An N_pos N_ub) ; unfold sigma in H. do 2 rewrite Nat.sub_0_r in H. replace (sum_f_R0 An (S (N + n))) with (sum_f_R0 (fun k:nat => An (0 + k)%nat) (S (N + n))). replace (sum_f_R0 An N) with (sum_f_R0 (fun k:nat => An (0 + k)%nat) N). assert (Hrew : (S (N + n) - S N)%nat = n) by intuition lia. rewrite Hrew in H. apply H. apply sum_eq; intros ; reflexivity. apply sum_eq; intros ; reflexivity. symmetry ; eapply Cseq_cv_unique. apply H2. unfold Rseq_cv in fn_cv |-* ; intros eps eps_pos ; destruct (fn_cv _ eps_pos) as [N' HN'] ; exists N' ; intros n n_lb. unfold R_dist ; replace (sum_f_C0 (fun l:nat => fn (S N + l)%nat x) n - (l1 - CFpartial_sum (fun n0 : nat => fn n0 x) N)) with ((CFpartial_sum (fun n0 : nat => fn n0 x) N + sum_f_C0 (fun l:nat => fn (S N + l)%nat x) n) - l1); [| ring ]. replace ((CFpartial_sum (fun n0 : nat => fn n0 x) N + sum_f_C0 (fun l:nat => fn (S N + l)%nat x) n)) with (CFpartial_sum (fun n0 : nat => fn n0 x) (S N + n)%nat). apply HN' ; intuition lia. assert (N_pos : (0 <= N)%nat) by intuition. assert (N_ub : (N < S (N + n))%nat) by intuition. intros; assert (H := Csigma_split (fun n => fn n x) O (S (N + n)) N N_pos N_ub) ; unfold Csigma in H. do 2 rewrite Nat.sub_0_r in H. replace (CFpartial_sum (fun n0 : nat => fn n0 x) (S N + n)) with (sum_f_C0 (fun n : nat => fn (0 + n)%nat x) (S (N + n))). replace (CFpartial_sum (fun n0 : nat => fn n0 x) N) with (sum_f_C0 (fun n : nat => fn (0 + n)%nat x) N). assert (Hrew : (S (N + n) - S N)%nat = n) by intuition lia. rewrite Hrew in H. apply H. unfold CFpartial_sum ; apply sum_f_C0_eq_seq ; intros ; reflexivity. unfold CFpartial_sum ; apply sum_f_C0_eq_seq ; intros ; reflexivity. exists (l2 - sum_f_R0 An N)%R. unfold Rseq_cv in An_cv |-* ; intros eps eps_pos ; destruct (An_cv _ eps_pos) as [N' HN'] ; exists N' ; intros n n_lb. unfold R_dist ; replace (sum_f_R0 (fun l:nat => An (S N + l)%nat) n - (l2 - sum_f_R0 An N))%R with (sum_f_R0 An N + sum_f_R0 (fun l:nat => An (S N + l)%nat) n - l2)%R; [| ring ]. replace (sum_f_R0 An N + sum_f_R0 (fun l:nat => An (S N + l)%nat) n)%R with (sum_f_R0 An (S (N + n)))%R. apply HN' ; intuition lia. assert (N_pos : (0 <= N)%nat) by intuition. assert (N_ub : (N < S (N + n))%nat) by intuition. intros; assert (H := sigma_split An N_pos N_ub) ; unfold sigma in H. do 2 rewrite Nat.sub_0_r in H. replace (sum_f_R0 An (S (N + n))) with (sum_f_R0 (fun k:nat => An (0 + k)%nat) (S (N + n))). replace (sum_f_R0 An N) with (sum_f_R0 (fun k:nat => An (0 + k)%nat) N). assert (Hrew : (S (N + n) - S N)%nat = n) by intuition lia. rewrite Hrew in H. apply H. apply sum_eq; intros ; reflexivity. apply sum_eq; intros ; reflexivity. exists (l1 - CFpartial_sum (fun n => fn n x) N). intros eps eps_pos ; destruct (fn_cv _ eps_pos) as [N' HN'] ; exists N' ; intros n n_lb. replace (sum_f_C0 (fun l:nat => fn (S N + l)%nat x) n - (l1 - CFpartial_sum (fun n0 : nat => fn n0 x) N)) with ((CFpartial_sum (fun n0 : nat => fn n0 x) N + sum_f_C0 (fun l:nat => fn (S N + l)%nat x) n) - l1); [| ring ]. replace ((CFpartial_sum (fun n0 : nat => fn n0 x) N + sum_f_C0 (fun l:nat => fn (S N + l)%nat x) n)) with (CFpartial_sum (fun n0 : nat => fn n0 x) (S N + n)%nat). apply HN' ; intuition lia. assert (N_pos : (0 <= N)%nat) by intuition. assert (N_ub : (N < S (N + n))%nat) by intuition. intros; assert (H := Csigma_split (fun n => fn n x) O (S (N + n)) N N_pos N_ub) ; unfold Csigma in H. do 2 rewrite Nat.sub_0_r in H. replace (CFpartial_sum (fun n0 : nat => fn n0 x) (S N + n)) with (sum_f_C0 (fun n : nat => fn (0 + n)%nat x) (S (N + n))). replace (CFpartial_sum (fun n0 : nat => fn n0 x) N) with (sum_f_C0 (fun n : nat => fn (0 + n)%nat x) N). assert (Hrew : (S (N + n) - S N)%nat = n) by intuition lia. rewrite Hrew in H. apply H. unfold CFpartial_sum ; apply sum_f_C0_eq_seq ; intros ; reflexivity. unfold CFpartial_sum ; apply sum_f_C0_eq_seq ; intros ; reflexivity. Qed.
imports: Rsequence_def Rinterval Ranalysis_def Rsequence_cv_facts Rsequence_tactics MyRIneq Cfunctions Csequence Csequence_facts CFsequence Cnorm Cprop_base Ctacfield Lia Lra PeanoNat Cmet Canalysis_def Canalysis_deriv