proposition: Lemma IElemProductFubini : forall { I J : IntegrationSpace } (f : PartialFunction (prod (X (ElemFunc I)) (X (ElemFunc J)))) (l : list ProdIntegrable) (res : PartialRestriction (ProdLFunc l) f), IElemProduct f (existT _ l res) == Integral (LElemProductIntegralFstIntegrable l).
proof: Proof. intros. simpl. clear res f. induction l. - simpl. rewrite <- (@IntegralZeroIsZero I). apply IntegralExtensional. simpl. intros. rewrite (@IntegralExtensional (IntegrationSpaceCast J) _ _ (LElemProductIntegrableAEspec nil x xdg) IntegrableZero). symmetry. apply (@IntegralZeroIsZero (IntegrationSpaceCast J)). reflexivity. - simpl. rewrite IHl. clear IHl. setoid_replace (prodint_factor a * MeasureSet (prodint_fint a) * CRcast (MeasureSet (prodint_gint a))) with (Integral (ProdIntegrableFuncIntegrable a)). + rewrite <- (@IntegralPlus I). apply IntegralExtensional. intros; simpl in xdf, xdg. destruct xdf as [s d]. unfold Xplus, XbinOp, XbinOpXY, IntegralFst, partialApply. unfold ProdIntegrableFuncIntegrableAE. rewrite IntegralRestrict. rewrite <- (@IntegralPlus (IntegrationSpaceCast J) _ _ _ (LElemProductIntegrableAEspec l x d)); apply (@IntegralExtensional (IntegrationSpaceCast J)). intros. destruct xdf, xdg0, d2. simpl. apply CRplus_morph. 2: apply DomainProp. destruct s. destruct d2. 2: contradiction. destruct d0. destruct d4. reflexivity. contradiction. destruct d4. contradiction. reflexivity. destruct d2. contradiction. rewrite CRmult_0_r, CRmult_0_l, CRmult_0_l. reflexivity. + unfold ProdIntegrableFuncIntegrable; rewrite IntegralRestrict. rewrite IntegralScale. rewrite (CRmult_comm (Integral (prodint_fint a))). do 2 rewrite CRmult_assoc. apply CRmult_morph. reflexivity. rewrite CRmult_comm. reflexivity. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile