proposition: Lemma contains_RInt_gen_infty_invxln : forall prec deg limit check vars hyps beta pf pu cf cu, R.eval_hyps_bnd (R.merge_hyps prec hyps) vars -> no_floor_prog pf = true -> let hyps := R.merge_hyps prec hyps in let (mid, Fi) := eval_RInt_gen_infty_init prec deg hyps (invxln_interval beta) pf (invxln_prog 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 / (t * pow (ln t) (S (S beta)))) (at_point (Prog.eval_real' pu vars cu)) (Rbar_locally p_infty))).
proof: Proof. intros prec deg limit check vars hyps beta pf pu cf cu H' Hp. apply contains_RInt_gen_infty ; cycle 2. - apply invxln_prog_correct. - unfold invxln_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 invxln_interval, c1. destruct F'.lt' eqn:Hul ; cycle 1. now rewrite I.nai_correct. intros _. assert (Hu': (1 < u)%R). apply F'.lt'_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 Rlt_le_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': (1 < x)%R). now apply Rlt_le_trans with u. apply (continuous_f_neg x (S (S beta))). now apply Rlt_trans with (1 := Rlt_0_1). now apply Rgt_not_eq. + intros x Hx. apply Rlt_le, Rinv_0_lt_compat, Rmult_lt_0_compat. lra. apply (pow_lt (ln x) (S (S beta))). rewrite <- ln_1. apply ln_increasing. apply Rlt_0_1. now apply Rlt_le_trans with u. + now apply (f_neg_correct_RInt_gen_a_infty u (S beta)). + now apply BI.f_neg_int_correct. 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