proposition: Lemma f_neg_correct_RInt_gen_0_a a beta (Ha : 0 < a < 1) (Hbeta : beta <> 0%N) : is_RInt_gen (fun x => / (x * (ln x)^beta.+1)) (at_right 0) (at_point a) (f_neg a beta).
proof: Proof. apply prodi_to_single_r. have apos : 0 < a by lra. set ap := mkposreal a apos. apply: (filterlimi_lim_ext_loc). exists ap => x Hx1 Hx2. apply f_neg_correct_RInt_0_1 => // ;move/ball_to_lra: Hx1 => /=; lra. rewrite -{2}[f_neg _ _ ]Rminus_0_r. apply: (filterlim_comp _ _ _ (fun x => f_neg x beta) (fun x => f_neg a beta - x) (at_right 0) _ _) ;last first. rewrite /Rminus. apply: continuous_plus. exact: filterlim_const. exact: filterlim_opp. rewrite /f_neg. apply: filterlim_comp; last first. rewrite -[0]Ropp_0. exact: (filterlim_opp 0). case HEvenOdd: (odd beta); last first. - rewrite -[locally 0]/(Rbar_locally (Rbar_inv p_infty)). apply (filterlim_comp _ _ _ (fun x => INR beta*ln x ^ beta) Rinv _ (Rbar_locally p_infty)). have -> : p_infty = Rbar_mult (INR beta) p_infty. by rewrite Rbar_mult_p_l // ; apply: lt_0_INR; apply/ltP; case: beta Hbeta HEvenOdd. suff: filterlim (fun x => (ln x)^beta) (at_right 0) (Rbar_locally p_infty). move => Hln. apply: filterlim_comp; last first. exact: filterlim_Rbar_mult_l. exact: Hln. apply: (filterlim_comp _ _ _ _ (fun x => x ^beta)) => //; try apply: is_lim_ln_0. case: beta Hbeta HEvenOdd => [|beta] Hbeta HevenOdd // . by apply: filterlim_pow_m_even; by rewrite HevenOdd. exact: is_lim_RInv_p_infty. - rewrite -[locally 0]/(Rbar_locally (Rbar_inv m_infty)). apply (filterlim_comp _ _ _ (fun x => INR beta*ln x ^ beta) Rinv _ (Rbar_locally m_infty)). have -> : m_infty = Rbar_mult (INR beta) m_infty. by rewrite Rbar_mult_m_l // ; apply: lt_0_INR; apply/ltP; case: beta Hbeta HEvenOdd. suff: filterlim (fun x => (ln x)^beta) (at_right 0) (Rbar_locally m_infty). move => Hln. apply: filterlim_comp; first exact: Hln. exact: filterlim_Rbar_mult_l. apply: (filterlim_comp _ _ _ _ (fun x => x ^ beta)); try apply: is_lim_ln_0. case: beta Hbeta HEvenOdd => [|beta] Hbeta HevenOdd // . by apply: filterlim_pow_m_odd; by rewrite HevenOdd. by apply: is_lim_RInv_m_infty. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval