proposition: Lemma IntegralMonotoneConvergenceDecr (IS : IntegrationSpace) (fn : nat -> PartialFunction (X (ElemFunc IS))) (fnInt : forall n:nat, IntegrableFunction (fn n)) (a : CRcarrier (RealT (ElemFunc IS))) : (forall n:nat, partialFuncLe (fn (S n)) (fn n)) -> CR_cv _ (fun n:nat => Integral (fnInt n)) a -> { limInt : IntegrableFunction (XpointwiseLimit fn) | Integral limInt == a }.
proof: Proof. intros. destruct (IntegrableXpointwiseLimit fn fnInt (Integral (fnInt O) - a)). - apply (CR_cv_eq _ (fun n => Integral (fnInt O) - Integral (fnInt (S n)))). induction n. simpl. rewrite <- IntegralMinus. apply IntegralExtensional. intros. rewrite applyXabs, CRabs_left. simpl. destruct xdf, xdg. rewrite CRopp_plus_distr. rewrite <- CRopp_mult_distr_l, <- CRopp_mult_distr_l. rewrite CRmult_1_l, CRmult_1_l, CRopp_involutive, CRplus_comm. rewrite (DomainProp _ x d1 d0), (DomainProp _ x d d2). reflexivity. destruct xdg. rewrite (applyXminus (fn 1%nat) (fn O)). rewrite <- (CRplus_opp_r (partialApply (fn O) x d0)). apply CRplus_le_compat_r. apply H. simpl. rewrite <- IHn. unfold CRminus. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite <- CRplus_0_l, <- (CRplus_opp_l (Integral (fnInt (S n)))). rewrite CRplus_assoc. apply CRplus_morph. reflexivity. pose proof (IntegralMinus (fn (S n))). unfold CRminus in H1. rewrite <- H1. apply IntegralExtensional. intros. rewrite applyXabs, CRabs_left. simpl. destruct xdf, xdg. rewrite CRopp_plus_distr. rewrite <- CRopp_mult_distr_l, <- CRopp_mult_distr_l. rewrite CRmult_1_l, CRmult_1_l, CRopp_involutive, CRplus_comm. rewrite (DomainProp _ x d1 d0), (DomainProp _ x d d2). reflexivity. destruct xdg. rewrite (applyXminus (fn (S (S n))) (fn (S n))). rewrite <- (CRplus_opp_r (partialApply (fn (S n)) x d0)). apply CRplus_le_compat_r. apply H. apply CR_cv_minus. apply CR_cv_const. apply (CR_cv_shift' _ 1) in H0. apply (CR_cv_eq _ (fun n : nat => Integral (fnInt (n + 1)%nat))). 2: exact H0. intro n. rewrite Nat.add_comm. reflexivity. - exists x. exact (CR_cv_unique _ _ _ c H0). Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions