proposition: Lemma CvMeasureMeasurable : forall {IS : IntegrationSpace} (fn : nat -> @PartialFunction (RealT (ElemFunc IS)) (X (ElemFunc IS))) (f : @PartialFunction (RealT (ElemFunc IS)) (X (ElemFunc IS))), almost_everywhere (Domain f) -> (forall n:nat, MeasurableFunction (fn n)) -> CvMeasure fn f -> MeasurableFunction f.
proof: Proof. intros IS fn f fFull fnMes fnCv. apply (MeasurableGenApprox f fFull). intros. specialize (fnCv A Aint eps epsPos) as [N Ncv]. specialize (Ncv N (Nat.le_refl N)) as [B Bcv]. specialize (fnMes N A n Aint). exists (pair (XmaxConst (XminConst (Xmult (CharacFunc A) (fn N)) (CR_of_Q (RealT (ElemFunc IS)) (Z.pos n # 1))) (CR_of_Q (RealT (ElemFunc IS)) (Z.neg n # 1))) B). split. exact fnMes. unfold fst, snd. intros. specialize (Bcv x xdh (snd xdf) H). refine (CRle_lt_trans _ _ _ _ Bcv). clear Bcv. rewrite applyXmaxConst, applyXmaxConst. apply (CRle_trans _ _ _ (CRmax_contract _ _ _)). rewrite applyXminConst, applyXminConst. apply (CRle_trans _ _ _ (CRmin_contract _ _ _)). simpl. destruct xdf, d. rewrite CRmult_1_l. apply CRle_refl. contradict n0. apply (sa_inc _ _ _ _ x H). Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile