proposition: Lemma weaveInfiniteSums : forall {R : ConstructiveReals} (u v : nat -> CRcarrier R) (su sv : CRcarrier R), series_cv u su -> series_cv v sv -> series_cv (weaveSequences (CRcarrier R) u v) (su + sv).
proof: Proof. intros. intros n. specialize (H (2*n)%positive). specialize (H0 (2*n)%positive). destruct H as [N H], H0 as [N0 H0]. exists (S(N*2 + (S N0)*2)). intros. rewrite weaveSequencesSum. destruct i. exfalso; inversion H1. destruct (Nat.even (S i)) eqn:snEven. + setoid_replace (CRsum u (S i / 2) + CRsum v (Init.Nat.pred (S i / 2)) - (su + sv)) with (CRsum u (S i / 2) - su + (CRsum v (Init.Nat.pred (S i / 2)) - sv)). apply (CRle_trans _ _ _ (CRabs_triang _ _)). setoid_replace (1 # n)%Q with ((1 # (2*n)) + (1 # (2*n)))%Q. apply le_S_n in H1. rewrite CR_of_Q_plus. apply CRplus_le_compat. apply H. rewrite <- (Nat.div_mul N 2). apply Nat.div_le_mono. auto. apply (Nat.le_trans (N*2) (N*2 + (S N0)*2)). apply Nat.le_add_r. apply (Nat.le_trans _ i). assumption. apply le_S. apply Nat.le_refl. auto. apply H0. assert (N0 = pred (S N0)). reflexivity. rewrite H2. apply Nat.pred_le_mono. rewrite <- (Nat.div_mul (S N0) 2). apply Nat.div_le_mono. auto. apply (Nat.le_trans _ (N*2 + (S N0)*2)). rewrite Nat.add_comm. apply Nat.le_add_r. apply (Nat.le_trans (N*2 + (S N0)*2) i). assumption. apply le_S. apply Nat.le_refl. auto. rewrite Qinv_plus_distr. reflexivity. unfold CRminus. do 2 rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite CRopp_plus_distr, CRplus_comm. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. apply CRplus_comm. + setoid_replace (CRsum u (S i / 2) + CRsum v (S i / 2) - (su + sv)) with (CRsum u (S i / 2) - su + (CRsum v (S i / 2) - sv)). apply (CRle_trans _ _ _ (CRabs_triang _ _)). setoid_replace (1 # n)%Q with ((1 # (2*n)) + (1 # (2*n)))%Q. apply le_S_n in H1. rewrite CR_of_Q_plus. apply CRplus_le_compat. apply H. rewrite <- (Nat.div_mul N 2). apply Nat.div_le_mono. auto. apply (Nat.le_trans (N*2) (N*2 + (S N0)*2)). apply Nat.le_add_r. apply (Nat.le_trans _ i). assumption. apply le_S. apply Nat.le_refl. auto. apply H0. rewrite <- (Nat.div_mul N0 2). apply Nat.div_le_mono. auto. apply (Nat.le_trans (N0*2) (N*2 + (S N0)*2)). rewrite Nat.add_comm. apply (Nat.le_trans (N0 * 2) (S N0 * 2)). apply Nat.mul_le_mono_r. apply le_S. apply Nat.le_refl. apply Nat.le_add_r. apply (Nat.le_trans _ i). assumption. apply le_S. apply Nat.le_refl. auto. rewrite Qinv_plus_distr. reflexivity. unfold CRminus. do 2 rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite CRopp_plus_distr, CRplus_comm. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. apply CRplus_comm. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase