proposition: Lemma applyProdLFuncBound : forall { I J : IntegrationSpace } (l : list (@ProdIntegrable I J)) x (xD : Domain (ProdLFunc l) x), partialApply _ x xD <= fold_right (CRplus (RealT (ElemFunc I))) 0 (map (fun a => CRabs _ (prodint_factor a)) l).
proof: Proof. induction l. - intros. apply CRle_refl. - intros. simpl. destruct xD. apply CRplus_le_compat. destruct d. simpl. destruct d. destruct d1. do 2 rewrite CRmult_1_r. apply CRle_abs. rewrite CRmult_0_r. apply CRabs_pos. rewrite CRmult_0_r, CRmult_0_l. apply CRabs_pos. apply IHl. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile