proposition: Lemma DiagSeqNegTriangle : forall {R : ConstructiveReals} (u : nat -> nat -> CRcarrier R) (n p : nat) (eps sAbs : CRcarrier R), (forall k : nat, le (diagPlane 0 n) k -> (CRabs _ (CRsum (diagSeq (fun i j : nat => CRabs _ (u i j))) k - sAbs) < eps )) -> CRabs _ (CRsum (fun k : nat => CRsum (u (S n + k)%nat) (p - k)) p) < eps * CR_of_Q R 2.
proof: Proof. intros. apply (CRle_lt_trans _ (CRsum (fun k : nat => CRabs _ (CRsum (u (S n + k)%nat) (p - k))) p)). apply multiTriangleIneg. apply (CRle_lt_trans _ (CRsum (fun k : nat => CRsum (fun l => CRabs _ (u (S n + k)%nat l)) (p - k)) p)). apply sum_Rle. intros. apply multiTriangleIneg. apply (CRle_lt_trans _ (CRsum (diagSeq (fun i j : nat => CRabs _ (u i j))) (diagPlane 0 (S n + p)) - CRsum (diagSeq (fun i j : nat => CRabs _ (u i j))) (diagPlane 0 n))). rewrite (diagSumTriangle _ (S n + p)). rewrite (diagSumTriangle _ n). rewrite sum_assoc. rewrite CRplus_comm. rewrite <- (CRplus_0_r (CRsum (fun k : nat => CRsum (fun l : nat => CRabs _ (u (S n + k)%nat l)) (p - k)) p)). setoid_replace (CRsum (fun k : nat => CRsum (fun j : nat => CRabs _ (u (S n + k)%nat j)) (S n + p - (S n + k))) p) with (CRsum (fun k : nat => CRsum (fun l : nat => CRabs _ (u (S n + k)%nat l)) (p - k)) p). unfold CRminus. rewrite CRplus_assoc. apply CRplus_le_compat_l. rewrite CRplus_comm. rewrite <- (CRplus_opp_l (CRsum (fun i : nat => CRsum (fun j : nat => CRabs _ (u i j)) (n - i)) n)). apply CRplus_le_compat_l. apply sum_Rle. intros. apply pos_sum_more. intros. apply CRabs_pos. apply Nat.sub_le_mono_r. 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. apply CRsum_eq. intros. replace (S n + p - (S n + i))%nat with (p - i)%nat. reflexivity. simpl. rewrite Nat.sub_add_distr. rewrite Nat.add_comm. rewrite Nat.add_sub. reflexivity. apply (CRle_lt_trans _ _ _ (CRle_abs _)). setoid_replace (CRsum (diagSeq (fun i j : nat => CRabs _ (u i j))) (diagPlane 0 (S n + p)) - CRsum (diagSeq (fun i j : nat => CRabs _ (u i j))) (diagPlane 0 n)) with (CRsum (diagSeq (fun i j : nat => CRabs _ (u i j))) (diagPlane 0 (S n + p)) - sAbs + (sAbs - CRsum (diagSeq (fun i j : nat => CRabs _ (u i j))) (diagPlane 0 n))). apply (CRle_lt_trans _ _ _ (CRabs_triang _ _)). rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l, CRmult_1_r. apply CRplus_le_lt_compat. apply CRlt_asym. apply (H (diagPlane 0 (S n + p))). unfold diagPlane. rewrite Nat.add_0_l. rewrite Nat.add_0_l. remember (S n + p)%nat as n0. assert (n <= n0)%nat. subst n0. 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. apply Nat.add_le_mono. assumption. apply Nat.div_le_mono. auto. apply Nat.mul_le_mono. assumption. apply le_n_S. assumption. rewrite CRabs_minus_sym. apply H. apply Nat.le_refl. unfold CRminus. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. reflexivity. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits