proposition: Lemma ApplyProdLFuncDisjointAbs : forall {I J : IntegrationSpace} (l : list (@ProdIntegrable I J)) (x : X (ElemFunc I)) (y : X (ElemFunc J)) (xyL : Domain (ProdLFunc l) (x,y)) (f : CRcarrier (RealT (ElemFunc I)) -> CRcarrier (RealT (ElemFunc I))) (xyA : Domain (ProdLFunc (map (ProdIntegrableMapCoef f) l)) (x,y)), ProdIntegrableSimple l -> f 0 == 0 -> (forall x y : CRcarrier (RealT (ElemFunc I)), x == y -> f x == f y) -> partialApply (ProdLFunc (map (ProdIntegrableMapCoef f) l)) (x,y) xyA == f (partialApply (ProdLFunc l) (x,y) xyL).
proof: Proof. induction l as [|a l]. - intros. rewrite H0. reflexivity. - intros. simpl. destruct xyA, xyL, d. unfold fst in d. destruct d. unfold snd in d3. destruct d3. + simpl. rewrite (H1 (prodint_factor a * (if fst d1 then 1 else 0) * (if snd d1 then 1 else 0) + partialApply (fold_right Xplus (Xconst (X (ElemFunc I) * X (ElemFunc J)) 0) (map ProdIntegrableFunc l)) (x, y) d2) (prodint_factor a)). rewrite (ApplyProdLFuncDisjointHeadMap l a x y f d0 H p p0). rewrite CRplus_0_r. do 2 rewrite CRmult_1_r. reflexivity. destruct d1. simpl. destruct d. destruct d1. 2: contradiction. 2: contradiction. do 2 rewrite CRmult_1_r. rewrite (ApplyProdLFuncDisjointHead l a x y d2 H p p0). rewrite CRplus_0_r. reflexivity. + simpl. rewrite CRmult_0_r, CRplus_0_l. rewrite (H1 (prodint_factor a * (if fst d1 then 1 else 0) * (if snd d1 then 1 else 0) + partialApply (fold_right Xplus (Xconst (X (ElemFunc I) * X (ElemFunc J)) 0) (map ProdIntegrableFunc l)) (x, y) d2) (partialApply (ProdLFunc l) (x, y) d2)). apply IHl. apply H. exact H0. exact H1. destruct d1. unfold snd in d1. simpl. destruct d. destruct d1. contradiction. rewrite CRmult_0_r, CRplus_0_l. reflexivity. rewrite CRmult_0_r, CRmult_0_l, CRplus_0_l. reflexivity. + simpl. rewrite CRmult_0_r, CRmult_0_l, CRplus_0_l. destruct d1. simpl. rewrite (H1 (prodint_factor a * (if d then 1 else 0) * (if d1 then 1 else 0) + partialApply (fold_right Xplus (Xconst (X (ElemFunc I) * X (ElemFunc J)) 0) (map ProdIntegrableFunc l)) (x, y) d2) (partialApply (ProdLFunc l) (x, y) d2)). apply IHl. apply H. exact H0. exact H1. destruct d. destruct d1. contradiction. rewrite CRmult_0_r, CRplus_0_l. reflexivity. rewrite CRmult_0_r, CRmult_0_l, CRplus_0_l. reflexivity. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile