proposition: Lemma x_alpha_beta alpha beta (Halpha : (alpha < -1)%Z) : is_lim (fun x => powerRZ x (alpha + 1)%Z * (pow (ln x) beta.+1)) p_infty (0%R).
proof: Proof. have Halpah1 : IZR (alpha + 1) < 0. by apply: (IZR_lt _ 0); lia. have Hbeta1 : INR beta.+1 > 0. apply: lt_0_INR. exact: Nat.lt_0_succ. have foo : 0 < IZR (- (alpha + 1)) / INR beta.+1. rewrite opp_IZR. by apply: RIneq.Rdiv_lt_0_compat => // ; lra. set X := fun x => Rpower x ((IZR (Z.opp (alpha + 1))) / INR beta.+1). have Htransform: forall x, x > 0 -> powerRZ x (alpha + 1) * ln x ^ beta.+1 = pow (-((INR beta.+1) / IZR (alpha + 1)) * (ln (X x) * / (X x))) beta.+1. move => x Hx. have HXgt0 : X x > 0. by apply: Rpower_pos => // ; lra. have -> : -((INR beta.+1) / IZR (alpha + 1)) * (ln (X x) / (X x)) = (-((INR beta.+1) / IZR (alpha + 1)) * ln (X x)) / (X x). field. by split; lra. rewrite -ln_Rpower ?Rpow_mult_distr => // . + have -> : Rpower (X x) (-(INR beta.+1 / IZR (alpha + 1))) = x. rewrite Rpower_mult. rewrite opp_IZR. have -> : (- IZR ((alpha + 1)) / INR beta.+1 * -(INR beta.+1 / IZR (alpha + 1))) = 1 by field; lra. exact: Rpower_1. + rewrite Rmult_comm. congr (_ * _). have Hpow_pos : Rpower x (IZR (- (alpha + 1)) / INR beta.+1) > 0. by apply: Rpower_pos => // ; lra. rewrite -Rinv_pow /X; try lra. rewrite -Rpower_pow ?Rpower_mult -?Rpower_Ropp // . have -> : (- (IZR (- (alpha + 1)) / INR beta.+1 * INR beta.+1)) = IZR (alpha + 1)%Z. by rewrite opp_IZR; field; lra. by rewrite powerRZ_Rpower. apply: Ropp_0_ge_le_contravar. apply: Rle_ge. rewrite /Rdiv. apply: Rmult_le_pos_neg => // ; try lra. by apply: Rlt_le; apply: Rinv_lt_0_compat. apply: (is_lim_ext_loc (fun x => (- (INR beta.+1 / IZR (alpha + 1)) * (ln (X x) * / X x)) ^ beta.+1) ). by exists 0; move => x Hx ; rewrite Htransform // . apply: is_lim_pow_0. have -> : 0 = Rbar_mult (- (INR beta.+1 / IZR (alpha + 1))) 0. by rewrite /Rbar_mult /Rbar_mult' Rmult_0_r. apply (is_lim_scal_l (fun (x : R) => (ln (X x) * / X x)) (- (INR beta.+1 / IZR (alpha + 1))) p_infty 0). apply: (is_lim_comp (fun x => ln x / x) X p_infty 0 p_infty). + exact: is_lim_div_ln_p. + apply: is_lim_Rpower => // . + exists 0 => x Hx // . Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval