proposition: Lemma UC_integral_plus : forall {R : ConstructiveReals} (f g : CRcarrier R -> CRcarrier R) (a b : CRcarrier R) (modF modG modS : forall eps:CRcarrier R, 0 < eps -> CRcarrier R) (fCont : UniformCont f modF) (gCont : UniformCont g modG) (sCont : UniformCont (fun x => (f x) + (g x)) modS) (leab leabb : a <= b), UC_integral (fun x => (f x) + (g x)) a b modS sCont leab == UC_integral f a b modF fCont leabb + UC_integral g a b modG gCont leabb.
proof: Proof. intros. unfold UC_integral. destruct (CR_complete R (fun last : nat => IntegralFiniteSum f (fun n : nat => a + (b - a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) (fun n : nat => a + (b - a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) last) (UC_integral_cauchy f a b modF fCont leabb)). destruct (CR_complete R (fun last : nat => IntegralFiniteSum g (fun n : nat => a + (b - a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) (fun n : nat => a + (b - a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) last) (UC_integral_cauchy g a b modG gCont leabb)). destruct (CR_complete R (fun last : nat => IntegralFiniteSum (fun x1 : CRcarrier R => f x1 + g x1) (fun n : nat => a + (b - a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) (fun n : nat => a + (b - a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) last) (UC_integral_cauchy (fun x1 : CRcarrier R => f x1 + g x1) a b modS sCont leab)). apply (CR_cv_unique _ _ _ c1). apply (CR_cv_eq _ (fun last : nat => (IntegralFiniteSum f (fun n : nat => (a + (b - a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last)))) (fun n : nat => (a + (b - a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last)))) last) + (IntegralFiniteSum g (fun n : nat => (a + (b - a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last)))) (fun n : nat => (a + (b - a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last)))) last))). intro n. unfold IntegralFiniteSum. rewrite <- sum_plus. apply CRsum_eq. 2: apply CR_cv_plus; assumption. intros. generalize (f (a + (b - a) * CR_of_Q R (Z.of_nat i # Pos.of_nat (S n)))), (g (a + (b - a) * CR_of_Q R (Z.of_nat i # Pos.of_nat (S n)))). intros. setoid_replace (a + (b - a) * CR_of_Q R (Z.of_nat (S i) # Pos.of_nat (S n)) - (a + (b - a) * CR_of_Q R (Z.of_nat i # Pos.of_nat (S n)))) with ((b - a) * CR_of_Q R (Z.of_nat (S i) # Pos.of_nat (S n)) - (b - a) * CR_of_Q R (Z.of_nat i # Pos.of_nat (S n))). rewrite <- CRmult_plus_distr_r. reflexivity. unfold CRminus. rewrite (CRplus_comm a), CRopp_plus_distr. rewrite CRplus_assoc, <- (CRplus_assoc a), CRplus_opp_r, CRplus_0_l. reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont