fact: Definition IabsOpContract {IS : IntegrationSpace} (fn : nat -> PartialFunction (X (ElemFunc IS))) (fnL : forall n:nat, L (ElemFunc IS) (fn n)) (op : CRcarrier (RealT (ElemFunc IS)) -> CRcarrier (RealT (ElemFunc IS))) (opEq : forall x y : CRcarrier (RealT (ElemFunc IS)), x == y -> op x == op y) (opL : forall f : PartialFunction (X (ElemFunc IS)), L (ElemFunc IS) f -> L (ElemFunc IS) (Xop (X (ElemFunc IS)) f op opEq)) (contract : forall x y : CRcarrier (RealT (ElemFunc IS)), CRabs _ (op x - op y) <= CRabs _ (x - y)) (zeroFix : op 0 == 0) (sumIAbsFn : CRcarrier (RealT (ElemFunc IS))) : series_cv (fun k : nat => Iabs (fn k) (fnL k)) sumIAbsFn -> { l : CRcarrier (RealT (ElemFunc IS)) & series_cv (fun k => Iabs (telescopicOp _ fn op opEq k) (telescopicOpL fn fnL op opEq opL k)) l }.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase