proposition: Lemma continuous_f_neg x beta (H0x : 0 < x) (Hx1 : x <> 1): continuous (fun x0 : R => / (x0 * ln x0 ^ beta)) x.
proof: Proof. have Hlnn0 x1 beta1 : 0 < x1 -> 1 <> x1 -> ln x1 ^ beta1 <> 0. by move => H0x1 Hx10; apply: pow_nonzero; case: (Rlt_dec 1 x1) => H; move: (ln_increasing 1 x1); move: (ln_increasing x1 1); rewrite ln_1; lra. apply: continuous_comp. apply: continuous_mult; first exact: continuous_id. apply: (continuous_comp ln (fun x => pow x beta)). 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. 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