proposition: Lemma IntegrableFunctionsComplete : forall (IS : IntegrationSpace) (fn : nat -> PartialFunction (X (ElemFunc IS))) (fnInt : forall n:nat, IntegrableFunction (fn n)) (sumIAbsFn : CRcarrier (RealT (ElemFunc IS))), (series_cv (fun k:nat => Integral (IntegrableAbs (fnInt k))) sumIAbsFn) -> { represInt : IntegralRepresentation & prod (PartialRestriction (XinfiniteSumAbs (IntFn represInt)) (XinfiniteSumAbs fn)) (series_cv (fun n => Integral (fnInt n)) (IntegralSeries represInt)) }.
proof: Proof. intros. pose proof (CompleteRepresentationRestrict IS fn fnInt) as complRestrict. destruct (CompleteRepresentation IS fn fnInt) as [intRepresN restrN]. destruct (series_cv_maj (fun n => IntAbsSum (intRepresN n)) (fun n => Integral (IntegrableAbs (fnInt n)) + CRpow (CR_of_Q _ (1#2)) n) (sumIAbsFn + CR_of_Q _ 2)) as [s [cvs majS]]. - intro n. rewrite CRabs_right. apply (restrN n). destruct (intRepresN n); simpl. apply (series_cv_nonneg (fun k : nat => Iabs (IntFn k) (IntFnL k))). intro n0. apply integralPositive. intros x xdf. rewrite applyXabs. apply CRabs_pos. assumption. - apply series_cv_plus. apply H. apply GeoHalfTwo. - assert (series_cv (fun k : nat => Iabs (diagSeq (fun n k0 : nat => IntFn (intRepresN n) k0) k) (diagSeqL IS (fun n k0 : nat => IntFn (intRepresN n) k0) (fun n k0 : nat => IntFnL (intRepresN n) k0) k)) s). { apply (series_cv_eq (diagSeq (fun n k => Iabs (IntFn (intRepresN n) k) (IntFnL (intRepresN n) k)))). intro n. unfold diagSeq, diagSeqL. destruct (diagPlaneInv n). reflexivity. apply (DiagSeqInfiniteSumColPos _ (fun n : nat => IntAbsSum (intRepresN n))). intros n k. apply integralPositive. intros x xdf. rewrite applyXabs. apply CRabs_pos. intro n. apply (intRepresN n). assumption. } exists (Build_IntegralRepresentation IS (diagSeq (fun n k => IntFn (intRepresN n) k)) (diagSeqL IS _ (fun n k => IntFnL (intRepresN n) k)) s H0). split. + exact complRestrict. + pose proof (IntegralCv {| IntFn := diagSeq (fun n k : nat => IntFn (intRepresN n) k); IntFnL := diagSeqL IS (fun n k : nat => IntFn (intRepresN n) k) (fun n k : nat => IntFnL (intRepresN n) k); IntAbsSum := s; IntAbsSumCv := H0 |}); simpl. simpl in H1. destruct (series_cv_maj (diagSeq (fun n k : nat => CRabs _ (I IS _ (IntFnL (intRepresN n) k)))) (fun k : nat => Iabs _ (diagSeqL IS (fun n k0 : nat => IntFn (intRepresN n) k0) (fun n k0 : nat => IntFnL (intRepresN n) k0) k)) s). intro n. rewrite CRabs_right. unfold diagSeq, diagSeqL. destruct (diagPlaneInv n). apply integralAbsMaj. unfold diagSeq. destruct (diagPlaneInv n). apply CRabs_pos. assumption. destruct (DiagSeqInfiniteSum (fun n k => I IS _ (IntFnL (intRepresN n) k)) (fun n : nat => Integral (fnInt n)) x). apply p. intro n. clear p. clear x. pose proof (IntegralRepresentationInvariant (fn n) (existT _ (intRepresN n) (fst (restrN n))) (fnInt n)). rewrite <- H2. apply (IntegralCv (intRepresN n)). destruct (series_cv_maj (fun n : nat => I IS _ (diagSeqL IS (fun n0 k : nat => IntFn (intRepresN n0) k) (fun n0 k : nat => IntFnL (intRepresN n0) k) n)) (fun k : nat => Iabs _ (diagSeqL IS (fun n k0 : nat => IntFn (intRepresN n) k0) (fun n k0 : nat => IntFnL (intRepresN n) k0) k)) s (fun n : nat => integralAbsMaj _ (diagSeqL IS (fun n0 k : nat => IntFn (intRepresN n0) k) (fun n0 k : nat => IntFnL (intRepresN n0) k) n)) H0). setoid_replace x1 with x0. apply p0. apply (series_cv_unique (diagSeq (fun n k : nat => I IS (IntFn (intRepresN n) k) (IntFnL (intRepresN n) k)))). 2: apply p0. apply (series_cv_eq (fun n : nat => I IS _ (diagSeqL IS (fun n0 k : nat => IntFn (intRepresN n0) k) (fun n0 k : nat => IntFnL (intRepresN n0) k) n))). intro n. unfold diagSeq, diagSeqL. destruct (diagPlaneInv n). reflexivity. assumption. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions