fact: Fixpoint f (alpha : Z) (beta : nat) (A B : R) {struct beta} := match beta with | 0 => (powerRZ B (alpha+1)- powerRZ A (alpha+1)) / (IZR (alpha + 1)) | S m => (powerRZ B (alpha+1) * (pow (ln B) (beta)) - powerRZ A (alpha+1) * (pow (ln A) beta)) / (IZR (alpha + 1)) - (INR beta) / (IZR (alpha+1)) * f alpha m A B end.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval