proposition: Lemma contains_RInt_gen_zero_bertrand : forall prec deg limit check vars hyps alpha beta pf pv cf cv, R.eval_hyps_bnd (R.merge_hyps prec hyps) vars -> (-1 < alpha)%Z -> no_floor_prog pf = true -> let hyps := R.merge_hyps prec hyps in let (mid, Fi) := eval_RInt_gen_zero_init prec deg hyps (bertrand_zero_interval alpha beta) pf (bertrand_prog alpha beta pf) pv cf cf cv 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_right 0) (at_point (Prog.eval_real' pv vars cv)))).
proof: Proof. intros prec deg limit check vars hyps alpha beta pf pv cf cv H' Halpha Hp. apply contains_RInt_gen_zero ; 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 vi f v Hv Hc Hf Hb. unfold bertrand_zero_interval, c1. destruct F'.lt' eqn:Hvl ; cycle 1. cbv [andb]. now rewrite I.nai_correct. destruct F'.le' eqn:Hvu ; cycle 1. cbv [andb]. now rewrite I.nai_correct. intros _. assert (Hv': (0 < v)%R). apply F'.lt'_correct in Hvl. rewrite F.zero_correct in Hvl. rewrite I.lower_correct in Hvl by now exists v. destruct (I.convert vi) as [|[|vl] vr] ; try easy. now apply Rlt_le_trans with (2 := proj1 Hv). eapply IU.integral_interval_mul_zero with (1 := Hv') (2 := Hv) (3 := Hf) (4 := Hb) (5 := Hc). + intros x Hx. 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. + destruct (Zeven_odd_dec (Z.of_nat beta)) as [Hbeta|Hbeta] ; [left|right] ; intros x Hx. apply Rmult_le_pos_pos. now apply powerRZ_le. apply IT.TM.TMI.ZEven_pow_le. now apply Zeven_equiv. apply Rmult_le_pos_neg. now apply powerRZ_le. apply IT.TM.TMI.ZOdd_pow_le. now apply Zodd_equiv. rewrite <- ln_1. apply ln_le. apply Hx. apply Rle_trans with (1 := proj2 Hx). apply F'.le'_correct in Hvu. rewrite F.fromZ_correct in Hvu by easy. rewrite I.upper_correct in Hvu by now exists v. destruct (I.convert vi) as [|vr [|vu]] ; try easy. now apply Rle_trans with (1 := proj2 Hv). + now apply f0eps_lim_correct with (1 := Halpha). + apply BI.f0eps_correct ; try easy. now apply Zgt_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