proposition: Lemma DiagSeqInfiniteSum : forall {R : ConstructiveReals} (u : nat -> nat -> CRcarrier R) (sumCol : nat -> CRcarrier R) (sAbs : CRcarrier R), series_cv (diagSeq (fun i j => CRabs _ (u i j))) sAbs -> (forall n:nat, series_cv (u n) (sumCol n)) -> { s : CRcarrier R & (series_cv sumCol s) * (series_cv (diagSeq u) s) * (s <= sAbs) }%type.
proof: Proof. intros R u sumCol sAbs H7 H1. assert { s : CRcarrier R & prod (series_cv (diagSeq u) s) (s <= sAbs) } as [s H]. { destruct (series_cv_maj (diagSeq u) (diagSeq (fun i j => CRabs _ (u i j))) sAbs) as [s scv]. intros. unfold diagSeq. destruct (diagPlaneInv n). apply CRle_refl. exact H7. exists s. exact scv. } exists s. split. split. 2: apply H. 2: apply H. destruct H as [H _]. pose proof (Un_cv_nat_real _ _ H7) as H0. clear H7. apply Un_cv_real_nat. intros eps epsPos. assert (forall n : nat, (0 <= diagSeq (fun i j : nat => CRabs _ (u i j)) n)) as diagPos. { intro n. unfold diagSeq. destruct (diagPlaneInv n). apply CRabs_pos. } assert (0 < eps * CRpow (CR_of_Q R (1#2)) 3) as eighthEpsPos. { apply CRmult_lt_0_compat. assumption. apply CRpow_gt_zero. simpl. apply CR_of_Q_lt. reflexivity. } destruct (H0 (eps * CRpow (CR_of_Q R (1#2)) 3) eighthEpsPos) as [Nabs H2]. pose proof (DiagTriangleShift Nabs) as tShift. destruct (diagPlaneInv Nabs) as [i j] eqn:desNabs. exists (i + j)%nat. intros n nMaj. specialize (tShift n nMaj). setoid_replace eps with (INR 7 * eps * CRpow (CR_of_Q R (1#2)) 3 + eps * CRpow (CR_of_Q R (1#2)) 3). setoid_replace (CRsum sumCol n - s) with (CRsum sumCol n -CRsum (diagSeq u) (diagPlane 0 n) + (CRsum (diagSeq u) (diagPlane 0 n) - s)). apply (CRle_lt_trans _ _ _ (CRabs_triang _ _)). apply CRplus_le_lt_compat. - apply CRlt_asym. destruct (DiagTruncateRect u sumCol (eps * CRpow (CR_of_Q R (1#2)) 4) n) as [p geo]. apply CRmult_lt_0_compat. assumption. apply CRpow_gt_zero. simpl. apply CR_of_Q_lt. reflexivity. intros. apply H1. setoid_replace (CRsum sumCol n - CRsum (diagSeq u) (diagPlane 0 n)) with (CRsum sumCol n - CRsum (fun k => (CRsum (u k) (p+(n-k)))) n + (CRsum (fun k => (CRsum (u k) (p+(n-k)))) n - CRsum (diagSeq u) (diagPlane 0 n))). apply (CRle_lt_trans _ _ _ (CRabs_triang _ _)). setoid_replace (INR 7 * eps * CRpow (CR_of_Q R (1 # 2)) 3) with (eps * CRpow (CR_of_Q R (1 # 2)) 3 + INR 6 * eps * CRpow (CR_of_Q R (1 # 2)) 3). apply CRplus_le_lt_compat. + apply CRlt_asym. unfold CRminus. rewrite <- sum_opp, <- sum_plus. apply (CRle_lt_trans _ (CRsum (fun l : nat => CRabs _ (sumCol l - CRsum (u l) (p+(n-l)))) n)). apply multiTriangleIneg. apply (CRle_lt_trans _ (CRsum (fun k => eps * CRpow (CR_of_Q R (1 # 2)) 4 * CRpow (CR_of_Q R (1 # 2)) k) n)). apply sum_Rle. intros. specialize (geo (p + (n - k))%nat k). apply CRlt_asym. rewrite CRabs_minus_sym. apply geo. exact H3. rewrite <- (Nat.add_0_r p). rewrite <- Nat.add_assoc. apply Nat.add_le_mono_l. apply Nat.le_0_l. rewrite <- (CRsum_eq (fun k : nat => CRpow (CR_of_Q R (1 # 2)) k * (eps * CRpow (CR_of_Q R (1 # 2)) 4))). rewrite sum_scale. rewrite CRmult_comm, CRmult_assoc. apply CRmult_lt_compat_l. assumption. setoid_replace (CRpow (CR_of_Q R (1 # 2)) 3) with (CRpow (CR_of_Q R (1 # 2)) 4 * CR_of_Q R 2). apply CRmult_lt_compat_l. apply CRpow_gt_zero. simpl. apply CR_of_Q_lt. reflexivity. apply GeoHalfBelowTwo. setoid_replace (CRpow (CR_of_Q R (1 # 2)) 4) with (CR_of_Q R (1#2) * CRpow (CR_of_Q R (1 # 2)) 3). 2: reflexivity. rewrite CRmult_comm, <- CRmult_assoc, <- (CR_of_Q_mult _ 2). setoid_replace (2 * (1 # 2))%Q with 1%Q. rewrite CRmult_1_l. reflexivity. reflexivity. intros. apply CRmult_comm. + destruct p. setoid_replace (CRsum (fun k : nat => CRsum (u k) (0 + (n - k))) n) with (CRsum (diagSeq u) (diagPlane 0 n)). unfold CRminus. rewrite CRplus_opp_r. rewrite CRabs_right. 2: apply CRle_refl. apply CRmult_lt_0_compat. apply CRmult_lt_0_compat. apply CR_of_Q_lt. reflexivity. assumption. apply CRpow_gt_zero. simpl. apply CR_of_Q_lt. reflexivity. simpl. rewrite diagSumTriangle. reflexivity. setoid_replace (CRsum (fun k : nat => CRsum (u k) (S p + (n - k))) n) with (CRsum (diagSeq u) (diagPlane 0 (S n+p)) - CRsum (fun k : nat => CRsum (u (S n + k)%nat) (p - k)) p). unfold CRminus. rewrite CRplus_comm. rewrite <- CRplus_assoc. setoid_replace (- CRsum (diagSeq u) (diagPlane 0 n) + CRsum (diagSeq u) (diagPlane 0 (S n + p)) + - CRsum (fun k : nat => CRsum (u (S n + k)%nat) (p - k)) p) with (CRsum (diagSeq u) (diagPlane 0 (S n + p)) - CRsum (diagSeq u) (diagPlane 0 n) - (CRsum (fun k : nat => CRsum (u (S n + k)%nat) (p - k)) p)). apply (CRle_lt_trans _ _ _ (CRabs_triang _ _)). rewrite CRabs_opp. setoid_replace (INR 6 * eps * CRpow (CR_of_Q R (1 # 2)) 3) with (INR 2 * eps * CRpow (CR_of_Q R (1 # 2)) 3 + INR 4 * eps * CRpow (CR_of_Q R (1 # 2)) 3). apply CRplus_le_lt_compat. setoid_replace (CRsum (diagSeq u) (diagPlane 0 (S n + p)) - CRsum (diagSeq u) (diagPlane 0 n)) with (CRsum (diagSeq u) (diagPlane 0 (S n + p)) - s + (s - CRsum (diagSeq u) (diagPlane 0 n))). apply (CRle_trans _ _ _ (CRabs_triang _ _)). unfold INR. simpl (Z.of_nat 2 # 1). rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_r, CRmult_1_l. rewrite CRmult_plus_distr_r. apply CRplus_le_compat. apply (CRle_trans _ (sAbs - CRsum (fun n0 : nat => CRabs _ (diagSeq u n0)) (diagPlane 0 (S n + p)))). apply (series_cv_abs_remainder (diagSeq u)). apply H. apply (series_cv_eq (diagSeq (fun i j : nat => CRabs _ (u i j)))). intros. unfold diagSeq. destruct (diagPlaneInv n0). reflexivity. apply Un_cv_real_nat. apply H0. rewrite <- (CRsum_eq (diagSeq (fun i j : nat => CRabs _ (u i j)))). apply CRlt_asym. apply (CRle_lt_trans _ _ _ (CRle_abs _)). rewrite CRabs_minus_sym. apply H2. pose proof (DiagTriangleShift Nabs (S n +p)). rewrite desNabs in H3. apply H3. apply (Nat.le_trans _ n). assumption. simpl. apply le_S. rewrite <- (Nat.add_0_r n). rewrite <- Nat.add_assoc. apply Nat.add_le_mono_l. apply Nat.le_0_l. intros. unfold diagSeq. destruct (diagPlaneInv i0). reflexivity. rewrite CRabs_minus_sym. apply (CRle_trans _ (sAbs - CRsum (fun n0 : nat => CRabs _ (diagSeq u n0)) (diagPlane 0 n))). apply (series_cv_abs_remainder (fun n0 : nat => diagSeq u n0)). assumption. apply (series_cv_eq (diagSeq (fun i j : nat => CRabs _ (u i j)))). intros. unfold diagSeq. destruct (diagPlaneInv n0). reflexivity. apply Un_cv_real_nat. apply H0. rewrite <- (CRsum_eq (diagSeq (fun i j : nat => CRabs _ (u i j)))). apply CRlt_asym. apply (CRle_lt_trans _ _ _ (CRle_abs _)). rewrite CRabs_minus_sym. apply H2. assumption. intros. unfold diagSeq. destruct (diagPlaneInv i0). reflexivity. unfold CRminus. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. reflexivity. apply (CRlt_trans _ (eps * CRpow (CR_of_Q R (1 # 2)) 3 * CR_of_Q R 2)). apply (DiagSeqNegTriangle _ _ _ _ sAbs). intros. apply H2. apply (Nat.le_trans _ (diagPlane 0 n)); assumption. rewrite <- (CRmult_comm (CR_of_Q R 2)). rewrite CRmult_assoc. apply CRmult_lt_compat_r. apply CRmult_lt_0_compat. assumption. apply CRpow_gt_zero. simpl. apply CR_of_Q_lt. reflexivity. apply CR_of_Q_lt. reflexivity. setoid_replace (@INR R 6) with (@INR R 2 + @INR R 4). do 2 rewrite CRmult_plus_distr_r. reflexivity. unfold INR. rewrite <- CR_of_Q_plus. apply CR_of_Q_morph. rewrite Qinv_plus_distr. reflexivity. apply CRplus_morph. 2: reflexivity. rewrite (diagSumTriangle _ (S n + p)). unfold CRminus. rewrite CRplus_comm. reflexivity. rewrite (diagSumTriangle _ (S n + p)). unfold CRminus. rewrite sum_assoc. rewrite (CRsum_eq (fun k : nat => CRsum (u (S n + k)%nat) (S n + p - (S n + k))) (fun k : nat => CRsum (u (S n + k)%nat) (p - k))). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_r, CRplus_0_r. apply CRsum_eq. intros. replace (S n + p - i0)%nat with (S p + (n - i0))%nat. reflexivity. rewrite Nat.add_sub_assoc. simpl. destruct i0. rewrite Nat.add_comm. reflexivity. rewrite Nat.add_comm. reflexivity. assumption. intros. replace (S n + p - (S n + i0))%nat with (p - i0)%nat. reflexivity. simpl. rewrite Nat.sub_add_distr. rewrite Nat.add_comm. rewrite Nat.add_sub. reflexivity. + setoid_replace (@INR R 7) with (1 + @INR R 6). do 2 rewrite CRmult_plus_distr_r. rewrite CRmult_1_l. reflexivity. unfold INR. rewrite <- CR_of_Q_plus. apply CR_of_Q_morph. rewrite Qinv_plus_distr. reflexivity. + unfold CRminus. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. reflexivity. - apply (CRle_lt_trans _ (sAbs - CRsum (fun n => CRabs _ (diagSeq u n)) (diagPlane 0 n))). apply (series_cv_abs_remainder (fun n0 : nat => diagSeq u n0)). apply H. apply (series_cv_eq (diagSeq (fun i j : nat => CRabs _ (u i j)))). intros. unfold diagSeq. destruct (diagPlaneInv n0). reflexivity. apply Un_cv_real_nat. apply H0. rewrite <- (CRsum_eq (diagSeq (fun i j : nat => CRabs _ (u i j)))). apply (CRle_lt_trans _ _ _ (CRle_abs _)). rewrite CRabs_minus_sym. apply H2. assumption. intros. unfold diagSeq. destruct (diagPlaneInv i0). reflexivity. - unfold CRminus. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. reflexivity. - setoid_replace (CRpow (CR_of_Q R (1 # 2)) 3) with (CR_of_Q R (1 # 8)). rewrite <- CRmult_plus_distr_r. setoid_replace (INR 7 * eps + eps) with (eps * INR 8). rewrite CRmult_assoc. unfold INR. rewrite <- CR_of_Q_mult. setoid_replace ((Z.of_nat 8 # 1) * (1 # 8))%Q with 1%Q. rewrite CRmult_1_r. reflexivity. reflexivity. setoid_replace (@INR R 8) with (1 + @INR R 7). rewrite CRmult_plus_distr_l, CRmult_1_r, CRplus_comm, CRmult_comm. reflexivity. unfold INR. rewrite <- CR_of_Q_plus. apply CR_of_Q_morph. reflexivity. unfold CRpow. rewrite CRmult_1_r. do 2 rewrite <- CR_of_Q_mult. apply CR_of_Q_morph. reflexivity. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits