fact: Record IntegrationSpace := { ElemFunc : FunctionRieszSpace; I : forall f : PartialFunction (X ElemFunc), (L ElemFunc) f -> CRcarrier (RealT ElemFunc); Iadditive : forall (f g : PartialFunction (X ElemFunc)) (fL : L ElemFunc f) (gL : L ElemFunc g), I (Xplus f g) (LplusStable ElemFunc f g fL gL) == I f fL + I g gL; Ihomogeneous : forall (a : CRcarrier (RealT ElemFunc)) (f : PartialFunction (X ElemFunc)) (fL : L ElemFunc f), I (Xscale a f) (LscaleStable ElemFunc a f fL) == a * (I f fL); Ione : PartialFunction (X ElemFunc); IoneL : L ElemFunc Ione; IoneInt : I Ione IoneL == 1; Icontinuous : ElemIntegralContinuous I; Ilimit : forall (f : PartialFunction (X ElemFunc)) (fL : L ElemFunc f), prod (CR_cv _ (fun n => I (XminConst f (INR n)) (LminIntStable n f fL)) (I f fL)) (CR_cv _ (fun n => I (XminConst (Xabs f) (CR_of_Q _ (1# Pos.of_nat (S n)))) (LminConstStable (CR_of_Q _ (1# Pos.of_nat (S n))) (Xabs f) (invSuccRealPositive n) (LabsStable ElemFunc f fL))) 0) }.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions