proposition: Lemma DominatedConvergence : forall {IS : IntegrationSpace} (fn : nat -> @PartialFunction (RealT (ElemFunc IS)) (X (ElemFunc IS))) (fnInt : forall n:nat, IntegrableFunction (fn n)) (f g : @PartialFunction (RealT (ElemFunc IS)) (X (ElemFunc IS))) (fInt : IntegrableFunction f), CvMeasure fn f -> IntegrableFunction g -> (forall n:nat, partialFuncLe (Xabs (fn n)) g) -> CR_cv _ (fun n:nat => Integral (fnInt n)) (Integral fInt).
proof: Proof. intros IS fn fnInt f g fInt cvfn gInt fnle. assert (CvMeasure (fun n : nat => Xabs (Xminus (fn n) f)) (Xconst (X (ElemFunc IS)) 0)) as cvZero. { intros A Aint eps epsPos. specialize (cvfn A Aint eps epsPos) as [N Nmaj]. exists N. intros. specialize (Nmaj n H) as [B Bapprox]. exists B. intros. destruct xdfn. specialize (Bapprox x d0 d H0). refine (CRle_lt_trans _ _ _ _ Bapprox). simpl. rewrite (CRabs_minus_sym (partialApply f x d0)). unfold CRminus. rewrite CRplus_0_l, CRabs_opp. rewrite CRabs_right. 2: apply CRabs_pos. rewrite <- CRopp_mult_distr_l, CRmult_1_l. apply CRle_refl. } assert (forall n : nat, nonNegFunc (Xabs (Xminus (fn n) f))). { intros n x xdf. apply CRabs_pos. } assert (forall (eps : CRcarrier (RealT (ElemFunc IS))) (p : positive), 0 < eps -> 0 < eps * CR_of_Q _ (1#p)) as deltaPos. { intros. apply (CRmult_lt_0_compat _ _ _ H0). apply CR_of_Q_pos. reflexivity. } assert (forall eps : CRcarrier (RealT (ElemFunc IS)), 0 < eps -> IntegralDominated (fun n : nat => Xabs (Xminus (fn n) f)) (fun n : nat => IntegrableAbs (IntegrableMinus (fnInt n) fInt)) eps) as domin. { intros eps epsPos. destruct (IntegralSupportExists _ (IntegrablePlus _ _ gInt (IntegrableAbs fInt)) _ (deltaPos eps 2%positive epsPos)) as [t [_ [tsupp tdist]]]. remember (fun x : X (ElemFunc IS) => exists xD : Domain (Xabs (Xplus g (Xabs f))) x, t <= partialApply (Xabs (Xplus g (Xabs f))) x xD) as A. destruct (Un_cv_nat_real _ _ (IntegralTruncateLimit _ (IntegrablePlus _ _ gInt (IntegrableAbs fInt))) _ (deltaPos eps 4%positive epsPos)) as [n nmaj]. apply (Build_IntegralDominated IS _ _ _ _ O _ (deltaPos eps (4 * Pos.of_nat (S n))%positive epsPos) tsupp). intros B Bmes i _ H0. apply (CRle_lt_trans _ (Integral (RestrictedIntegrable (IntegrableAbs (IntegrableMinus (fnInt i) fInt)) (MeasurableIntersectIntegrable Bmes tsupp)) + Integral (RestrictedMeasurable (IntegrableAbs (IntegrableMinus (fnInt i) fInt)) (MeasurableSetCompl _ (IntegrableMeasurable _ tsupp))))). - rewrite <- IntegralPlus; apply IntegralNonDecreasing. intros x xdf xdg. simpl. destruct xdf, xdg, d0, d1, d2, d4, d5. rewrite (DomainProp f x d7 d3); clear d7. rewrite (DomainProp f x d6 d3); clear d6. rewrite (DomainProp _ x d5 d0); clear d5. rewrite (DomainProp _ x d4 d0); clear d4. rewrite <- CRmult_plus_distr_r. apply CRmult_le_compat_r. apply CRabs_pos. destruct d. destruct d1. destruct d2. destruct a; contradiction. rewrite CRplus_0_r. apply CRle_refl. rewrite CRplus_0_l. destruct d2. apply CRle_refl. contradict n1. intro abs. contradict n0. split; assumption. destruct d1. destruct d2. destruct a; contradiction. rewrite CRplus_0_r. apply CRlt_asym, CRzero_lt_one. rewrite CRplus_0_l. destruct d2. apply CRlt_asym, CRzero_lt_one. apply CRle_refl. - apply (CRle_lt_trans _ (Integral (RestrictedIntegrable (IntegrablePlus _ _ gInt (IntegrableAbs fInt)) (MeasurableIntersectIntegrable Bmes tsupp)) + Integral (RestrictedMeasurable (IntegrablePlus _ _ gInt (IntegrableAbs fInt)) (MeasurableSetCompl _ (IntegrableMeasurable _ tsupp))))). apply CRplus_le_compat. + apply IntegralNonDecreasing. intros x xdf xdg. destruct xdf, xdg. rewrite applyXmult, applyXmult. rewrite (DomainProp _ x d1 d). apply CRmult_le_compat_l. simpl. destruct d. apply CRlt_asym, CRzero_lt_one. apply CRle_refl. simpl. destruct d2, d0. apply (CRle_trans _ _ _ (CRabs_triang _ _)). apply CRplus_le_compat. apply fnle. rewrite <- CRopp_mult_distr_l, CRmult_1_l, CRabs_opp. rewrite (DomainProp f x d4 d3). apply CRle_refl. + apply IntegralNonDecreasing. intros x xdf xdg. destruct xdf, xdg. rewrite applyXmult, applyXmult. rewrite (DomainProp _ x d1 d). apply CRmult_le_compat_l. simpl. destruct d. apply CRlt_asym, CRzero_lt_one. apply CRle_refl. simpl. destruct d0, d2. rewrite <- CRopp_mult_distr_l, CRmult_1_l. apply (CRle_trans _ _ _ (CRabs_triang _ _)). apply CRplus_le_compat. apply fnle. rewrite CRabs_opp, (DomainProp f x d4 d3). apply CRle_refl. + apply (CRlt_le_trans _ (eps * CR_of_Q (RealT (ElemFunc IS)) (1 # 2) + eps * CR_of_Q (RealT (ElemFunc IS)) (1 # 2))). apply CRplus_le_lt_compat. specialize (nmaj (S n) (le_S _ _ (Nat.le_refl n))). apply CRlt_asym in nmaj. rewrite CRabs_minus_sym, CRabs_right in nmaj. apply (CRplus_le_reg_r (- (MeasureSet (MeasurableIntersectIntegrable Bmes tsupp) * CR_of_Q _ (Z.of_nat (S n) #1)))). apply (CRle_trans _ (eps * CR_of_Q (RealT (ElemFunc IS)) (1 # 4))). apply (CRle_trans _ (Integral (RestrictedIntegrable (IntegrablePlus g (Xabs f) gInt (IntegrableAbs fInt)) (MeasurableIntersectIntegrable Bmes tsupp)) - Integral (RestrictedIntegrable (IntegrableMinInt (Xplus g (Xabs f)) (S n) (IntegrablePlus g (Xabs f) gInt (IntegrableAbs fInt))) (MeasurableIntersectIntegrable Bmes tsupp)))). apply CRplus_le_compat_l. apply CRopp_ge_le_contravar. unfold MeasureSet. rewrite <- IntegralScale. apply IntegralNonDecreasing. intros x xdf xdg. simpl. destruct xdf, d0. destruct d. rewrite CRmult_1_l. destruct xdg. rewrite CRmult_1_r. apply CRmin_r. contradiction. rewrite CRmult_0_l. destruct xdg. rewrite CRmult_1_r. apply CR_of_Q_le. destruct n; discriminate. rewrite CRmult_0_r. apply CRle_refl. refine (CRle_trans _ _ _ _ nmaj). rewrite <- IntegralMinus, <- IntegralMinus. apply IntegralNonDecreasing. intros x xdf xdg. simpl. destruct xdf, d, d1, d0, d3, xdg, d5, d6. rewrite (DomainProp g x d3 d1), (DomainProp g x d6 d1), (DomainProp g x d5 d1), (DomainProp f x d8 d2), (DomainProp f x d7 d2), (DomainProp f x d4 d2). destruct d. destruct d0. 2: contradiction. rewrite CRmult_1_l, CRmult_1_l. apply CRle_refl. rewrite CRmult_0_l. destruct d0. contradiction. rewrite CRmult_0_l. rewrite CRmult_0_r, CRplus_0_l. rewrite <- CRopp_mult_distr_l, CRmult_1_l. rewrite <- (CRplus_opp_r (CRmin (partialApply g x d1 + CRabs (RealT (ElemFunc IS)) (partialApply f x d2)) (INR (S n)))). apply CRplus_le_compat_r. apply CRmin_l. rewrite <- CRplus_0_r. setoid_replace (eps * CR_of_Q (RealT (ElemFunc IS)) (1 # 2)) with (eps * CR_of_Q (RealT (ElemFunc IS)) (1 # 4) + eps * CR_of_Q (RealT (ElemFunc IS)) (1 # 4)). rewrite CRplus_assoc. apply CRplus_le_compat_l. rewrite <- (CRplus_opp_r (MeasureSet (MeasurableIntersectIntegrable Bmes tsupp) * CR_of_Q (RealT (ElemFunc IS)) (Z.of_nat (S n) # 1))). apply CRplus_le_compat_r. apply (CRmult_le_reg_r (CR_of_Q (RealT (ElemFunc IS)) (1 # Pos.of_nat (S n)))). apply CR_of_Q_pos. reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((Z.of_nat (S n) # 1) * (1 # Pos.of_nat (S n)))%Q with 1%Q. rewrite CRmult_1_r, CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 4) * (1 # Pos.of_nat (S n)))%Q with (1 # 4 * Pos.of_nat (S n))%Q. apply CRlt_asym, H0. reflexivity. unfold Qeq, Qmult, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r, Z.mul_1_l, Pos.mul_1_l. unfold Z.of_nat. rewrite Pos.of_nat_succ. reflexivity. rewrite <- CRmult_plus_distr_l. apply CRmult_morph. reflexivity. rewrite <- CR_of_Q_plus. apply CR_of_Q_morph. reflexivity. rewrite <- IntegralMinus. apply IntegralNonNeg. intros x xdf. simpl. destruct xdf, d, d0. rewrite <- CRopp_mult_distr_l, CRmult_1_l. rewrite <- (CRplus_opp_r (CRmin (partialApply g x d0 + CRabs (RealT (ElemFunc IS)) (partialApply f x d2)) (INR (S n)))). apply CRplus_le_compat_r. rewrite (DomainProp g x d0 d), (DomainProp f x d2 d1). apply CRmin_l. refine (CRle_lt_trans _ _ _ _ tdist). apply IntegralNonDecreasing. intros x xdf xdg. simpl. destruct xdf, xdg, d0, d1, d2, d5. destruct d. 2: rewrite CRmult_0_l; apply CRabs_pos. rewrite CRmult_1_l. destruct d2. contradiction. rewrite CRmult_0_l, CRmult_0_r, CRplus_0_r. rewrite (DomainProp g x d1 d0), (DomainProp f x d4 d3). apply CRle_abs. rewrite <- CRmult_plus_distr_l, <- CR_of_Q_plus. setoid_replace ((1 # 2) + (1 # 2))%Q with 1%Q. rewrite CRmult_1_r. apply CRle_refl. reflexivity. } intro p. destruct (DominatedMeasureCvZero (fun n : nat => Xabs (Xminus (fn n) f)) (fun n => IntegrableAbs (IntegrableMinus (fnInt n) fInt)) cvZero H domin p) as [n nmaj]. exists n. intros. specialize (nmaj i H0). unfold CRminus in nmaj. rewrite CRopp_0, CRplus_0_r, CRabs_right in nmaj. refine (CRle_trans _ _ _ _ nmaj). clear nmaj. refine (CRle_trans _ _ _ _ (IntegralTriangle _ _)). rewrite (CRabs_morph _ (Integral (IntegrableMinus (fnInt i) fInt))). apply CRle_refl. rewrite <- IntegralMinus. reflexivity. apply IntegralNonNeg. intros x xdf. apply CRabs_pos. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile