proposition: Lemma IntegralPlus : forall {IS : IntegrationSpace} (f g : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (gInt : IntegrableFunction g), Integral (IntegrablePlus f g fInt gInt) == Integral fInt + Integral gInt.
proof: Proof. intros. destruct (IntegrablePlus f g fInt gInt) as [[pn pnL IsumP majP] restrictP] eqn:desP. destruct fInt as [[fn fnL IsumF majF] restrictF]. destruct gInt as [[gn gnL IsumG majG] restrictG]. simpl. apply (series_cv_unique (weaveSequences _ (fun n0 : nat => I IS (fn n0) (fnL n0)) (fun n0 : nat => I IS (gn n0) (gnL n0)))). simpl in desP. - apply (series_cv_eq (fun n : nat => I IS (pn n) (pnL n))). + intro n. unfold IntegrablePlus in desP; simpl in desP. inversion desP. inversion H1. unfold weaveSequences, weaveSequencesL. destruct (Nat.even n); reflexivity. + pose proof (IntegralCv {| IntFn := pn; IntFnL := pnL; IntAbsSum := IsumP; IntAbsSumCv := majP |}). assumption. - apply weaveInfiniteSums. + pose proof (IntegralCv {| IntFn := fn; IntFnL := fnL; IntAbsSum := IsumF; IntAbsSumCv := majF |}). assumption. + pose proof (IntegralCv {| IntFn := gn; IntFnL := gnL; IntAbsSum := IsumG; IntAbsSumCv := majG |}). assumption. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase