proposition: Lemma ProdLFuncApplyUnique : forall {I J : IntegrationSpace} (hn : list (@ProdIntegrable I J)) (x : X (ElemFunc I)) (y : X (ElemFunc J)) (xyS : Domain (ProdLFunc hn) (x,y)) (n : nat) (ltnh : lt n (length hn)), (forall (k:nat) (ltkh : lt k (length hn)), k <> n -> partialApply _ _ (DomainProdLFuncInc hn x y xyS k ltkh) == 0) -> partialApply _ _ xyS == partialApply _ _ (DomainProdLFuncInc hn x y xyS n ltnh).
proof: Proof. induction hn. - intros. exfalso; inversion ltnh. - intros. destruct xyS. specialize (IHhn x y d0). transitivity (partialApply _ _ d + partialApply _ _ d0). reflexivity. destruct n. + simpl (nth 0 (a :: hn) (ProdIntegrableZero I J)). rewrite <- (CRplus_0_r (partialApply (ProdIntegrableFunc a) (x, y) (DomainProdLFuncInc (a :: hn) x y (d, d0) 0 ltnh))). apply CRplus_morph. apply DomainProp. apply ProdLFuncApplyZero. intros. assert (S n < length (a :: hn))%nat. { apply le_n_S, ltnh0. } rewrite <- (H (S n) H0). apply DomainProp. discriminate. + assert (n < length hn)%nat. { apply le_S_n. exact ltnh. } specialize (IHhn n H0). rewrite IHhn. clear IHhn. rewrite <- (CRplus_0_l (partialApply (ProdIntegrableFunc (nth (S n) (a :: hn) (ProdIntegrableZero I J))) (x, y) (DomainProdLFuncInc (a :: hn) x y (d, d0) (S n) ltnh))). apply CRplus_morph. 2: apply DomainProp. assert (0 < S (length hn))%nat. apply le_n_S, Nat.le_0_l. specialize (H O H1). unfold nth in H. rewrite <- H. apply DomainProp. discriminate. clear IHhn. intros. assert (S k < length (a :: hn))%nat. { apply le_n_S, ltkh. } specialize (H (S k) H2). simpl (nth (S k) (a :: hn) (ProdIntegrableZero I J)) in H. rewrite <- H. apply DomainProp. intro abs. inversion abs. contradiction. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile