proposition: Lemma IElemProductExtensional : forall { I J : IntegrationSpace } (f : PartialFunction (X (ProductFunctionRieszSpace I J))) (fl : list (@ProdIntegrable I J)) (fres : PartialRestriction (ProdLFunc fl) f) (g : PartialFunction (X (ProductFunctionRieszSpace I J))) (gL : L (ProductFunctionRieszSpace I J) g) , (forall x (xD : Domain (ProdLFunc fl) x) (yD : Domain g x), partialApply _ x xD == partialApply g x yD) -> IElemProduct f (existT _ fl fres) == IElemProduct g gL.
proof: Proof. intros I J f fl fres g gL res. destruct gL. do 2 rewrite IElemProductFubini. apply IntegralExtensional. intros. simpl. apply (@IntegralExtensional (IntegrationSpaceCast J)). intros. simpl. destruct p, fres. rewrite (c _ xdg0 (d _ xdg0)). apply res. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile