proposition: Lemma extension_C1_is_derive (f df : R -> V) (a b : Rbar) : Rbar_le a b -> (forall x : R, Rbar_le a x -> Rbar_le x b -> is_derive f x (df x)) -> forall x : R, is_derive (extension_C1 f df a b) x (extension_C0 df a b x).
proof: Proof. intros Hab Cf x. apply Rbar_le_lt_or_eq_dec in Hab ; case: Hab => Hab. case: (Rbar_lt_le_dec x a) => Hax. evar_last. eapply is_derive_ext_loc. apply locally_interval with m_infty a. by []. by []. move => y _ Hay. rewrite /extension_C1. case: Rbar_le_dec => H. contradict H ; by apply Rbar_lt_not_le. reflexivity. apply is_derive_plus. apply is_derive_const. apply @is_derive_scal_l. apply @is_derive_minus. apply is_derive_id. apply is_derive_const. rewrite plus_zero_l minus_zero_r scal_one. rewrite /extension_C0. case: Rbar_le_dec => H //. by apply Rbar_le_not_lt in H. apply Rbar_le_lt_or_eq_dec in Hax ; case: Hax => Hax. case: (Rbar_lt_le_dec x b) => Hbx. evar_last. eapply is_derive_ext_loc. apply locally_interval with a b. by []. by []. move => y Hay Hby. apply sym_eq, extension_C1_ext ; by apply Rbar_lt_le. apply Cf ; by apply Rbar_lt_le. rewrite /extension_C0. case: Rbar_le_dec => // H. case: Rbar_le_dec => // H0. by apply Rbar_lt_le in Hbx. by apply Rbar_lt_le in Hax. apply Rbar_le_lt_or_eq_dec in Hbx ; case: Hbx => Hbx. evar_last. eapply is_derive_ext_loc. apply locally_interval with b p_infty. by []. by []. move => y Hby _. rewrite /extension_C1. case: Rbar_le_dec => H. case: Rbar_le_dec => H0. contradict H0 ; by apply Rbar_lt_not_le. reflexivity. contradict H ; eapply Rbar_le_trans, Rbar_lt_le, Hby. by apply Rbar_lt_le. apply is_derive_plus. apply is_derive_const. apply @is_derive_scal_l. apply @is_derive_minus. apply is_derive_id. apply is_derive_const. rewrite plus_zero_l minus_zero_r scal_one. rewrite /extension_C0. case: Rbar_le_dec => H //. case: Rbar_le_dec => H0 //. by apply Rbar_le_not_lt in H0. by apply Rbar_lt_le in Hax. destruct b as [b | | ] => //. injection Hbx => {} Hbx. rewrite -Hbx {x Hbx} in Hax |- *. evar_last. apply is_derive_ext_loc with (extension_cont f (fun x => plus (f (real b)) (scal (x - real b) (df (real b)))) b). apply locally_interval with a p_infty => //. move => y Hay _. rewrite /extension_cont /extension_C1. case: Rle_dec => H ; case: Rbar_le_dec => H0 ; case: (Rbar_le_dec y b) => // _. contradict H0 ; by apply Rbar_lt_le. contradict H0 ; by apply Rbar_lt_le. apply extension_cont_is_derive => //. apply Cf => /=. by apply Rbar_lt_le. by apply Rle_refl. evar_last. apply is_derive_plus. apply is_derive_const. apply @is_derive_scal_l. apply @is_derive_minus. apply is_derive_id. apply is_derive_const. by rewrite plus_zero_l minus_zero_r scal_one. by rewrite Rminus_eq_0 @scal_zero_l plus_zero_r. rewrite /extension_C0. case: Rbar_le_dec => H0. case: Rbar_le_dec (Rle_refl b) => //. by apply Rbar_lt_le in Hax. destruct a as [a | | ] => //. injection Hax => {} Hax. rewrite -Hax {x Hax}. evar_last. apply is_derive_ext_loc with (extension_cont (fun x => plus (f (real a)) (scal (x - real a) (df (real a)))) f a). apply locally_interval with m_infty b => //. move => y _ Hbx. rewrite /extension_cont /extension_C1. case: Rle_dec => H ; case: Rbar_le_dec => //= H0 ; try case: Rbar_le_dec => // H1. replace y with a by now apply Rle_antisym. by rewrite Rminus_eq_0 @scal_zero_l plus_zero_r. contradict H1 ; by apply Rbar_lt_le. contradict H1 ; by apply Rbar_lt_le. by contradict H0 ; apply Rlt_le, Rnot_le_lt. apply extension_cont_is_derive => //. apply is_derive_plus. apply is_derive_const. apply @is_derive_scal_l. apply @is_derive_minus. apply is_derive_id. apply is_derive_const. rewrite plus_zero_l minus_zero_r scal_one. apply Cf. by apply Rle_refl. by apply Rbar_lt_le. by rewrite Rminus_eq_0 @scal_zero_l plus_zero_r. rewrite plus_zero_l minus_zero_r scal_one. rewrite /extension_C0. case: Rbar_le_dec (Rle_refl a) => // _ _. case: Rbar_le_dec => H //. by apply Rbar_lt_le in Hab. rewrite -Hab {b Hab Cf}. evar_last. eapply is_derive_ext. intros y. rewrite /extension_C1. case: Rbar_le_dec => H. 2: reflexivity. case: Rbar_le_dec => // H0. destruct a as [a | | ] => //. replace y with a by now apply Rle_antisym. by rewrite Rminus_eq_0 @scal_zero_l plus_zero_r. apply is_derive_plus. apply is_derive_const. apply @is_derive_scal_l. apply @is_derive_minus. apply is_derive_id. apply is_derive_const. rewrite plus_zero_l minus_zero_r scal_one. rewrite /extension_C0. case: Rbar_le_dec => H //. case: Rbar_le_dec => H0 //. destruct a as [a | | ] => //. by replace a with x by now apply Rle_antisym. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv