proposition: Lemma f0eps_lim_correct alpha beta epsilon (Halpha : (-1 < alpha)%Z) (Heps : 0 < epsilon) : is_RInt_gen ((fun x => powerRZ x alpha * (pow (ln x) beta))) (at_right 0) (at_point epsilon) (f0eps_lim alpha beta epsilon).
proof: Proof. set eps := mkposreal epsilon Heps. apply prodi_to_single_r. apply: (filterlimi_lim_ext_loc (fun x => f0eps alpha beta epsilon (/ x))). exists (pos_div_2 eps) => y /= Hy1 Hy2. move/ball_to_lra in Hy1. have {1}-> : y = / / y by rewrite Rinv_involutive; lra. rewrite -is_RInt_gen_at_point. apply (f0eps_correct); rewrite ?Rinv_involutive; try lra. exact: Rinv_0_lt_compat. exact Halpha. exact: f0eps_lim_is_lim. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval