proposition: Lemma f0eps_lim_correct_sing alpha beta epsilon sing (Halpha : (-1 < alpha)%Z) (Heps : 0 < epsilon) : is_RInt_gen ((fun x => powerRZ (x - sing) alpha * (pow (ln (x - sing)) beta))) (at_right sing) (at_point (sing + 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 - sing)))). exists (pos_div_2 eps) => y /= Hy1 Hy2. move/ball_to_lra in Hy1. have {1}-> : y = sing + / / (y - sing) by rewrite Rinv_involutive; lra. rewrite -is_RInt_gen_at_point. apply f0eps_correct_sing; rewrite ?Rinv_involutive; try lra. apply: Rinv_0_lt_compat; lra. exact Halpha. exact: f0eps_lim_is_lim_sing. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval