proposition: Lemma contains_RInt_gen_infty_bertrand : forall prec deg limit check vars hyps alpha beta pf pu cf cu, R.eval_hyps_bnd (R.merge_hyps prec hyps) vars -> (alpha < -1)%Z -> no_floor_prog pf = true -> let hyps := R.merge_hyps prec hyps in let (mid, Fi) := eval_RInt_gen_infty_init prec deg hyps (bertrand_infty_interval alpha beta) pf (bertrand_prog alpha beta pf) pu cf cf cu in contains (I.convert (IR.bisect prec limit mid Fi check)) (Xreal (RInt_gen (fun t => Prog.eval_real' pf (t :: vars) cf * (powerRZ t alpha * pow (ln t) beta)) (at_point (Prog.eval_real' pu vars cu)) (Rbar_locally p_infty))).
proof: Proof. intros prec deg limit check vars hyps alpha beta pf pu cf cu H' Halpha Hp. apply contains_RInt_gen_infty ; cycle 2. - apply bertrand_prog_correct. - unfold bertrand_prog, no_floor_prog in Hp |- *. rewrite <- fold_left_rev_right. rewrite rev_app_distr. simpl. rewrite fold_left_rev_right. now rewrite Hp. - exact Hp. - exact H'. - intros fi ui f u Hu Hc Hf Hb. unfold bertrand_infty_interval, c1. destruct F'.le' eqn:Hul ; cycle 1. now rewrite I.nai_correct. intros _. assert (Hu': (1 <= u)%R). apply F'.le'_correct in Hul. rewrite F.fromZ_correct in Hul by easy. rewrite I.lower_correct in Hul by now exists u. destruct (I.convert ui) as [|[|ul] ur] ; try easy. now apply Rle_trans with (2 := proj1 Hu). eapply IU.integral_interval_mul_infty with (1 := Hu) (2 := Hf) (3 := Hb) (4 := Hc). + intros x Hx. assert (Hx': (0 < x)%R). apply Rlt_le_trans with (1 := Rlt_0_1). now apply Rle_trans with u. apply @continuous_mult. apply @ex_derive_continuous. apply ex_derive_powerRZ. right. now apply Rgt_not_eq. apply @ex_derive_continuous. apply ex_derive_pow. eexists. now apply is_derive_ln. + intros x Hx. apply Stdlib.Rmult_le_pos_pos. apply powerRZ_le. lra. apply pow_le. rewrite <- ln_1. apply ln_le. apply Rlt_0_1. now apply Rle_trans with u. + apply f_lim_correct with (2 := Halpha). now apply Rlt_le_trans with (1 := Rlt_0_1). + apply BI.f_int_fast_correct. exact Hu. now apply Rlt_le_trans with (1 := Rlt_0_1). now apply Zlt_not_eq. Qed.
imports: Coq(Reals List ZArith Psatz) Flocq(Zaux) Coquelicot(Coquelicot) Stdlib Coquelicot Xreal Basic Sig Interval Integral Eval Bertrand Tree Prog Reify Refine Interval_helper