proposition: Lemma IntegralFunctionCast : forall {IS : IntegrationSpace} {R : ConstructiveReals} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f), Integral (@IntegrableFunctionCast IS R f fInt) == CRcast (Integral fInt).
proof: Proof. intros. unfold Integral. apply (series_cv_unique _ _ _ (IntegralCv (let (i, _) := IntegrableFunctionCast f fInt in i))). apply CRmorph_series_cv. apply (series_cv_eq (fun n : nat => I IS (IntFn (let (i, _) := fInt in i) n) (IntFnL (let (i, _) := fInt in i) n))). 2: exact (IntegralCv (let (i, _) := fInt in i)). intro n. apply IExtensional. intros. destruct fInt, x0. unfold IntegrableFunctionCast, CMTIntegrableFunctions.IntFn. simpl. unfold CRcast. transitivity (CRmorph (CRmorph_compose (@SlowConstructiveRealsMorphism (RealT (ElemFunc IS)) R) (@SlowConstructiveRealsMorphism (RealT (FunctionRieszSpaceCast (ElemFunc IS))) (RealT (ElemFunc IS)))) (partialApply (IntFn n) x y)). rewrite Endomorph_id. apply DomainProp. reflexivity. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets