proposition: Lemma IcontinuousCast : forall (IS : IntegrationSpace) {R : ConstructiveReals}, ElemIntegralContinuous (fun (f : PartialFunction (X (FunctionRieszSpaceCast (ElemFunc IS)))) (fL : L (@FunctionRieszSpaceCast R (ElemFunc IS)) f) => CRcast (I IS (PartialFunctionCast f) fL)).
proof: Proof. intros IS R f fn fL fnL fnPos [l [lcv lmaj]]. destruct (Icontinuous IS (PartialFunctionCast f) (fun n => PartialFunctionCast (fn n)) fL fnL). - intros n x xdf. simpl. unfold CRcast. rewrite <- (CRmorph_zero (@SlowConstructiveRealsMorphism R (RealT (ElemFunc IS)))). apply CRmorph_le, fnPos. - exists (CRcast l). split. apply (series_cv_eq (fun n => (CRmorph (CRmorph_compose (@SlowConstructiveRealsMorphism (RealT (ElemFunc IS)) R) (@SlowConstructiveRealsMorphism (RealT (FunctionRieszSpaceCast (ElemFunc IS))) (RealT (ElemFunc IS))) ) (I IS (PartialFunctionCast (fn n)) (fnL n))))). intro n. apply Endomorph_id. unfold CRmorph_compose, CRmorph. apply CRmorph_series_cv, lcv. rewrite <- (Endomorph_id (CRmorph_compose (@SlowConstructiveRealsMorphism (RealT (ElemFunc IS)) R) (@SlowConstructiveRealsMorphism (RealT (FunctionRieszSpaceCast (ElemFunc IS))) (RealT (ElemFunc IS))) ) (I IS (PartialFunctionCast f) fL)). unfold CRcast. unfold CRmorph_compose, CRmorph. apply CRmorph_increasing. exact lmaj. - destruct x. simpl in s. exists (Build_CommonPointFunSeq _ _ f fn cpx cpxF cpxFn). simpl. destruct s. exists (CRcast x). split. apply (series_cv_eq (fun n => (CRmorph (CRmorph_compose (@SlowConstructiveRealsMorphism (RealT (FunctionRieszSpaceCast (ElemFunc IS))) (RealT (ElemFunc IS))) (@SlowConstructiveRealsMorphism (RealT (ElemFunc IS)) R) ) (partialApply (fn n) cpx (cpxFn n))))). intro n. apply Endomorph_id. unfold CRmorph_compose, CRmorph. apply CRmorph_series_cv, p. rewrite <- (Endomorph_id (CRmorph_compose (@SlowConstructiveRealsMorphism (RealT (FunctionRieszSpaceCast (ElemFunc IS))) (RealT (ElemFunc IS))) (@SlowConstructiveRealsMorphism (RealT (ElemFunc IS)) R) ) (partialApply f cpx cpxF)). unfold CRcast. unfold CRmorph_compose, CRmorph. apply CRmorph_increasing. apply p. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets