proposition: Lemma subst_lemma alpha beta epsilon (eta : R) (Heps : 0 < epsilon) (Heta : 0 < eta <= epsilon) (Halpha : -1 < IZR alpha) : RInt_gen (fun x => powerRZ x alpha * pow (ln x) beta) (at_point eta) (at_point epsilon) = - RInt (fun x => - (pow (-1) beta) * powerRZ x (- 2 - alpha) * (pow (ln x) beta)) (1 / epsilon) (1 / eta).
proof: Proof. have Hint : ex_RInt (fun x : R => powerRZ x alpha * ln x ^ beta) eta epsilon. eexists. apply: f_correct => // . suff: (-1 < alpha)%Z by lia. apply: lt_IZR => // . have -> : RInt_gen (fun x : R => powerRZ x alpha * ln x ^ beta) (at_point eta) (at_point epsilon) = RInt (fun x : R => powerRZ x alpha * ln x ^ beta) eta epsilon. apply is_RInt_gen_unique; rewrite is_RInt_gen_at_point. exact: RInt_correct => // . pose g := fun x => Rinv x. pose dg := fun x => - 1 / x^2. have {1}-> : 1 / eta = (g eta). by rewrite /g; field; lra. have {1}-> : 1 / epsilon = (g epsilon). by rewrite /g; field; lra. rewrite -(RInt_comp _ _ dg). rewrite -opp_RInt_swap ; first congr (opp _) ; last by apply: ex_RInt_swap. symmetry; apply: RInt_ext. move => x Hx. rewrite Rmin_right in Hx; try lra. rewrite Rmax_left in Hx; try lra. have Hxneg0 : x <> 0 by lra. have Hinv : / x <> 0. by apply: Rinv_neq_0_compat. have -> : scal (dg x)(- (-1) ^ beta * powerRZ (g x) (-2 - alpha) * ln (g x) ^ beta) = (dg x) * (- (-1) ^ beta * powerRZ (g x) (-2 - alpha) * ln (g x) ^ beta) by []. rewrite /dg /g. rewrite powerRZ_add ?ln_Rinv; try lra. rewrite -> (powerRZ_neg _ 2), powerRZ_neg, Rinv_involutive by easy. rewrite [(- ln x) ^beta] pow_negx. replace (powerRZ x alpha * ln x ^ beta) with ((-1)^beta * (-1)^beta * (powerRZ x alpha * ln x ^ beta)). rewrite /(powerRZ x 2) /=. now field. rewrite -Rpow_mult_distr. have -> : -1 * -1 = 1 by ring. by rewrite pow1 Rmult_1_l. move => x Hx. rewrite Rmin_right in Hx; try lra. rewrite Rmax_left in Hx; try lra. apply: continuous_mult. apply: continuous_mult. exact: continuous_const. apply: ex_derive_continuous. apply: ex_derive_powerRZ. by rewrite /g; right; apply: Rinv_neq_0_compat; lra. rewrite /g. apply: continuous_ext. move => x0. by rewrite pow_powerRZ. apply: (continuous_comp ln (fun x => powerRZ x (Z.of_nat beta))). by apply: continuous_ln; apply: Rinv_0_lt_compat; lra. apply: ex_derive_continuous. by apply: ex_derive_powerRZ; left; apply: Zle_0_nat. move => x Hx. rewrite Rmin_right in Hx; try lra. rewrite Rmax_left in Hx; try lra. split. rewrite /g /dg. apply: (is_derive_inv (fun x => x) x 1); last by lra. exact: is_derive_id. rewrite /dg. apply: continuous_mult; first exact: continuous_const. apply: continuous_Rinv_comp. apply: (continuous_ext (fun t => t * t)) => [t|]. by rewrite pow_powerRZ /=; ring. by apply: continuous_mult; exact: continuous_id. by apply: pow_nonzero; 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