proposition: Lemma LElemProductIntegrableAEspec : forall { I J : IntegrationSpace } (l : list (@ProdIntegrable I J)) (x : X (ElemFunc I)), Domain (XsumList (map (fun pi => @CharacFunc (RealT (ElemFunc I)) _ (prodint_f pi)) l)) x -> @IntegrableFunction (IntegrationSpaceCast J) (Xproj1 (ProdLFunc l) x).
proof: Proof. intros I J l x xDS. induction l. - apply (IntegrableFunctionExtensional (Xconst _ 0)). split. intros y H0. simpl. trivial. intros. apply DomainProp. apply IntegrableZero. - unfold ProdLFunc. simpl. apply (@IntegrableFunctionExtensional (IntegrationSpaceCast J) (Xplus (Xproj1 (ProdIntegrableFunc a) x) (Xproj1 (XsumList (map ProdIntegrableFunc l)) x))). split. intros y H0. apply H0. intros. destruct xD, xG. apply CRplus_morph. apply CRmult_morph. apply CRmult_morph. reflexivity. apply DomainProp. apply DomainProp. simpl. apply DomainProp. apply (@IntegrablePlus (IntegrationSpaceCast J)). 2: apply IHl, xDS. destruct xDS. apply (@IntegrableFunctionExtensional (IntegrationSpaceCast J) (Xscale (prodint_factor a * partialApply _ x d) (CharacFunc (prodint_g a)))). split. intros y H. split. exact d. exact H. intros. apply CRmult_morph. apply CRmult_morph. reflexivity. apply DomainProp. apply DomainProp. apply (@IntegrableScale (IntegrationSpaceCast J)). apply (@IntegrableFunctionExtensional (IntegrationSpaceCast J) (@PartialFunctionCast (RealT (ElemFunc J)) (RealT (ElemFunc I)) _ (CharacFunc (prodint_g a)))). split. intros y ydf. exact ydf. intros. simpl. destruct xD, xG. apply CRmorph_one. contradiction. contradiction. apply CRmorph_zero. exact (@IntegrableFunctionCast J _ (CharacFunc (prodint_g a)) (prodint_gint a)). Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile