proposition: Lemma D_correct : forall (e : expr) l n, let '(a,b) := D e n in interp_domain l b -> is_derive (fun x => interp (set_nth R0 l n x) e) (nth R0 l n) (interp l a).
proof: Proof. induction e using expr_ind'. simpl => l k _. apply is_derive_ext with (fun x => if ssrnat.eqn n k then x else nth 0 l n). intros t. now rewrite nth_set_nth. case ssrnat.eqnP => [H|H]. eapply filterdiff_ext_lin. apply filterdiff_id. simpl => y ; apply sym_eq, Rmult_1_r. eapply filterdiff_ext_lin. apply filterdiff_const. simpl => y ; apply sym_eq, Rmult_0_r. simpl D => l n. assert (Dle: forall v n l, let '(a,b) := D (nth (Cst 0) le v) n in interp_domain l b -> is_derive (fun x => interp (set_nth 0 l n x) (nth (Cst 0) le v)) (nth 0 l n) (interp l a)). clear n l. induction le => v n l. rewrite nth_nil /= => _. apply: is_derive_const. simpl in H |- *. destruct v as [|v]. apply H. simpl. now apply IHle. move: (interp_AppExt_set_nth_not_const k f le l n) (uniq_index_not_const n le). case (index_not_const le n) => [|v1 [|v2 [|v3 q]]] /= Hc. intros _ _. apply is_derive_ext with (fun x => apply k f (nth 0 (map (interp l) le))). intros t. apply sym_eq. apply Hc. apply: is_derive_const. intros _. case (ssrnat.leqP (size le) v1) => Hv1. rewrite nth_default ?size_map //. now intros (_&F&_). rewrite (nth_map (Cst 0)) //. move: (Dle v1 n l). case (D (nth (Cst 0) le v1)) => /= [d1 d2] {} Dle [H1 [H2 _]]. specialize (Dle H2). apply is_derive_ext with (fun x => apply k f (fun i => if ssrnat.eqn i v1 then interp (set_nth 0 l n x) (nth (Cst 0) le v1) else nth 0 (map (interp l) le) i)). intros t. now apply sym_eq. apply: (is_derive_comp (fun x => apply k f (fun i => if ssrnat.eqn i v1 then x else nth 0 (map (interp l) le) i))) Dle. rewrite interp_set_nth. rewrite -(nth_map (Cst 0) 0) //. now apply Derive_correct. intros Hv. case (ssrnat.leqP (size le) v1) => Hv1. rewrite nth_default ?size_map //. case (nth (Cst 0, Never) (map (fun e => D e n) le) v2) => [d3 d4]. now intros (_&F&_). rewrite (nth_map (Cst 0)) //. move: (Dle v1 n l). case (D (nth (Cst 0) le v1)) => /= [d1 d2] Dle1. case (ssrnat.leqP (size le) v2) => Hv2. rewrite nth_default ?size_map //. now intros (_&_&_&F&_). rewrite (nth_map (Cst 0)) //. move: (Dle v2 n l). case (D (nth (Cst 0) le v2)) => /= [d3 d4] Dle2 {Dle} [[H1 H2] [H3 [H4 [H5 _]]]]. rewrite Rmult_comm (Rmult_comm (interp l d3) _). specialize (Dle1 H3). specialize (Dle2 H5). set (g u v := apply k f (fun i => if ssrnat.eqn i v1 then u else if ssrnat.eqn i v2 then v else nth 0 (map (interp l) le) i)). apply is_derive_ext with (fun x => g (interp (set_nth 0 l n x) (nth (Cst 0) le v1)) (interp (set_nth 0 l n x) (nth (Cst 0) le v2))). intros t. unfold g. now apply sym_eq. apply is_derive_Reals. apply derivable_pt_lim_comp_2d with (f1 := g). rewrite 2!interp_set_nth. assert (H1': ex_derive_Rn k f v1 (nth 0 (map (interp l) le))). apply locally_2d_singleton in H1. unfold ex_derive_Rn in H1 |- *. rewrite ssrnat.eqnE eqtype.eq_refl in H1. apply: ex_derive_ext H1 => t. apply apply_ext => p Hp. rewrite -ssrnat.eqnE. case E: (ssrnat.eqn p v1) => //. case E': (ssrnat.eqn p v2) => //. now rewrite (ssrnat.eqnP E'). rewrite /Derive_Rn. rewrite -(nth_map (Cst 0) 0 (interp l) Hv1). rewrite -(nth_map (Cst 0) 0 (interp l) Hv2). rewrite -(Derive_ext (fun x => g x (nth 0 (map (interp l) le) v2))). apply filterdiff_differentiable_pt_lim. eapply filterdiff_ext_lin. apply (is_derive_filterdiff g). apply filter_imp with ( 2 := proj1 (locally_2d_locally _ _ _) H1). case => u v H'. unfold g. unfold ex_derive_Rn in H'. rewrite ssrnat.eqnE eqtype.eq_refl in H'. evar_last. apply Derive_correct. apply: ex_derive_ext H' => t. apply apply_ext => p Hp. rewrite -ssrnat.eqnE. now case E: (ssrnat.eqn p v1). simpl ; reflexivity. apply is_derive_ext with (2 := Derive_correct _ _ H4) => t. apply apply_ext => p Hp. case E: (ssrnat.eqn p v1) => //. rewrite (ssrnat.eqnP E). revert Hv. rewrite /in_mem /= ssrnat.eqnE. now rewrite orbF andbT => /negbTE ->. apply continuity_2d_pt_filterlim in H2. apply: continuous_ext H2 => [[u v]]. unfold Derive_Rn. rewrite ssrnat.eqnE eqtype.eq_refl. apply Derive_ext => t. apply apply_ext => p Hp. rewrite -ssrnat.eqnE. now case E: (ssrnat.eqn p v1). intros t ; reflexivity. intros t. apply apply_ext. intros p Hp. case (ssrnat.eqn p v1) => //. case E: (ssrnat.eqn p v2) => //. now rewrite (ssrnat.eqnP E). apply is_derive_Reals, Dle1. apply is_derive_Reals, Dle2. easy. simpl => l p []. simpl => l n []. simpl => l n []. simpl => l n _. apply: is_derive_const. simpl => l n. specialize (IHe1 l n). specialize (IHe2 l n). destruct (D e1 n) as (a1,b1). destruct (D e2 n) as (a2,b2). case C1: (is_const e1 n). assert (H1 := is_const_correct e1 n C1 l). case o ; intros H2. rewrite -(Rplus_0_l (interp l a2)). apply: is_derive_plus. apply is_derive_ext with (fun x => interp (set_nth 0 l n 0) e1). apply H1. apply: is_derive_const. now apply IHe2. simpl. replace (interp l e1 * interp l a2) with (0 * interp (set_nth 0 l n (nth 0 l n)) e2 + interp l e1 * interp l a2) by ring. rewrite -(interp_set_nth n _ e1). apply is_derive_Reals. apply (derivable_pt_lim_mult (fun x => interp (set_nth 0 l n x) e1) (fun x => interp (set_nth 0 l n x) e2)). apply is_derive_Reals. apply is_derive_ext with (fun x => interp (set_nth 0 l n 0) e1). apply H1. apply: is_derive_const. apply is_derive_Reals. now apply IHe2. case C2: (is_const e2 n) => {C1}. assert (H2 := is_const_correct e2 n C2 l). case o ; intros H1. rewrite -(Rplus_0_r (interp l a1)). apply: is_derive_plus. now apply IHe1. apply is_derive_ext with (fun x => interp (set_nth 0 l n 0) e2). apply H2. apply: is_derive_const. simpl. replace (interp l a1 * interp l e2) with (interp l a1 * interp l e2 + interp (set_nth 0 l n (nth 0 l n)) e1 * 0) by ring. rewrite -(interp_set_nth n _ e2). apply is_derive_Reals. apply (derivable_pt_lim_mult (fun x => interp (set_nth 0 l n x) e1) (fun x => interp (set_nth 0 l n x) e2)). now apply is_derive_Reals, IHe1. apply is_derive_Reals. apply is_derive_ext with (fun x => interp (set_nth 0 l n 0) e2). apply H2. apply: is_derive_const. clear C2. case o ; simpl ; intros (H1&H2&_) ; specialize (IHe1 H1) ; specialize (IHe2 H2). now apply: is_derive_plus. rewrite -(interp_set_nth n _ e1) -(interp_set_nth n _ e2). apply is_derive_Reals. apply (derivable_pt_lim_mult (fun x => interp (set_nth 0 l n x) e1) (fun x => interp (set_nth 0 l n x) e2)) ; now apply is_derive_Reals. simpl => l n. specialize (IHe l n). destruct (D e n) as (a,b). case o. simpl. intros H. apply: is_derive_opp. now apply IHe. simpl. intros (H,(H0,_)). rewrite -{2}(Rmult_1_r (interp l e)). rewrite -(interp_set_nth n l e) in H0 |-*. apply is_derive_inv. now apply IHe. exact H0. simpl. intros f f' Df H. rewrite -(interp_set_nth n l e). apply: is_derive_comp. apply Df. now apply IHe. simpl. intros f f' df Df (H,(H0,_)). rewrite -(interp_set_nth n l e) in H0 |-*. apply: is_derive_comp. apply Df. exact H0. now apply IHe. simpl => l n. specialize (IHe2 l n). specialize (IHe3 l n). move: (fun l => IHe1 l (S n)) => {} IHe1. destruct (D e1 (S n)) as (a1,b1). destruct (D e2 n) as (a2,b2). destruct (D e3 n) as (a3,b3). assert (HexI: forall f x, locally x (fun x => continuity_pt f x) -> exists eps : posreal, ex_RInt f (x - eps) (x + eps)). clear => f x [eps H]. exists (pos_div_2 eps). apply ex_RInt_Reals_1. apply RiemannInt_P6. apply Rplus_lt_compat_l. apply Rle_lt_trans with (2 := cond_pos _). rewrite -Ropp_0. apply Ropp_le_contravar. apply Rlt_le. apply cond_pos. intros u Hu. apply H. apply Rle_lt_trans with (pos_div_2 eps). now apply Rabs_le_between'. rewrite (double_var eps). rewrite -(Rplus_0_r (pos_div_2 eps)). apply Rplus_lt_compat_l. apply (cond_pos (pos_div_2 eps)). assert (HexD: ( exists d : posreal, forall t u, Rmin (interp l e2) (interp l e3) - d < t < Rmax (interp l e2) (interp l e3) + d -> Rabs (u - nth 0 l n) < d -> interp_domain (t :: set_nth 0 l n u) b1 ) -> forall t, Rmin (interp l e2) (interp l e3) <= t <= Rmax (interp l e2) (interp l e3) -> locally_2d (fun u v => is_derive (fun x => interp (v :: set_nth 0 l n x) e1) u (interp (v :: set_nth 0 l n u) a1)) (nth 0 l n) t). intros (e,H) t Ht. exists e => /= u v Hu Hv. assert (H': Rmin (interp l e2) (interp l e3) - e < v < Rmax (interp l e2) (interp l e3) + e). apply (Rlt_le_trans _ _ e) in Hv. 2: apply Rle_refl. apply Rabs_lt_between' in Hv. split. apply Rle_lt_trans with (2 := proj1 Hv). now apply Rplus_le_compat_r. apply Rlt_le_trans with (1 := proj2 Hv). now apply Rplus_le_compat_r. move: (IHe1 _ (H v u H' Hu)) => {IHe1} /=. rewrite nth_set_nth /= eqtype.eq_refl. apply is_derive_ext => z. now rewrite set_set_nth /= eqtype.eq_refl. assert (Htw: forall e : posreal, forall t, Rmin (interp l e2) (interp l e3) <= t <= Rmax (interp l e2) (interp l e3) -> Rmin (interp l e2) (interp l e3) - e < t < Rmax (interp l e2) (interp l e3) + e). intros e t Ht. split. apply Rlt_le_trans with (2 := proj1 Ht). rewrite -{2}[Rmin _ _]Rplus_0_r -Ropp_0. apply Rplus_lt_compat_l. apply Ropp_lt_contravar. apply cond_pos. apply Rle_lt_trans with (1 := proj2 Ht). rewrite -{1}[Rmax _ _]Rplus_0_r. apply Rplus_lt_compat_l. apply cond_pos. case C1: (is_const e1 (S n)). clear IHe1. case C2: (is_const e2 n). simpl. intros (H3&Hi&H1&_). apply is_derive_ext with (comp (fun x => RInt (fun t => interp (t :: l) e1) (interp (set_nth 0 l n (nth 0 l n)) e2) x) (fun x => interp (set_nth 0 l n x) e3)). intros t. unfold comp. rewrite -(is_const_correct e2 n C2 l (nth 0 l n)). apply RInt_ext. intros z _. rewrite -(interp_set_nth (S n)). apply (is_const_correct e1 (S n) C1 (z :: l)). apply: is_derive_comp. rewrite 2!interp_set_nth. apply (is_derive_RInt (fun t : R => interp (t :: l)%SEQ e1) _ (interp l e2)). apply HexI in H1. case: H1 => e He. exists e => /= y Hy. apply: RInt_correct. eapply ex_RInt_Chasles. apply Hi. eapply ex_RInt_Chasles. eapply ex_RInt_Chasles, He. eapply ex_RInt_swap, @ex_RInt_Chasles_1, He. apply Rabs_le_between'. rewrite Rminus_eq_0 Rabs_R0 ; by apply Rlt_le, e. eapply ex_RInt_swap, @ex_RInt_Chasles_2, He. apply Rabs_le_between'. by apply Rlt_le, Hy. now apply continuity_pt_filterlim, locally_singleton. now apply IHe3. clear C2. case C3: (is_const e3 n). simpl. intros (H2&Hi&H1&_). rewrite -Ropp_mult_distr_r_reverse. apply is_derive_ext with (fun x => comp (fun x => RInt (fun t => interp (t :: l) e1) x (interp (set_nth 0 l n (nth 0 l n)) e3)) (fun x => interp (set_nth 0 l n x) e2) x). intros t. unfold comp. rewrite -(is_const_correct e3 n C3 l (nth 0 l n)). apply RInt_ext. intros z _. rewrite -(interp_set_nth (S n)). apply (is_const_correct e1 (S n) C1 (z :: l)). apply: (is_derive_comp (fun x0 : R => RInt (fun t : R => interp (t :: l) e1) x0 (interp (set_nth 0 l n (nth 0 l n)) e3)) (fun x0 : R => interp (set_nth 0 l n x0) e2)). rewrite 2!interp_set_nth. apply (is_derive_RInt' (fun t : R => interp (t :: l)%SEQ e1) _ _ (interp l e3)). apply HexI in H1. case: H1 => e He. exists e => /= y Hy. apply: RInt_correct. eapply ex_RInt_Chasles, Hi. eapply ex_RInt_Chasles. eapply ex_RInt_Chasles, He. eapply ex_RInt_swap, @ex_RInt_Chasles_1, He. apply Rabs_le_between'. by apply Rlt_le, Hy. eapply ex_RInt_swap, @ex_RInt_Chasles_2, He. apply Rabs_le_between'. rewrite Rminus_eq_0 Rabs_R0 ; by apply Rlt_le, e. now apply continuity_pt_filterlim, locally_singleton. now apply IHe2. clear C3. simpl. intros (H2&H3&Hi&H12&H13&_). apply is_derive_ext with (fun x => RInt (fun t => interp (t :: l) e1) (interp (set_nth 0 l n x) e2) (interp (set_nth 0 l n x) e3)). intros t. apply RInt_ext. intros z _. rewrite -(interp_set_nth (S n)). apply (is_const_correct e1 (S n) C1 (z :: l)). rewrite -(interp_set_nth n l e2) -(interp_set_nth n l e3). evar_last. apply (is_derive_RInt_bound_comp (fun t : R => interp (t :: l)%SEQ e1)). rewrite 2!interp_set_nth. eapply filter_imp. intros x Hx ; simpl. apply: RInt_correct. exact: Hx. apply @ex_RInt_locally => //. now apply HexI. now apply HexI. rewrite interp_set_nth. now apply continuity_pt_filterlim, locally_singleton. rewrite interp_set_nth. now apply continuity_pt_filterlim, locally_singleton. now apply IHe2. now apply IHe3. reflexivity. case C2: (is_const e2 n). clear IHe2. case C3: (is_const e3 n). clear IHe3. clear C1. simpl. intros (H3&H2&H4&_). apply is_derive_ext with (fun x => RInt (fun t => interp (t :: set_nth 0 l n x) e1) (interp (set_nth 0 l n (nth 0 l n)) e2) (interp (set_nth 0 l n (nth 0 l n)) e3)). intros t. apply f_equal2. now apply is_const_correct. now apply is_const_correct. rewrite 2!interp_set_nth. destruct H3 as (d,H3). assert (H3': locally (nth R0 l n) (fun x => forall t, Rmin (interp l e2) (interp l e3) <= t <= Rmax (interp l e2) (interp l e3) -> interp_domain (set_nth 0 (t :: l) (S n) x) b1)). exists d => y Hy t Ht. apply H3. split. apply Rlt_le_trans with (2 := proj1 Ht). rewrite -{2}[Rmin _ _]Rplus_0_r -Ropp_0. apply Rplus_lt_compat_l. apply Ropp_lt_contravar. apply cond_pos. apply Rle_lt_trans with (1 := proj2 Ht). rewrite -{1}[Rmax _ _]Rplus_0_r. apply Rplus_lt_compat_l. apply cond_pos. exact Hy. rewrite (RInt_ext (fun x => interp (x :: l) a1) (fun x => Derive (fun t => interp (set_nth 0 (x :: l) (S n) t) e1) (nth 0 (x :: l) (S n)))). apply is_derive_RInt_param. move: H3' ; apply filter_imp => y H3' t Ht. specialize (IHe1 _ (H3' t Ht)). rewrite nth_set_nth /= eqtype.eq_refl in IHe1. exists (interp (set_nth 0 (t :: l) (S n) y) a1). apply is_derive_ext with (f := fun x => interp (set_nth 0 (set_nth 0 (t :: l) (S n) y) (S n) x) e1) (2 := IHe1). intros t'. now rewrite set_set_nth eqtype.eq_refl. intros t Ht. apply continuity_2d_pt_ext_loc with (f := fun x y => interp (set_nth 0 (y :: l) (S n) x) a1). exists d => u v Hu Hv. apply sym_eq. apply is_derive_unique. apply is_derive_ext with (f := fun z => interp (set_nth 0 (set_nth 0 (v :: l) (S n) u) (S n) z) e1). intros z. now rewrite set_set_nth eqtype.eq_refl. pattern u at 2; replace u with (nth 0 (set_nth 0 (v :: l) (S n) u) (S n)). apply IHe1. apply H3. apply Rabs_lt_between' in Hv. split. apply Rle_lt_trans with (2 := proj1 Hv). now apply Rplus_le_compat_r. apply Rlt_le_trans with (1 := proj2 Hv). now apply Rplus_le_compat_r. exact Hu. now rewrite nth_set_nth /= eqtype.eq_refl. now apply H4. move: H2 ; apply filter_imp => y. rewrite (is_const_correct e2 n C2 l y (nth 0 l n)). rewrite (is_const_correct e3 n C3 l y (nth 0 l n)). now rewrite 2!interp_set_nth. intros t Ht. apply sym_eq. apply is_derive_unique. apply locally_singleton in H3'. apply (IHe1 (t :: l)). cut (interp_domain (set_nth 0 (t :: l)%SEQ (S n) (nth 0 l n)) b1). apply (interp_domain_set_nth (S n) (t :: l)). apply H3'. now split ; apply Rlt_le. clear C1 C3. simpl. intros (H2&H3&H6&H7&H8&H10&H11&_). rewrite Rplus_comm Rmult_comm. apply is_derive_ext with (fun x => RInt (fun t => interp (t :: set_nth 0 l n x) e1) (interp l e2) (interp (set_nth 0 l n x) e3)). intros x. rewrite (is_const_correct e2 n C2 l x (nth 0 l n)). now rewrite interp_set_nth. rewrite -(RInt_ext (fun x => Derive (fun t => interp (x :: set_nth 0 l n t) e1) (nth 0 l n))). rewrite -(interp_set_nth (S n) (interp l e3 :: l) e1). rewrite -(interp_set_nth n l e3) /=. apply (is_derive_RInt_param_bound_comp_aux3 (fun x t => interp (t :: set_nth 0 l n x) e1) (interp l e2) (fun x => interp (set_nth 0 l n x) e3)). now rewrite interp_set_nth. now rewrite interp_set_nth. now apply IHe3. rewrite interp_set_nth. destruct H11 as (e&H11). exists (pos_div_2 e). exists e => y Hy t Ht. assert (Ht': Rmin (interp l e2) (interp l e3) - e < t < Rmax (interp l e2) (interp l e3) + e). split. apply Rlt_le_trans with (2 := proj1 Ht). apply Rlt_le_trans with (Rmin (interp l e2) (interp l e3) - pos_div_2 e). apply Rplus_lt_compat_l. apply Ropp_lt_contravar. rewrite -(Rplus_0_r (pos_div_2 e)) /= {2}(double_var e). apply Rplus_lt_compat_l. apply is_pos_div_2. rewrite /Rminus Rplus_min_distr_r. apply Rle_min_compat_r. rewrite -{2}[interp l e2]Rplus_0_r -Ropp_0. apply Rplus_le_compat_l. apply Ropp_le_contravar. apply Rlt_le, cond_pos. apply Rle_lt_trans with (1 := proj2 Ht). apply Rle_lt_trans with (Rmax (interp l e2) (interp l e3) + pos_div_2 e). rewrite /Rminus Rplus_max_distr_r. apply Rle_max_compat_r. rewrite -{1}[interp l e2]Rplus_0_r. apply Rplus_le_compat_l. apply Rlt_le, cond_pos. apply Rplus_lt_compat_l. rewrite -(Rplus_0_r (pos_div_2 e)) /= {2}(double_var e). apply Rplus_lt_compat_l. apply is_pos_div_2. eexists. move: (IHe1 _ (H11 t y Ht' Hy)) => {IHe1} /=. rewrite nth_set_nth /= eqtype.eq_refl. apply is_derive_ext => z. now rewrite set_set_nth eqtype.eq_refl. rewrite interp_set_nth. intros t Ht. apply continuity_2d_pt_ext_loc with (f := fun x y => interp (set_nth 0 (y :: l) (S n) x) a1). apply: locally_2d_impl (HexD H11 t Ht). apply locally_2d_forall => u v H. apply sym_eq. now apply is_derive_unique. now apply H3. rewrite interp_set_nth. apply: locally_2d_impl H2. specialize (HexD H11 _ (conj (Rmin_r _ _) (Rmax_r _ _))). apply: locally_2d_impl_strong HexD. apply locally_2d_forall => u v H. rewrite nth_set_nth /= eqtype.eq_refl. apply continuity_2d_pt_ext_loc. apply: locally_2d_impl H. apply locally_2d_forall => u' v' H. apply sym_eq. apply is_derive_unique. now rewrite set_set_nth eqtype.eq_refl. rewrite interp_set_nth. apply locally_singleton in H7. apply: continuity_pt_ext H7. intros t. apply sym_eq. apply (interp_set_nth (S n) (t :: l)). intros t Ht. apply is_derive_unique. apply (IHe1 (t :: l)). destruct H11 as (e,H11). specialize (H11 t (nth 0 l n)). rewrite -(interp_domain_set_nth (S n)) /=. apply H11. apply Htw. now split ; apply Rlt_le. rewrite /Rminus Rplus_opp_r Rabs_R0. apply cond_pos. case C3: (is_const e3 n). clear IHe3. clear C1 C2. simpl. intros (H2&H3&H6&H7&H8&H10&H11&_). rewrite Rplus_comm Rmult_comm -Ropp_mult_distr_l_reverse. apply is_derive_ext with (fun x => RInt (fun t => interp (t :: set_nth 0 l n x) e1) (interp (set_nth 0 l n x) e2) (interp l e3)). intros x. rewrite (is_const_correct e3 n C3 l x (nth 0 l n)). now rewrite interp_set_nth. rewrite -(RInt_ext (fun x => Derive (fun t => interp (x :: set_nth 0 l n t) e1) (nth 0 l n))). rewrite -(interp_set_nth (S n) (interp l e2 :: l) e1). rewrite -(interp_set_nth n l e2) /=. apply (is_derive_RInt_param_bound_comp_aux2 (fun x t => interp (t :: set_nth 0 l n x) e1) (fun x => interp (set_nth 0 l n x) e2) (interp l e3)). now rewrite interp_set_nth. now rewrite interp_set_nth. now apply IHe2. rewrite interp_set_nth. destruct H11 as (e&H11). exists (pos_div_2 e). exists e => y Hy t Ht. assert (Ht': Rmin (interp l e2) (interp l e3) - e < t < Rmax (interp l e2) (interp l e3) + e). split. apply Rlt_le_trans with (2 := proj1 Ht). apply Rlt_le_trans with (Rmin (interp l e2) (interp l e3) - pos_div_2 e). apply Rplus_lt_compat_l. apply Ropp_lt_contravar. rewrite -(Rplus_0_r (pos_div_2 e)) /= {2}(double_var e). apply Rplus_lt_compat_l. apply is_pos_div_2. rewrite /Rminus Rplus_min_distr_r. apply Rle_min_compat_l. rewrite -{2}[interp l e3]Rplus_0_r -Ropp_0. apply Rplus_le_compat_l. apply Ropp_le_contravar. apply Rlt_le, cond_pos. apply Rle_lt_trans with (1 := proj2 Ht). apply Rle_lt_trans with (Rmax (interp l e2) (interp l e3) + pos_div_2 e). rewrite /Rminus Rplus_max_distr_r. apply Rle_max_compat_l. rewrite -{1}[interp l e3]Rplus_0_r. apply Rplus_le_compat_l. apply Rlt_le, cond_pos. apply Rplus_lt_compat_l. rewrite -(Rplus_0_r (pos_div_2 e)) /= {2}(double_var e). apply Rplus_lt_compat_l. apply is_pos_div_2. eexists. move: (IHe1 _ (H11 t y Ht' Hy)) => {IHe1} /=. rewrite nth_set_nth /= eqtype.eq_refl. apply is_derive_ext => z. now rewrite set_set_nth eqtype.eq_refl. rewrite interp_set_nth. intros t Ht. apply continuity_2d_pt_ext_loc with (f := fun x y => interp (set_nth 0 (y :: l) (S n) x) a1). apply: locally_2d_impl (HexD H11 t Ht). apply locally_2d_forall => u v H. apply sym_eq. now apply is_derive_unique. now apply H3. rewrite interp_set_nth. apply: locally_2d_impl H2. specialize (HexD H11 _ (conj (Rmin_l _ _) (Rmax_l _ _))). apply: locally_2d_impl_strong HexD. apply locally_2d_forall => u v H. rewrite nth_set_nth /= eqtype.eq_refl. apply continuity_2d_pt_ext_loc. apply: locally_2d_impl H. apply locally_2d_forall => u' v' H. apply sym_eq. apply is_derive_unique. now rewrite set_set_nth eqtype.eq_refl. rewrite interp_set_nth. apply locally_singleton in H7. apply: continuity_pt_ext H7. intros t. apply sym_eq. apply (interp_set_nth (S n) (t :: l)). intros t Ht. apply is_derive_unique. apply (IHe1 (t :: l)). destruct H11 as (e,H11). specialize (H11 t (nth 0 l n)). rewrite -(interp_domain_set_nth (S n)) /=. apply H11. apply Htw. now split ; apply Rlt_le. rewrite /Rminus Rplus_opp_r Rabs_R0. apply cond_pos. clear C1 C2 C3. simpl. intros (H1&H2&H3&H4&H5&H6&H7&H8&H9&H10&H11&_). rewrite Rplus_comm Rmult_comm (Rmult_comm (interp l a2)) -Ropp_mult_distr_l_reverse. rewrite [_*_+_]Rplus_comm -Rplus_assoc. rewrite -(RInt_ext (fun x => Derive (fun t => interp (x :: set_nth 0 l n t) e1) (nth 0 l n))). rewrite -(interp_set_nth (S n) (interp l e2 :: l) e1) -(interp_set_nth (S n) (interp l e3 :: l) e1). rewrite -(interp_set_nth n l e2) -(interp_set_nth n l e3) /=. apply (is_derive_RInt_param_bound_comp (fun x t => interp (t :: set_nth 0 l n x) e1) (fun x => interp (set_nth 0 l n x) e2) (fun x => interp (set_nth 0 l n x) e3)). rewrite 2!interp_set_nth. exact H8. rewrite interp_set_nth. exact H9. rewrite interp_set_nth. exact H10. now apply IHe2. now apply IHe3. rewrite 2!interp_set_nth. destruct H11 as (e&H11). exists (pos_div_2 e). exists e => y Hy t Ht. assert (Ht': Rmin (interp l e2) (interp l e3) - e < t < Rmax (interp l e2) (interp l e3) + e). split. apply Rlt_le_trans with (2 := proj1 Ht). rewrite /Rminus -Rplus_min_distr_r. apply Rplus_lt_compat_l. apply Ropp_lt_contravar. rewrite -(Rplus_0_r (pos_div_2 e)) /= {2}(double_var e). apply Rplus_lt_compat_l. apply is_pos_div_2. apply Rle_lt_trans with (1 := proj2 Ht). rewrite -Rplus_max_distr_r. apply Rplus_lt_compat_l. rewrite -(Rplus_0_r (pos_div_2 e)) /= {2}(double_var e). apply Rplus_lt_compat_l. apply is_pos_div_2. eexists. move: (IHe1 _ (H11 t y Ht' Hy)) => {IHe1} /=. rewrite nth_set_nth /= eqtype.eq_refl. apply is_derive_ext => z. now rewrite set_set_nth eqtype.eq_refl. rewrite 2!interp_set_nth. intros t Ht. apply continuity_2d_pt_ext_loc with (f := fun x y => interp (set_nth 0 (y :: l) (S n) x) a1). apply: locally_2d_impl (HexD H11 t Ht). apply locally_2d_forall => u v H. apply sym_eq. now apply is_derive_unique. now apply H3. rewrite interp_set_nth. apply: locally_2d_impl H1. specialize (HexD H11 _ (conj (Rmin_l _ _) (Rmax_l _ _))). apply: locally_2d_impl_strong HexD. apply locally_2d_forall => u v H. rewrite nth_set_nth /= eqtype.eq_refl. apply continuity_2d_pt_ext_loc. apply: locally_2d_impl H. apply locally_2d_forall => u' v' H. apply sym_eq. apply is_derive_unique. now rewrite set_set_nth eqtype.eq_refl. rewrite interp_set_nth. apply: locally_2d_impl H2. specialize (HexD H11 _ (conj (Rmin_r _ _) (Rmax_r _ _))). apply: locally_2d_impl_strong HexD. apply locally_2d_forall => u v H. rewrite nth_set_nth /= eqtype.eq_refl. apply continuity_2d_pt_ext_loc. apply: locally_2d_impl H. apply locally_2d_forall => u' v' H. apply sym_eq. apply is_derive_unique. now rewrite set_set_nth eqtype.eq_refl. rewrite interp_set_nth. apply locally_singleton in H5. apply: continuity_pt_ext H5. intros t. apply sym_eq. apply (interp_set_nth (S n) (t :: l)). rewrite interp_set_nth. apply locally_singleton in H7. apply: continuity_pt_ext H7. intros t. apply sym_eq. apply (interp_set_nth (S n) (t :: l)). intros t Ht. apply is_derive_unique. apply (IHe1 (t :: l)). destruct H11 as (e,H11). specialize (H11 t (nth 0 l n)). rewrite -(interp_domain_set_nth (S n)) /=. apply H11. apply Htw. now split ; apply Rlt_le. rewrite /Rminus Rplus_opp_r Rabs_R0. apply cond_pos. Qed.
imports: Coq(Reals Datatypes ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy Derive RInt RInt_analysis Derive_2d Continuity ElemFct