proposition: Lemma f0eps_lim_is_lim alpha beta epsilon (Halpha : (-1 < alpha)%Z) (Heps : 0 < epsilon) : filterlim (fun x : R => f0eps alpha beta epsilon (/ x)) (at_right 0) (locally (f0eps_lim alpha beta epsilon)).
proof: Proof. apply: filterlim_comp. exact: filterlim_Rinv_0_right. rewrite /f0eps /f0eps_lim. have H x : ((-1) ^ beta * x) = mult ((-1) ^ beta) x by []. rewrite H. apply: filterlim_ext. by move => x; first rewrite H. rewrite -[locally _]/(Rbar_locally (Rbar_mult (Finite _) (Finite _))). rewrite -[filterlim _ _ _]/(is_lim _ p_infty _). apply: is_lim_mult => // . + exact: is_lim_const. + apply: f_lim_is_lim; first exact: Rinv_0_lt_compat. by lia. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval