proposition: Lemma DominatedMeasureCvZero : forall {IS : IntegrationSpace} (fn : nat -> @PartialFunction (RealT (ElemFunc IS)) (X (ElemFunc IS))) (fnInt : forall n:nat, IntegrableFunction (fn n)), CvMeasure fn (Xconst _ 0) -> (forall n:nat, nonNegFunc (fn n)) -> (forall (eps : CRcarrier (RealT (ElemFunc IS))) (epsPos : 0 < eps), IntegralDominated fn fnInt eps) -> CR_cv _ (fun n:nat => Integral (fnInt n)) 0.
proof: Proof. intros IS fn fnInt fnCvZero fnPos fnDominated. apply Un_cv_real_nat. intros eps epsPos. assert (0 < eps * CR_of_Q _ (1#2)) as halfEpsPos. { apply CRmult_lt_0_compat. exact epsPos. apply CR_of_Q_pos. reflexivity. } destruct (fnDominated _ halfEpsPos). assert (0 < MeasureSet idom_int0 + 1) as H. { apply (CRlt_le_trans _ 1). apply CRzero_lt_one. rewrite <- (CRplus_0_l 1), <- CRplus_assoc. apply CRplus_le_compat_r. rewrite CRplus_0_r. apply MeasureNonNeg. } assert (0 < CRmin (eps * CR_of_Q _ (1#2) * CRinv _ _ (inr H)) idom_delta0) as H0. { apply CRmin_lt. 2: exact idom_delta_pos0. apply CRmult_lt_0_compat. apply CRmult_lt_0_compat. exact epsPos. apply CR_of_Q_pos. reflexivity. apply CRinv_0_lt_compat, H. } specialize (fnCvZero idom_support0 idom_int0 _ H0) as [N Nmaj]. exists (max N idom_idx0). intros. specialize (Nmaj i (Nat.le_trans _ _ _ (Nat.le_max_l _ _) H1)) as [[C Cint] Cmaj]. unfold sa_approx in Cmaj. assert (Integral (MeasurableIntersectIntegrable (MeasurableSetCompl C (IntegrableMeasurable (CharacFunc C) Cint)) idom_int0) < idom_delta0) as H2. { apply (CRlt_le_trans _ (CRmin (eps * CR_of_Q _ (1#2) * (/ (MeasureSet idom_int0 + 1)) (inr H)) idom_delta0)). 2: apply CRmin_r. refine (CRle_lt_trans _ _ _ _ sa_mes0). rewrite <- MeasureDifferenceIncluded. 2: exact sa_inc0. apply IntegralNonDecreasing. intros x xdf xdg. simpl. destruct xdf. destruct xdg. apply CRle_refl. contradict n. split; apply a. destruct xdg. apply CRlt_asym, CRzero_lt_one. apply CRle_refl. } assert (le idom_idx0 i). { apply (Nat.le_trans _ (max N idom_idx0)). apply Nat.le_max_r. exact H1. } specialize (idom_dom0 _ _ _ H3 H2). clear H2 H3. apply (CRle_lt_trans _ (Integral (RestrictedMeasurable (fnInt i) (MeasurableSetCompl C (IntegrableMeasurable (CharacFunc C) Cint))) + Integral (RestrictedIntegrable (fnInt i) Cint))). unfold CRminus. rewrite CRopp_0, CRplus_0_r, CRabs_right. - rewrite <- IntegralPlus. apply IntegralNonDecreasing. intros x xdf xdg. simpl. destruct xdg, d, d0. rewrite (DomainProp _ x d2 xdf), (DomainProp _ x d1 xdf). destruct d, d0. contradiction. rewrite CRmult_0_l, CRmult_1_l, CRplus_0_r. apply CRle_refl. rewrite CRmult_0_l, CRmult_1_l, CRplus_0_l. apply CRle_refl. contradiction. - exact (IntegralNonNeg _ _ (fnPos i)). - apply (CRlt_le_trans _ (eps * CR_of_Q (RealT (ElemFunc IS)) (1 # 2) + eps * CR_of_Q (RealT (ElemFunc IS)) (1 # 2))). apply (CRplus_lt_le_compat _ _ _ _ idom_dom0). clear idom_dom0. apply (CRle_trans _ (MeasureSet Cint * (eps * CR_of_Q (RealT (ElemFunc IS)) (1 # 2) * (/ (MeasureSet idom_int0 + 1)) (inr H)))). unfold MeasureSet. rewrite <- IntegralScale. apply IntegralNonDecreasing. + intros x xdf xdg. simpl. destruct xdf, d, xdg. rewrite CRmult_1_l, CRmult_1_r. clear c0. specialize (Cmaj x Logic.I d0 c). apply CRlt_asym in Cmaj. simpl in Cmaj. unfold CRminus in Cmaj. rewrite CRplus_0_l, CRabs_opp, CRabs_right in Cmaj. apply (CRle_trans _ _ _ Cmaj (CRmin_l _ _)). apply fnPos. contradiction. contradiction. rewrite CRmult_0_l, CRmult_0_r. apply CRle_refl. + rewrite CRmult_comm, CRmult_assoc. apply (CRle_trans _ (eps * CR_of_Q (RealT (ElemFunc IS)) (1 # 2) * 1)). 2: rewrite CRmult_1_r; apply CRle_refl. apply CRmult_le_compat_l. apply CRmult_le_0_compat. apply CRlt_asym, epsPos. apply CR_of_Q_le. discriminate. apply (CRmult_le_reg_l (MeasureSet idom_int0 + 1) _ _ H). rewrite CRmult_1_r, <- CRmult_assoc, CRinv_r, CRmult_1_l. apply (CRle_trans _ (MeasureSet idom_int0 + 0)). rewrite CRplus_0_r. exact (MeasureNonDecreasing _ _ _ _ sa_inc0). apply CRplus_le_compat_l. apply CRlt_asym, CRzero_lt_one. + rewrite <- CRmult_plus_distr_l, <- CR_of_Q_plus. setoid_replace ((1 # 2) + (1 # 2))%Q with 1%Q. 2: reflexivity. rewrite CRmult_1_r. apply CRle_refl. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile