proposition: Lemma contains_RInt_gen_infty : forall prec deg limit check vars hyps mi mp mr pf pu cf cu, R.eval_hyps_bnd (R.merge_hyps prec hyps) vars -> (forall yi ui f u, contains (I.convert ui) (Xreal u) -> (forall t, (u <= t)%R -> continuous f t) -> (forall t, (u <= t)%R -> contains (I.convert yi) (Xreal (f t))) -> I.bounded yi = true -> I.convert (mi prec ui) <> Inan -> exists I : R, is_RInt_gen (fun t : R => f t * mr t) (at_point u) (Rbar_locally p_infty) I /\ contains (I.convert (I.mul prec yi (mi prec ui))) (Xreal I)) -> (forall c t, nth 0 (Prog.eval_real mp (t :: c)) 0 = nth 0 (Prog.eval_real pf (t :: c)) 0 * mr t)%R -> no_floor_prog mp = true -> no_floor_prog pf = true -> let hyps := R.merge_hyps prec hyps in let (mid, Fi) := eval_RInt_gen_infty_init prec deg hyps mi pf mp 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 * mr t) (at_point (Prog.eval_real' pu vars cu)) (Rbar_locally p_infty))).
proof: Proof. intros prec deg limit check vars hyps mi mp mr pf pu cf cu H' Hf Hm1 Hm2 Hp. unfold Prog.eval_real'. simpl. fold (compute_inputs prec hyps cu). assert (Hcu := app_merge_hyps_eval_bnd prec _ _ cu H'). generalize (A.BndValuator.eval_correct' prec pu _ _ Hcu 0). generalize (nth 0 (A.BndValuator.eval prec pu (compute_inputs prec hyps cu)) I.nai). generalize (nth 0 (Prog.eval_real pu (vars ++ map (fun c => eval c nil) cu)) 0%R). clear -H' Hf Hm1 Hm2 Hp. intros u ui Hu. apply IR.bisect_correct with (uf := at_point u) (vf := Rbar_locally p_infty) ; [ typeclasses eauto .. | idtac ]. intros u' v'. fold (compute_inputs prec hyps cf). set (bounds := compute_inputs prec hyps cf). apply (app_merge_hyps_eval_bnd prec _ _ cf) in H'. set (fi := fun b => nth 0 (A.BndValuator.eval prec pf (b :: bounds)) I.nai). set (fmi := fun b => nth 0 (A.BndValuator.eval prec mp (b :: bounds)) I.nai). set (Fi1 := let bounds := map A.TaylorValuator.TM.const bounds in fun ui vi => let xi := I.join ui vi in let gi := A.TaylorValuator.TM.get_tm (prec, deg) xi (nth 0 (A.TaylorValuator.eval prec deg xi mp (A.TaylorValuator.TM.var :: bounds)) A.TaylorValuator.TM.dummy) in IT.taylor_integral_naive_intersection prec fmi gi xi ui vi). set (Fi2 := let bounds := map A.TaylorValuator.TM.const bounds in fun ui => let yi := fi (I.upper_extent ui) in if I.bounded yi then I.mul prec yi (mi prec ui) else I.nai). apply IR.valid_at_mixed with (u := u) (v := Rbar_locally p_infty) (fi1 := Fi1) (fi2 := Fi2) (ui := ui) (u' := u') (v' := v'). - typeclasses eauto. - exact Hu. - clear -H' Hf Hm1 Hm2 Hp. intros ui vi u v Hu Hv. apply RInt_helper. intros Hi. assert (ex_RInt (fun t => nth 0 (Prog.eval_real pf (t :: vars ++ map (fun c => eval c nil) cf)) 0%R * mr t) u v) as [I HI]. eapply ex_RInt_ext. intros x _. apply Hm1. apply (A.BndValuator.ex_RInt_eval prec) with (xi := I.join ui vi) (1 := H'). apply Hm2. apply contains_connected. apply Rmin_case ; apply I.join_correct. now left. now right. apply Rmax_case ; apply I.join_correct. now left. now right. contradict Hi. unfold Fi1, IT.taylor_integral_naive_intersection, fmi. clear -Hi. rewrite I.real_correct. destruct (I.convert (I.mul _ _ _)) as [|il iu] eqn:Hm. easy. exfalso. eapply I.mul_propagate_r in Hi. fold bounds in Hi. now rewrite Hm in Hi. exists I. apply (conj HI). rewrite <- is_RInt_unique with (1 := HI). apply IT.taylor_integral_naive_intersection_correct ; cycle 2. now exists I. exact Hu. exact Hv. apply I.join_correct. now left. apply I.join_correct. now right. intros xi x Hx. rewrite <- Hm1. now apply A.BndValuator.eval_correct_ext'. apply A.TaylorValuator.TM.get_tm_correct ; cycle 1. exists u. apply I.join_correct. now left. eapply A.TaylorValuator.TM.approximates_ext. intros x. rewrite <- Hm1. easy. now apply A.TaylorValuator.eval_correct_aux'. - clear -H' Hp Hf. intros ui u Hu. apply RInt_gen_helper ; [typeclasses eauto .. | idtac]. unfold Fi2. destruct I.bounded eqn:Hb ; cycle 1. now rewrite I.nai_correct. intros Hi. apply Hf with (1 := Hu) (4 := Hb). + intros t Ht. apply A.BndValuator.continuous_eval with (prec := prec) (xi := I.upper_extent ui) (1 := H') (2 := Hp). now apply I.upper_extent_correct with (1 := Hu). change (I.convert (fi (I.upper_extent ui)) <> Inan). contradict Hi. now apply I.mul_propagate_l. + intros t Ht. apply A.BndValuator.eval_correct_ext' with (1 := H'). now apply I.upper_extent_correct with (1 := Hu). + contradict Hi. now apply I.mul_propagate_r. 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