proposition: Lemma f_neg_correct_RInt_gen_a_infty a beta (Ha : 1 < a) (Hbeta : beta <> 0%N) : is_RInt_gen (fun x => / (x * (ln x)^beta.+1)) (at_point a) (Rbar_locally p_infty) (- f_neg a beta).
proof: Proof. apply prodi_to_single_l. apply: (filterlimi_lim_ext_loc). exists a => x Hx. by apply f_neg_correct_RInt_a_infty => // ; lra. rewrite -Rminus_0_l. apply: (filterlim_comp _ _ _ (fun x => f_neg x beta) (fun x => x - f_neg a beta) _ _);last first. rewrite /Rminus. apply: continuous_plus 0%R _ _. exact: filterlim_id. exact: filterlim_const. rewrite /f_neg. apply: filterlim_comp. apply: (is_lim_inv (fun x => INR beta*ln x ^ beta) (p_infty) (p_infty)) => // . have {2} -> : p_infty = Rbar_mult (INR beta) p_infty. by rewrite Rbar_mult_p_l // ; apply: lt_0_INR; apply/ltP; case: beta Hbeta. apply: is_lim_mult; first exact: is_lim_const. apply: (filterlim_comp _ _ _ _ (fun x => x ^beta)) => // ; try apply: is_lim_ln_p. by case :beta Hbeta => [| beta] // Hbeta; apply: is_lim_pow_infty. by apply: not_0_INR; case: beta Hbeta. rewrite -[0]Ropp_0. exact: (filterlim_opp 0). Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval