fact: Definition CompleteRepresentation (IS : IntegrationSpace) (fn : nat -> PartialFunction (X (ElemFunc IS))) (fnInt : forall n:nat, IntegrableFunction (fn n)) : { intRepresN : nat -> IntegralRepresentation & forall n:nat, prod (PartialRestriction (XinfiniteSumAbs (IntFn (intRepresN n))) (fn n)) (IntAbsSum (intRepresN n) <= Integral (IntegrableAbs (fnInt n)) + CRpow (CR_of_Q _ (1#2)) n) }.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions