proposition: Lemma IElemProductAdditive : forall { I J : IntegrationSpace } (f g : PartialFunction (prod (X (ElemFunc I)) (X (ElemFunc J)))) (fL : L (ProductFunctionRieszSpace I J) f) (gL : L (ProductFunctionRieszSpace I J) g), IElemProduct (Xplus f g) (LplusStable (ProductFunctionRieszSpace I J) f g fL gL) == IElemProduct f fL + IElemProduct g gL.
proof: Proof. intros. simpl; unfold IElemProduct; destruct fL as [fl fL]; destruct gL as [gl gL]. clear gL g fL f. induction fl. - simpl (fold_right (CRplus (RealT (ElemFunc I))) 0 (map (fun pi : ProdIntegrable => prodint_factor pi * MeasureSet (prodint_fint pi) * MeasureSet (prodint_gint pi)) nil)). rewrite CRplus_0_l. reflexivity. - simpl. rewrite IHfl. rewrite CRplus_assoc. reflexivity. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile