proposition: Lemma ProductIContinuous { I J : IntegrationSpace } : @ElemIntegralContinuous (ProductFunctionRieszSpace I J) IElemProduct.
proof: Proof. intros f fn fL fnL fnNonNeg cv. destruct fL as [fl fL]. pose (fun n => let (l,_) := fnL n in l) as ln. assert (forall n:nat, PartialRestriction (ProdLFunc (ln n)) (fn n)) as resn. { intro n. unfold ln. destruct (fnL n). exact p. } destruct (IntegrableContinuous (IntegralFst (ProdLFunc fl) (LElemProductIntegrableAE fl)) (fun n => IntegralFst (ProdLFunc (ln n)) (LElemProductIntegrableAE (ln n))) (LElemProductIntegralFstIntegrable fl) (fun n => LElemProductIntegralFstIntegrable (ln n))) as [x [limx xcv]]. intro n. apply IntegralFstNonNeg. intros t tdf. destruct (resn n). rewrite (c t tdf (d t tdf)). apply fnNonNeg. destruct cv, p. simpl in x. exists x. split. apply (series_cv_eq (fun n : nat => IElemProduct (fn n) (fnL n))). 2: exact s. intro n. unfold ln. destruct (fnL n). rewrite IElemProductFubini. reflexivity. simpl. rewrite IElemProductFubini in c. exact c. assert (forall n:nat, Domain (XsumList (map (fun x : ProdIntegrable => @CharacFunc (RealT (ElemFunc I)) _ (prodint_f x)) (ln n))) (cpx _ _ _ x)) as H2. { intro n. apply (cpxFn _ _ _ x n). } assert (forall n:nat, @IntegrableFunction (IntegrationSpaceCast J) (Xproj1 (ProdLFunc (ln n)) (cpx _ _ _ x))) as fnInt. { intro n. specialize (H2 n). unfold ln. unfold ln in H2. destruct (fnL n). apply LElemProductIntegrableAEspec. exact H2. } destruct (@IntegrableContinuous (IntegrationSpaceCast J) (Xproj1 (ProdLFunc fl) (cpx _ _ _ x)) (fun n => Xproj1 (ProdLFunc (ln n)) (cpx _ _ _ x)) (LElemProductIntegrableAEspec fl (cpx _ _ _ x) (cpxF _ _ _ x)) fnInt) as [y ycv]. intro n. intros y ydf. pose proof (Xproj1Restriction _ _ (cpx _ _ _ x) (resn n)) as [d c]. rewrite (c y ydf (d y ydf)). apply fnNonNeg. exists limx. destruct xcv. split. apply (series_cv_eq (fun n : nat => partialApply (IntegralFst (ProdLFunc (ln n)) (LElemProductIntegrableAE (ln n))) (cpx _ _ _ x) (cpxFn _ _ _ x n))). 2: exact s. intro n. apply applyIntegralFst. destruct x. simpl in c. simpl. exact c. destruct fL. assert (forall n : nat, DomainInclusion (ProdLFunc (ln n)) (fn n)) as incn. { intro n. destruct (resn n). exact d0. } exists (Build_CommonPointFunSeq _ _ f fn (cpx _ _ _ x, cpx _ _ _ y) (d (cpx _ _ _ x, cpx _ _ _ y) (cpxF _ _ _ y)) (fun n => incn n (cpx _ _ _ x, cpx _ _ _ y) (cpxFn _ _ _ y n))); unfold cpx, cpxF, cpxFn. destruct ycv as [y0 [ycv ylt]]. exists y0. split. apply (series_cv_eq (fun n : nat => partialApply (Xproj1 (ProdLFunc (ln n)) (cpx (X (ElemFunc I)) (IntegralFst (ProdLFunc fl) (LElemProductIntegrableAE fl)) (fun n0 : nat => IntegralFst (ProdLFunc (ln n0)) (LElemProductIntegrableAE (ln n0))) x)) (cpx _ _ _ y) (cpxFn _ _ _ y n))). 2: exact ycv. intro n. destruct (resn n). apply c0. simpl in ylt; rewrite c in ylt; exact ylt. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile