proposition: Lemma DiagSeqInfiniteSumColPos : forall {R : ConstructiveReals} (u : nat -> nat -> CRcarrier R) (sumCol : nat -> CRcarrier R) (s : CRcarrier R), (forall n k:nat, 0 <= u n k) -> (forall n:nat, series_cv (u n) (sumCol n)) -> (series_cv sumCol s) -> (series_cv (diagSeq u) s).
proof: Proof. intros R u sumCol s uPos cvCol cvSumCol. assert (forall n:nat, CRsum (diagSeq u) n <= s) as belowS. { apply diagSumMaj. assumption. intros n k. apply (CRle_trans _ (CRsum sumCol n)). apply sum_Rle. intros. apply growing_ineq. 2: apply cvCol. intro i. rewrite <- CRplus_0_r. apply CRplus_le_compat. apply CRle_refl. apply uPos. apply growing_ineq. 2: apply cvSumCol. intro i. rewrite <- CRplus_0_r. apply CRplus_le_compat. apply CRle_refl. apply (series_cv_nonneg (u (S i))). apply uPos. apply cvCol. } intros n. destruct (cvSumCol (2*n)%positive) as [N H1]. assert (0 < CR_of_Q R (1 # 4*n)) as quarterEpsPos. { apply CR_of_Q_lt. reflexivity. } destruct (DiagTruncateRect u sumCol (CR_of_Q R (1 # 4*n)) N quarterEpsPos cvCol) as [p H2]. exists (diagPlane 0 (N+p)). intros. rewrite CRabs_minus_sym. rewrite CRabs_right. apply (CRle_trans _ (s - CRsum (diagSeq u) (diagPlane 0 (N + p)))). unfold CRminus. apply CRplus_le_compat_l. apply CRopp_ge_le_contravar. apply growing_transit. - intro k. rewrite <- (CRplus_0_r (CRsum (diagSeq u) k)). simpl. apply CRplus_le_compat_l. unfold diagSeq. destruct (diagPlaneInv (S k)). apply uPos. - apply H. - rewrite diagSumTriangle. apply (CRle_trans _ (s - CRsum (fun i : nat => CRsum (u i) (N + p - i)) N)). unfold CRminus. apply CRplus_le_compat_l. apply CRopp_ge_le_contravar. apply pos_sum_more. intro k. apply cond_pos_sum. apply uPos. rewrite <- (Nat.add_0_r N). rewrite <- Nat.add_assoc. apply Nat.add_le_mono_l. apply Nat.le_0_l. apply (CRle_trans _ (s - CRsum sumCol N + CR_of_Q R (1#2*n))). specialize (H1 N (Nat.le_refl N)). rewrite CRabs_minus_sym in H1. apply (CRle_trans _ _ _ (CRle_abs _)) in H1. unfold CRminus. rewrite CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_l (CRsum sumCol N)). rewrite <- CRplus_assoc. rewrite CRplus_opp_r. rewrite CRplus_0_l. rewrite <- sum_opp. rewrite <- sum_plus. apply (CRle_trans _ (CRsum (fun k => CR_of_Q R (1#4*n) * CRpow (CR_of_Q R (1#2)) k) N)). apply sum_Rle. intros n0 H0. specialize (H2 (N+p-n0)%nat n0). apply (CRle_trans _ _ _ (CRle_abs _)). pose proof (CRabs_minus_sym (sumCol n0)). unfold CRminus in H3. rewrite H3. clear H3. apply CRlt_asym, H2. exact H0. rewrite Nat.add_comm. rewrite <- Nat.add_sub_assoc. rewrite <- (Nat.add_0_r p). rewrite <- Nat.add_assoc. apply Nat.add_le_mono_l. apply Nat.le_0_l. assumption. rewrite (CRsum_eq _ (fun k : nat => CRpow (CR_of_Q R (1#2)) k * (CR_of_Q R (1# 4*n)))). rewrite sum_scale, CRmult_comm. apply CRlt_asym. apply (CRlt_le_trans _ (CR_of_Q R (1#4*n) * CR_of_Q R 2)). apply CRmult_lt_compat_l. exact quarterEpsPos. apply GeoHalfBelowTwo. rewrite <- CR_of_Q_mult. apply CR_of_Q_le. unfold Qmult, Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l. rewrite <- Pos2Z.inj_mul. rewrite Pos.mul_1_r, Pos.mul_assoc. apply Z.le_refl. intros. apply CRmult_comm. apply (CRplus_le_reg_r (- CR_of_Q R (1#2*n))). rewrite CRplus_assoc. rewrite CRplus_opp_r. rewrite CRplus_0_r. rewrite <- CR_of_Q_opp, <- CR_of_Q_plus. setoid_replace ((1 # n) + - (1 # 2 * n))%Q with (1 # 2*n)%Q. specialize (H1 N (Nat.le_refl N)). apply (CRle_trans _ _ _ (CRle_abs _)). rewrite CRabs_minus_sym. apply H1. rewrite <- (Qplus_inj_r _ _ (1#2*n)). rewrite Qinv_plus_distr. ring_simplify. reflexivity. - rewrite <- (CRplus_opp_r (CRsum (diagSeq u) i)). apply CRplus_le_compat. apply belowS. apply CRle_refl. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits