proposition: Lemma one_step_by_parts alpha beta (A : R) (B : R) (H : 0 < A <= B) (Halpha: alpha <> (-1)%Z) : forall I, Bertrand alpha beta A B I -> Bertrand alpha (S beta) A B ((powerRZ B (alpha+1) * (pow (ln B) (S beta)) - powerRZ A (alpha+1) * (pow (ln A) (S beta))) / (IZR (alpha + 1)) - (INR (S beta)) / (IZR (alpha+1)) * I).
proof: Proof. have Salpha_neq_0 : IZR (alpha + 1) <> 0. by apply: not_0_IZR; lia. move => I HABI. rewrite/Bertrand. pose f := (fun x => Rdiv (powerRZ x (alpha+1)) (IZR(alpha+1))). pose f' := (fun x => powerRZ x alpha). pose g := (fun x => pow (ln x) (beta.+1)). pose g' := (fun x => (1 / x) * (INR (beta.+1) * pow (ln x) beta)). set f'g := (fun x : R => scal (f' x) (g x)). pose fg' := (fun t => scal (f t) (g' t)). pose f'gplusfg' := (fun t : R => plus (f'g t) (fg' t)). apply (is_RInt_ext (fun x => minus (f'gplusfg' x) (fg' x))) => [x HX|]. rewrite /f'gplusfg' /fg' /f /g /f'g. by rewrite /minus -plus_assoc plus_opp_r plus_zero_r /scal. apply: is_RInt_minus. - apply: (is_RInt_ext (fun t : R => plus (scal (f' t) (g t)) (scal (f t) (g' t)))) =>[x Hx|]. by []. have -> : ((powerRZ B (alpha + 1) * ln B ^ beta.+1 - powerRZ A (alpha + 1) * ln A ^ beta.+1) / IZR (alpha + 1)) = (minus (scal (f B) (g B)) (scal (f A) (g A))). rewrite /f /g /minus /opp /plus /scal /mult /= /mult /= . by field. apply: (is_RInt_scal_derive f g f' g' A B) => x Hx. have xgt0 : x > 0 by case: Hx; rewrite Rmin_left; lra. + rewrite /f /f'. apply: (is_derive_ext (fun x0 => scal (powerRZ x0 (alpha + 1)) (1 / IZR (alpha + 1)))) => [t|]. by rewrite /scal /= /mult /=;field. have -> : powerRZ x alpha = scal (IZR (alpha+1) * (powerRZ x alpha)) (1 / IZR (alpha + 1)). by rewrite /scal /mult /= /mult /=; field. apply: is_derive_scal_l. apply: (is_derive_powerRZS alpha x). by lra. + rewrite /g /g'. have -> : (1 / x * (INR beta.+1 * ln x ^ beta)) = (INR beta.+1 * ( / x) * ln x ^ beta.+1.-1). rewrite -pred_Sn; field. by case: Hx; rewrite Rmin_left; lra. apply: (is_derive_pow). apply: is_derive_ln. by case: Hx; rewrite Rmin_left; lra. + have Hxneq0 : x <> 0 by rewrite Rmin_left in Hx; lra. apply: ex_derive_continuous. apply: ex_derive_powerRZ; right => // . + have Hxgt0 : x > 0 by rewrite Rmin_left in Hx; lra. have Hxneq0 : x <> 0 by lra. apply: continuous_mult. apply: continuous_Rdiv_1_x => // . apply: continuous_mult; first exact: continuous_const. apply: ex_derive_continuous. apply: ex_derive_is_derive. apply: is_derive_pow. by apply: is_derive_ln. move: HABI; rewrite /Bertrand. suff Hx : forall x, Rmin A B < x < Rmax A B -> (fun x => scal (INR beta.+1 / IZR (alpha + 1)) (powerRZ x alpha * ln x ^ beta)) x = fg' x => [HABI|t HAtB]. apply: is_RInt_ext. exact: Hx. apply: is_RInt_scal => // . have Hxgt0 : t > 0 by rewrite Rmin_left in HAtB; lra. have Hxneq0 : t <> 0 by lra. rewrite /fg' /f /g'. rewrite powerRZ_add // . rewrite /scal /= /mult /=. field; 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