proposition: Lemma infinite_sum_assoc : forall {R : ConstructiveReals} (xn : nat -> CRcarrier R) (Pn : nat -> nat) (s : CRcarrier R), (forall n, Pn n < Pn (S n))%nat -> (forall n, 0 <= xn n) -> Pn O = O -> (series_cv (fun n => CRsum (fun k => xn (k+ Pn n)%nat) (Pn (S n) - Pn n - 1)) s) -> series_cv xn s.
proof: Proof. intros. assert (forall p q : nat, p <= q -> Pn p <= Pn q)%nat as PnInc. { induction q. - intros. inversion H3. apply Nat.le_refl. - intros. apply Nat.le_succ_r in H3. destruct H3. apply (Nat.le_trans _ (Pn q)). apply IHq. apply H3. apply (Nat.le_trans _ (S (Pn q))). apply le_S. apply Nat.le_refl. apply H. subst p. apply Nat.le_refl. } assert (forall p:nat, CRsum (fun n : nat => CRsum (fun k : nat => xn (k + Pn n))%nat (Pn (S n) - Pn n - 1)) p == CRsum xn (Pn (S p) - 1)) as assocSum. { induction p. - simpl. repeat rewrite H1. rewrite Nat.sub_0_r. rewrite (CRsum_eq _ xn). reflexivity. intros. rewrite Nat.add_0_r. reflexivity. - simpl. rewrite IHp. clear IHp. destruct (Nat.le_exists_sub 1 (Pn (S p))) as [r [H3 _]]. specialize (H p). apply (Nat.le_trans _ (S (Pn p))). 2: apply H. apply le_n_S. apply Nat.le_0_l. assert (r+1 = S r)%nat. rewrite Nat.add_comm. reflexivity. rewrite H3. rewrite Nat.add_sub. rewrite (CRsum_eq (fun k : nat => xn (k + (r + 1))%nat) (fun k : nat => xn (S r + k)%nat)). rewrite <- (sum_assoc xn r). replace (S r + (Pn (S (S p)) - (r + 1) - 1))%nat with (Pn (S (S p)) - 1)%nat. reflexivity. rewrite Nat.add_sub_assoc. rewrite <- H4. rewrite Nat.add_comm. rewrite Nat.sub_add. reflexivity. rewrite <- H3. apply (Nat.le_trans _ (S (Pn (S p)))). apply le_S. apply Nat.le_refl. apply H. rewrite <- H3. destruct (Nat.le_exists_sub (S (Pn (S p))) (Pn (S (S p)))). apply H. destruct H5. rewrite H5. simpl. replace (S (Pn (S p))) with (1 + Pn (S p))%nat. rewrite Nat.add_assoc. rewrite Nat.add_sub. 2: reflexivity. rewrite Nat.add_comm. apply le_n_S. apply Nat.le_0_l. intros. rewrite Nat.add_comm. rewrite (Nat.add_comm r). reflexivity. } assert (forall n:nat, (Pn 1 <= n)%nat -> let (p,_) := FindPointInSubdivision Pn n H H1 in (CRsum (fun n : nat => CRsum (fun k : nat => xn (k + Pn n))%nat (Pn (S n) - Pn n - 1)) (p-1) <= CRsum xn n /\ CRsum xn n <= CRsum (fun n : nat => CRsum (fun k : nat => xn (k + Pn n))%nat (Pn (S n) - Pn n - 1)) p)). { intro n. destruct (FindPointInSubdivision Pn n H H1) as [p pmaj]. repeat rewrite assocSum. split. apply pos_sum_more. apply H0. destruct p. exfalso. apply Nat.le_ngt in H3. destruct pmaj. contradiction. simpl. rewrite Nat.sub_0_r. apply (Nat.le_trans _ (Pn (S p))). 2: apply pmaj. apply Nat.le_sub_l. apply pos_sum_more. apply H0. apply Nat.le_add_le_sub_r. rewrite Nat.add_comm. apply pmaj. } intros n. specialize (H2 n) as [p pmaj]. exists (Pn (S p)). intros. specialize (H3 i). pose proof (FindPointInSubdivisionSmallest Pn H H1 i). destruct (FindPointInSubdivision Pn i H H1) as [q qmaj]. rewrite CRabs_minus_sym. assert (S p <= q)%nat. { apply H4. apply H2. } apply (ROpenBallConvex _ _ (CRsum (fun n : nat => CRsum (fun k : nat => xn (k + Pn n)%nat) (Pn (S n) - Pn n - 1)) (q-1)) _ (CRsum (fun n : nat => CRsum (fun k : nat => xn (k + Pn n)%nat) (Pn (S n) - Pn n - 1)) q)). split; apply H3. apply (Nat.le_trans _ (Pn (S p))). 2: apply H2. apply PnInc. apply le_n_S. apply Nat.le_0_l. apply (Nat.le_trans _ (Pn (S p))). 2: apply H2. apply PnInc. apply le_n_S. apply Nat.le_0_l. rewrite CRabs_minus_sym. apply pmaj. apply Nat.le_add_le_sub_r. rewrite Nat.add_comm. apply H5. rewrite CRabs_minus_sym; apply pmaj. apply (Nat.le_trans _ (S p)). apply le_S. apply Nat.le_refl. apply H5. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits