proposition: Lemma partition_sum_by_packets : forall {R : ConstructiveReals} (f : CRcarrier R -> CRcarrier R) (a b : CRcarrier R) (y : nat -> CRcarrier R) (P Q : @IntervalPartition R a b) (subseq : nat -> nat), IntervalPartitionRefinement _ _ P Q subseq -> CRsum (fun n : nat => CRsum (fun i : nat => (f (y (i + subseq n)%nat) * (ipt_seq Q (S i + subseq n) - ipt_seq Q (i + subseq n)))) (pred (subseq (S n) - subseq n))) (ipt_last P) == CRsum (fun n : nat => (f (y n) * (ipt_seq Q (S n) - ipt_seq Q n))) (ipt_last Q).
proof: Proof. intros. destruct H, H0. transitivity (CRsum (fun n : nat => (f (y n) * (ipt_seq Q (S n) - ipt_seq Q n))) (pred (subseq (S (ipt_last P))))). pose (fun n:nat => match n with O => O | S p => subseq n end) as shiftSubseq. transitivity ( CRsum (fun n0 : nat => CRsum (fun i : nat => (f (y (i + shiftSubseq n0)%nat) * (ipt_seq Q (S i + shiftSubseq n0) - ipt_seq Q (i + shiftSubseq n0)))) (pred (shiftSubseq (S n0) - shiftSubseq n0))) (ipt_last P)). - apply CRsum_eq. intros. destruct i. 2: apply CRsum_eq; reflexivity. unfold shiftSubseq. destruct (Nat.le_exists_sub (S (subseq O)) (subseq 1%nat)) as [p [peq _]]. apply H0. auto. apply le_n_S, Nat.le_0_l. rewrite Nat.sub_0_r. rewrite peq. rewrite Nat.add_succ_r. replace (S (p + subseq 0%nat) - subseq 0)%nat with (S p). simpl. destruct (subseq O) eqn:des. rewrite Nat.add_0_r. apply CRsum_eq; reflexivity. rewrite <- (Nat.add_comm (S n)). rewrite sum_assoc. symmetry. rewrite <- (CRplus_0_l (CRsum (fun i : nat => f (y (i + S n)%nat) * (ipt_seq Q (S (i + S n)) - ipt_seq Q (i + S n))) p)). apply CRplus_morph. rewrite (CRsum_eq _ (fun _ => 0 * 0)). rewrite sum_scale, CRmult_0_r. reflexivity. intros. rewrite CRmult_0_l. rewrite Nat.add_0_r. setoid_replace (ipt_seq Q (S i)) with a. setoid_replace (ipt_seq Q i) with a. unfold CRminus. rewrite CRplus_opp_r, CRmult_0_r. reflexivity. symmetry. rewrite (partition_before_start _ _ _ (subseq O)). reflexivity. apply H1, Nat.le_0_l. rewrite H. symmetry. apply P. apply Nat.le_0_l. rewrite des. apply (Nat.le_trans _ _ _ H3). apply le_S, Nat.le_refl. rewrite (partition_before_start _ _ _ (subseq O)). reflexivity. apply H1, Nat.le_0_l. rewrite H. symmetry. apply P. apply Nat.le_0_l. rewrite des. apply le_n_S. exact H3. apply CRsum_eq. intros. rewrite Nat.add_0_r, Nat.add_comm. reflexivity. rewrite Nat.sub_succ_l. apply f_equal. rewrite Nat.add_sub. reflexivity. rewrite <- (Nat.add_0_l (subseq O)). rewrite Nat.add_assoc. apply Nat.add_le_mono_r. apply Nat.le_0_l. - replace (pred (subseq (S (ipt_last P)))) with (pred (shiftSubseq (S (ipt_last P)))). apply (sum_by_packets (fun n : nat => (f (y n) * (ipt_seq Q (S n) - ipt_seq Q n)))). intros. unfold shiftSubseq. destruct k. apply (Nat.le_lt_trans _ (subseq O)). apply Nat.le_0_l. apply H0. auto. apply le_n_S. exact H2. apply H0. apply Nat.le_refl. apply le_n_S. exact H2. reflexivity. reflexivity. - destruct (Nat.le_exists_sub (subseq (S (ipt_last P))) (S (ipt_last Q))) as [p [peq _]]. apply H1. apply Nat.le_refl. destruct p. replace (Init.Nat.pred (subseq (S (ipt_last P)))) with (ipt_last Q). reflexivity. simpl in peq. rewrite <- peq. reflexivity. inversion peq. clear peq. assert (subseq (S (ipt_last P)) <> 0%nat). { intro abs. specialize (H0 (ipt_last P) (S (ipt_last P)) (Nat.le_refl _) (Nat.le_refl _)). rewrite abs in H0. inversion H0. } pose proof (Nat.succ_pred (subseq (S (ipt_last P))) H2). replace (ipt_last Q) with (S (pred (subseq (S (ipt_last P)))) + p)%nat. rewrite sum_assoc. symmetry. rewrite <- (CRplus_0_r (CRsum (fun n : nat => f (y n) * (ipt_seq Q (S n) - ipt_seq Q n)) (Init.Nat.pred (subseq (S (ipt_last P)))))). apply CRplus_morph. rewrite CRplus_0_r. reflexivity. rewrite (CRsum_eq _ (fun _ => 0 * 0)). rewrite sum_scale, CRmult_0_r. reflexivity. intros. rewrite CRmult_0_l. rewrite H4. setoid_replace (ipt_seq Q (S (subseq (S (ipt_last P)) + i))) with b. setoid_replace (ipt_seq Q (subseq (S (ipt_last P)) + i)) with b. unfold CRminus. rewrite CRplus_opp_r, CRmult_0_r. reflexivity. rewrite (partition_after_end _ _ _ (subseq (S (ipt_last P)))). reflexivity. rewrite H. symmetry. apply P. apply Nat.le_refl. rewrite <- (Nat.add_0_r (subseq (S (ipt_last P)))). rewrite <- Nat.add_assoc. apply Nat.add_le_mono_l, Nat.le_0_l. apply (Nat.le_trans _ (subseq (S (ipt_last P)) + p)). apply Nat.add_le_mono_l. exact H5. rewrite Nat.add_comm, H3. apply le_S, Nat.le_refl. rewrite (partition_after_end _ _ _ (subseq (S (ipt_last P)))). reflexivity. rewrite H. symmetry. apply P. apply Nat.le_refl. apply (Nat.le_trans _ (S (subseq (S (ipt_last P))))). apply le_S, Nat.le_refl. apply le_n_S. rewrite <- (Nat.add_0_r (subseq (S (ipt_last P)))). rewrite <- Nat.add_assoc. apply Nat.add_le_mono_l, Nat.le_0_l. apply le_n_S. apply (Nat.le_trans _ (subseq (S (ipt_last P)) + p)). apply Nat.add_le_mono_l. exact H5. rewrite Nat.add_comm, H3. apply Nat.le_refl. rewrite H4, H3. rewrite Nat.add_comm. reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont