proposition: Lemma UC_compare_integrals : forall {Re : ConstructiveReals} (f : CRcarrier Re -> CRcarrier Re) (a b eps epsR : CRcarrier Re) (cont_mod : forall eps:CRcarrier Re, 0 < eps -> CRcarrier Re) (P R Q : @IntervalPartition Re a b) (epsPos : 0 < eps) (epsPosR : 0 < epsR) (subseq : nat -> nat) (subseqR : nat -> nat), UniformCont f cont_mod -> IntervalPartitionRefinement _ _ P Q subseq -> IntervalPartitionRefinement _ _ R Q subseqR -> (PartitionMesh (ipt_seq P) (S (ipt_last P))) < (cont_mod eps epsPos) -> (PartitionMesh (ipt_seq R) (S (ipt_last R))) < (cont_mod epsR epsPosR) -> CRabs _ (IntegralFiniteSum f (ipt_seq P) (ipt_seq P) (ipt_last P) - IntegralFiniteSum f (ipt_seq R) (ipt_seq R) (ipt_last R)) <= (eps+epsR) * (b-a).
proof: Proof. intros. setoid_replace (IntegralFiniteSum f (ipt_seq P) (ipt_seq P) (ipt_last P) - IntegralFiniteSum f (ipt_seq R) (ipt_seq R) (ipt_last R)) with (IntegralFiniteSum f (ipt_seq P) (ipt_seq P) (ipt_last P) - (IntegralFiniteSum f (ipt_seq Q) (ipt_seq Q) (ipt_last Q)) + (IntegralFiniteSum f (ipt_seq Q) (ipt_seq Q) (ipt_last Q) - IntegralFiniteSum f (ipt_seq R) (ipt_seq R) (ipt_last R))). apply (CRle_trans _ _ _ (CRabs_triang _ _)). rewrite CRmult_plus_distr_r. apply CRplus_le_compat. - apply (UC_refine_integral f a b eps cont_mod _ _ _ _ epsPos subseq). exact H. apply WeavedListSelf, ipt_ordered. apply WeavedListSelf, ipt_ordered. exact H0. exact H2. - rewrite CRabs_minus_sym. apply (UC_refine_integral f a b epsR cont_mod _ _ _ _ epsPosR subseqR). exact H. apply WeavedListSelf, ipt_ordered. apply WeavedListSelf, ipt_ordered. exact H1. exact H3. - unfold CRminus. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont