fact: Fixpoint interp_side_equa_in_R s (rho : list (sigT infinite_cv_radius)) : option (R -> R) := match s with | cst r => Return (fun _ => r) | scal r e => Bind (interp_side_equa_in_R e rho) (fun f => Return ((fun _ => r) * f)%F) | y i k a => Bind (nth_error rho i) (fun f => Return (fun x => nth_derive (sum (projT1 f) (projT2 f)) (D_infty_Rpser (projT1 f) (projT2 f) k) (a * x)%R)) | opp e => Bind (interp_side_equa_in_R e rho) (fun f => Return (- f)%F) | min e1 e2 => Bind (interp_side_equa_in_R e1 rho) (fun f => Bind (interp_side_equa_in_R e2 rho) (fun g => Return (f - g)%F)) | plus e1 e2 => Bind (interp_side_equa_in_R e1 rho) (fun f => Bind (interp_side_equa_in_R e2 rho) (fun g => Return (f + g)%F)) | mult e1 e2 => Bind (interp_side_equa_in_R e1 rho) (fun f => Bind (interp_side_equa_in_R e2 rho) (fun g => Return (f * g)%F)) end.
imports: Reals Rpser_def Rpser_sums Rpser_usual Rpser_derivative Rfunction_classes Nth_derivative_def Rfunction_def Functions Rsequence_def List Option