proposition: Lemma UC_refine_integral : forall {R : ConstructiveReals} (f : CRcarrier R -> CRcarrier R) (a b eps : CRcarrier R) (cont_mod : forall eps:CRcarrier R, 0 < eps -> CRcarrier R) (x y : nat -> CRcarrier R) (P Q : @IntervalPartition R a b) (epsPos : 0 < eps) (subseq : nat -> nat), UniformCont f cont_mod -> WeavedLists x (ipt_seq P) (ipt_last P) -> WeavedLists y (ipt_seq Q) (ipt_last Q) -> IntervalPartitionRefinement _ _ P Q subseq -> (PartitionMesh (ipt_seq P) (S (ipt_last P))) < (cont_mod eps epsPos) -> CRabs _ (IntegralFiniteSum f x (ipt_seq P) (ipt_last P) - IntegralFiniteSum f y (ipt_seq Q) (ipt_last Q)) <= eps * (b-a).
proof: Proof. intros. setoid_replace (IntegralFiniteSum f x (ipt_seq P) (ipt_last P) - IntegralFiniteSum f y (ipt_seq Q) (ipt_last Q)) with (CRsum (fun n:nat => f (x n) * (CRsum (fun i => 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 => CRsum (fun i => 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))). - rewrite <- Rsum_minus. apply (CRle_trans _ _ _ (multiTriangleIneg _ _)). apply (CRle_trans _ (CRsum (fun k => eps * (ipt_seq P (S k) - ipt_seq P k)) (ipt_last P))). + apply sum_Rle. intros n H4. rewrite CRmult_comm, <- sum_scale, <- Rsum_minus. apply (CRle_trans _ _ _ (multiTriangleIneg _ _)). apply (CRle_trans _ (CRsum (fun k : nat => CRabs _ (f (x n) - f (y (plus k (subseq n)))) * (ipt_seq Q (S k + subseq n) - ipt_seq Q (k + subseq n))) (pred (subseq (S n) - subseq n)))). apply sum_Rle. intros. rewrite <- (CRmult_comm (f (x n))). unfold CRminus. rewrite CRopp_mult_distr_l. rewrite <- CRmult_plus_distr_r, CRabs_mult. apply CRmult_le_compat_l. apply CRabs_pos. rewrite CRabs_right. apply CRle_refl. rewrite <- (CRplus_opp_r (ipt_seq Q (k + subseq n))). apply CRplus_le_compat. 2: apply CRle_refl. apply ipt_ordered. apply le_S_n. apply le_n_S in H5. apply (Nat.le_trans _ (subseq (S n))). rewrite Nat.succ_pred in H5. rewrite Nat.add_comm. apply Nat.lt_add_lt_sub_l. exact H5. intro abs. destruct H2, H6. specialize (H6 n (S n) (Nat.le_refl _)). apply Nat.sub_0_le in abs. apply (proj1 (Nat.le_ngt _ _) abs). apply H6, le_n_S, H4. apply H2. apply le_n_S, H4. apply (CRle_trans _ (CRsum (fun k : nat => (ipt_seq Q (S k + subseq n) - ipt_seq Q (k + subseq n)) * eps) (Init.Nat.pred (subseq (S n) - subseq n)))). apply sum_Rle. intros n0 H5. rewrite CRmult_comm. apply CRmult_le_compat_l. rewrite <- (CRplus_opp_r (ipt_seq Q (n0 + subseq n))). apply CRplus_le_compat. 2: apply CRle_refl. apply (ipt_ordered Q). apply le_n_S in H5. rewrite Nat.succ_pred in H5. apply le_S_n. apply (Nat.le_trans _ (subseq (S n))). rewrite Nat.add_comm. apply Nat.lt_add_lt_sub_l. exact H5. apply H2, le_n_S, H4. intro abs. destruct H2, H6. specialize (H6 n (S n) (Nat.le_refl _)). apply Nat.sub_0_le in abs. apply (proj1 (Nat.le_ngt _ _) abs). apply H6, le_n_S, H4. destruct H. apply CRlt_asym. apply (c0 eps _ _ epsPos). apply (CRle_lt_trans _ (PartitionMesh (ipt_seq P) (S (ipt_last P)))). 2: exact H3. apply (in_refinement_packet a b n (n0 + subseq n) x y P Q subseq H0 H1 H2 H4). apply le_n_S in H5. rewrite Nat.succ_pred in H5. apply (Nat.le_trans _ (0 + subseq n)). apply Nat.le_refl. apply Nat.add_le_mono_r. apply Nat.le_0_l. intro abs. destruct H2, H2. specialize (H2 n (S n) (Nat.le_refl _)). apply Nat.sub_0_le in abs. apply (proj1 (Nat.le_ngt _ _) abs). apply H2. apply le_n_S, H4. rewrite Nat.add_comm. apply Nat.lt_add_lt_sub_l. apply le_n_S in H5. rewrite Nat.succ_pred in H5. exact H5. intro abs. destruct H2, H2. specialize (H2 n (S n) (Nat.le_refl _)). apply Nat.sub_0_le in abs. apply (proj1 (Nat.le_ngt _ _) abs). apply H2. apply le_n_S, H4. rewrite sum_scale, CRmult_comm. apply CRmult_le_compat_l. apply CRlt_asym, epsPos. rewrite (TelescopicSum (fun i => ipt_seq Q (i + subseq n))). simpl. replace (S (pred (subseq (S n) - subseq n) + subseq n)) with (subseq (S n)). destruct H2. rewrite H2. 2: apply le_n_S, H4. rewrite H2. apply CRle_refl. apply (Nat.le_trans _ _ _ H4). apply le_S, Nat.le_refl. replace (S (Init.Nat.pred (subseq (S n) - subseq n) + subseq n)) with (S (Init.Nat.pred (subseq (S n) - subseq n)) + subseq n)%nat. 2: reflexivity. rewrite Nat.succ_pred. rewrite Nat.sub_add. reflexivity. apply (Nat.le_trans _ (S (subseq n))). apply le_S, Nat.le_refl. apply H2. apply Nat.le_refl. apply le_n_S, H4. intro abs. destruct H2, H5. specialize (H5 n (S n) (Nat.le_refl _)). apply Nat.sub_0_le in abs. apply (proj1 (Nat.le_ngt _ _) abs), H5, le_n_S, H4. + rewrite (CRsum_eq _ (fun k : nat => (ipt_seq P (S k) - ipt_seq P k) * eps)). rewrite sum_scale, CRmult_comm. apply CRmult_le_compat_l. apply CRlt_asym, epsPos. rewrite TelescopicSum. destruct P; simpl. rewrite <- ipt_lastB0, <- ipt_head0. apply CRle_refl. intros. rewrite CRmult_comm. reflexivity. - apply CRplus_morph. + apply CRsum_eq. intros. apply CRmult_morph. reflexivity. rewrite (TelescopicSum (fun n => ipt_seq Q (n + subseq i))). simpl. replace (S (pred (subseq (S i) - subseq i) + subseq i)) with (subseq (S i)). destruct H2. rewrite (H2 i). rewrite (H2 (S i)). reflexivity. apply le_n_S, H4. apply (Nat.le_trans _ _ _ H4), le_S, Nat.le_refl. replace (S (Init.Nat.pred (subseq (S i) - subseq i) + subseq i)) with (S (Init.Nat.pred (subseq (S i) - subseq i)) + subseq i)%nat. 2: reflexivity. rewrite Nat.succ_pred. rewrite Nat.sub_add. reflexivity. apply (Nat.le_trans _ (S (subseq i))). apply le_S, Nat.le_refl. apply H2. apply Nat.le_refl. apply le_n_S, H4. intro abs. destruct H2, H5. specialize (H5 i (S i) (Nat.le_refl _)). apply Nat.sub_0_le in abs. apply (proj1 (Nat.le_ngt _ _) abs), H5, le_n_S, H4. + unfold IntegralFiniteSum. rewrite partition_sum_by_packets. reflexivity. exact H2. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont