proposition: Lemma f_neg_correct_RInt_0_1 a b beta (Hab1 : 0 < a <= b) (Hb1 : b < 1) (Hbeta : beta <> 0%N) : is_RInt (fun x => / (x * (ln x)^beta.+1)) a b (f_neg b beta - f_neg a beta).
proof: Proof. have Hbetn0 : INR beta <> 0 by apply: not_0_INR; case: beta Hbeta. have Hlnn0 x beta1 : 0 < x < 1 -> ln x ^ beta1 <> 0. by move => Hx0; apply: pow_nonzero; move: (ln_increasing x 1); rewrite ln_1;lra. have Hder : forall x, 0 < x < 1 -> is_derive (fun x => f_neg x beta) x (/ (x * (ln x)^beta.+1)). move => x Hax. apply is_derive_f_neg. now destruct beta. apply Hax. now apply Rlt_not_eq. apply: (is_RInt_derive (fun x => f_neg x beta) _). by move => x Hx; apply: Hder; rewrite Rmin_left ?Rmax_right in Hx; try lra. move => x. (rewrite Rmin_left ?Rmax_right; try (by lra)). move => Hx. apply: continuous_comp. apply: continuous_mult; first exact: continuous_id. apply: (continuous_comp ln (fun x => pow x beta.+1)). by apply: continuous_ln; lra. by apply: ex_derive_continuous; apply: ex_derive_pow; exact: ex_derive_id. apply: continuous_Rinv. apply: Rmult_integral_contrapositive; split; try lra. by apply: Hlnn0; lra. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval