proposition: Lemma IntegralHomogeneousHalf : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (a : CRcarrier (RealT (ElemFunc IS))), IntegralSeries (IntegralRepresentationScaleHalf f a fInt) == (Integral fInt) * a.
proof: Proof. intros. destruct fInt. apply (series_cv_unique (fun n0 : nat => (I IS (IntFn x n0) (IntFnL x n0)) * a)). - apply (series_cv_eq (fun n:nat => I IS (Xscale a (IntFn x n)) (LscaleStable _ a _ (IntFnL x n)))). intro n. rewrite Ihomogeneous. apply CRmult_comm. apply (IntegralCv (IntegralRepresentationScaleHalf f a (existT (fun fInt : IntegralRepresentation => PartialRestriction (XinfiniteSumAbs (IntFn fInt)) f) x p))). - apply series_cv_scale. simpl. apply (IntegralCv x). Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase