proposition: Lemma f0eps_correct alpha beta epsilon (B : R) (Heps : 0 < / B <= epsilon) (HB : 0 < B) (Halpha : (-1 < alpha)%Z) : is_RInt_gen ((fun x => powerRZ x alpha * (pow (ln x) beta))) (at_point (/ B)) (at_point epsilon) (f0eps alpha beta epsilon B).
proof: Proof. have Hint : ex_RInt (fun x : R => powerRZ x alpha * ln x ^ beta) (/ B) epsilon. eexists. apply: f_correct => // . by lia. have HinvepsinvB : 0 < / epsilon <= B. split. by apply: Rinv_0_lt_compat; by lra. by rewrite -[B]Rinv_involutive; try lra; apply: Rinv_le; lra. rewrite is_RInt_gen_at_point. suff: f0eps alpha beta epsilon B = RInt (fun x : R => powerRZ x alpha * ln x ^ beta) (/B) epsilon. by move ->; apply: RInt_correct. rewrite -RInt_gen_at_point; last first. + eexists. apply: f_correct; try lra; try lia. + rewrite subst_lemma ; try lra. 2: now apply IZR_lt. symmetry. rewrite /f0eps. rewrite f_correct_RInt; try lra; try lia. rewrite (RInt_ext _ (fun x : R => scal (- (-1) ^ beta) (powerRZ x (-2 - alpha) * ln x ^ beta))); last first. by move => x Hx; rewrite /scal [in RHS]/= /mult /=; rewrite Rmult_assoc. set e1 := (-2 - alpha)%Z; rewrite RInt_scal /scal /= /mult /= . ring_simplify; congr(_ * RInt _ _ _) => // ; field; lra. rewrite /e1. by eexists; apply: f_correct; first (split; field_simplify; lra); lia. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval