proposition: Lemma UC_integral_sum : forall {R : ConstructiveReals} (fn : nat -> CRcarrier R -> CRcarrier R) (a b : CRcarrier R) (n : nat) (modFn : forall (n:nat) (eps:CRcarrier R), 0 < eps -> CRcarrier R) (modSn : forall (eps:CRcarrier R), 0 < eps -> CRcarrier R) (fnCont : forall k:nat, UniformCont (fn k) (modFn k)) (sCont : UniformCont (fun x => CRsum (fun k => (fn k x)) n) modSn) (leab : a <= b), UC_integral (fun x => CRsum (fun k => (fn k x)) n) a b modSn sCont leab == CRsum (fun k => UC_integral (fn k) a b (modFn k) (fnCont k) leab) n.
proof: Proof. induction n. - intros. simpl. apply UC_integral_extens. intros. reflexivity. - intros. simpl. destruct (UC_sum fn modFn fnCont n) as [modS c]. rewrite <- (IHn _ _ _ c). apply UC_integral_plus. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont