fact: Definition Cap_slow_modulus (f:Complete (X --> Y)) (e:Qpos) : QposInf := ((Qpos2QposInf (1#2)) *(mu (approximate f (Qpos2QposInf ((1#3)*e))%Qpos) ((1#3)*e)%Qpos))%QposInf.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax