proposition: Lemma prolongement_C1_derivable : forall (f d : R -> R) (a b : R), a <= b -> (forall c, a <= c <= b -> derivable_pt_abs f c (d c)) -> { derg | forall x, derive (C1_continuation f a b d) derg x = C1_continuation_derive d a b x}.
proof: Proof. intros f d a b Hab Hder. assert (Hrew : forall c u v, v <> 0 -> (c * (u + v - u) + f u - f u) / v - d u = c - d u) by ( intros; field; assumption). assert (Hrew2 : forall u x h z, h <> 0 -> ((u * (x + h - z) + f z -(u * (x - z) + f z)) / h - u) = 0) by (intros; field; assumption). assert(forall x, derivable_pt_abs (C1_continuation f a b d) x (C1_continuation_derive d a b x)). intro x. unfold C1_continuation, C1_continuation_derive, derivable_pt_abs, derivable_pt_lim. destruct (Rlt_dec x a) as [Hxa | Hax]. destruct (Rle_dec x b) as [Hxb | Hxb]. intros eps Heps. exists (mkposreal (a-x) (Rgt_minus _ _ Hxa)). intros h hneq Hcond. destruct(Rlt_dec (x+h) a) as [Hxha | Hxha]. rewrite Hrew2, Rabs_R0; assumption; apply Heps. apply False_ind, Hxha. apply Rle_lt_trans with (x+ Rabs h). apply Rplus_le_compat_l. apply RRle_abs. replace a with (x + a + -x) by ring. rewrite Rplus_assoc; apply Rplus_lt_compat_l. apply Hcond. apply False_ind, Hxb. apply Rle_trans with a; intuition (auto with real). destruct (Rle_dec x b) as [Hxb | Hxb]. intros eps Heps. apply Rnot_lt_le in Hax. assert (Hx : a <= x <= b) by (split;assumption). destruct (Hder x Hx eps Heps) as [delta Hdelta]. destruct Hxb as [Hxb | Hxb]. destruct Hax as [Hax |Hax]. assert (0 < Rmin delta (Rmin (b-x) (x - a))) as Hposreal. apply Rmin_pos. apply cond_pos. apply Rmin_pos; lra. exists (mkposreal _ Hposreal). intros h hneq Hcond. destruct(Rlt_dec (x+h) a) as [Hxha | Hxha]. apply False_ind; apply (Rlt_not_le _ _ Hxha). assert(- h < x - a) as Hf. apply Rle_lt_trans with (Rabs h). rewrite <- Rabs_Ropp; apply RRle_abs. apply Rlt_le_trans with (Rmin (b - x) (x - a)). apply (proj2 ((Rmin_Rgt_l delta (Rmin (b - x) (x - a)) (Rabs h) Hcond))). apply Rmin_r. lra. destruct (Rle_dec (x+h) b) as [Hxhb | Hxhb]. apply (Hdelta _ hneq). apply (proj1 (Rmin_Rgt_l delta _ _ Hcond)). apply False_ind, Hxhb. replace b with (x + (b - x)) by ring. apply Rplus_le_compat_l. apply Rle_trans with (Rabs h). apply RRle_abs. apply Rle_trans with (Rmin (b - x) (x - a)). left; apply (proj2 ((Rmin_Rgt_l delta _ (Rabs h) Hcond))). apply Rmin_l. subst x. assert( Hposreal : 0 < Rmin delta (b-a)). apply Rmin_pos. apply cond_pos. lra. exists (mkposreal _ Hposreal). intros h hneq Hcond. destruct (Rlt_dec (a + h) a) as [Hah | Hah]. rewrite Hrew. ring_simplify (d a - d a). rewrite Rabs_R0; apply Heps. apply hneq. destruct(Rle_dec (a+h) b) as [Hh | Hh]. apply (Hdelta h hneq). apply Rlt_le_trans with (Rmin delta (b-a)). apply Hcond. apply Rmin_l. apply False_ind, Hh. replace b with (a + (b-a)) by ring. apply Rplus_le_compat_l. apply Rle_trans with (Rabs h). apply RRle_abs. apply Rle_trans with (Rmin delta (b-a)). left; apply Hcond. apply Rmin_r. subst x. destruct Hax as [Hax | Hax]. assert( Hposreal : 0 < Rmin delta (b-a)). apply Rmin_pos. apply cond_pos. lra. exists (mkposreal _ Hposreal). intros h hneq Hcond. destruct (Rlt_dec (b + h) a) as [Hbh | Hbh]. apply False_ind, (Rlt_not_le _ _ Hbh). assert(- h <= b - a) as Hf. apply Rle_trans with (Rabs h). rewrite <- Rabs_Ropp; apply RRle_abs. apply Rle_trans with (Rmin delta (b - a)). intuition (auto with real). apply Rmin_r. lra. destruct(Rle_dec (b+h) b) as [Hh | Hh]. apply (Hdelta h hneq). apply Rlt_le_trans with (Rmin delta (b - a)). apply Hcond. apply Rmin_l. rewrite Hrew. ring_simplify ( d b - d b). rewrite Rabs_R0; apply Heps. apply hneq. subst b. exists delta. intros h hneq Hcond. destruct(Rlt_dec (a+h) a). rewrite Hrew. ring_simplify ( d a - d a). rewrite Rabs_R0; apply Heps. apply hneq. destruct (Rle_dec (a+h) a) as [Hh | Hh]. intuition. rewrite Hrew. ring_simplify ( d a - d a). rewrite Rabs_R0; apply Heps. apply hneq. destruct (Rle_dec x b). intros eps Heps. apply Rnot_le_lt in Hxb. exists (mkposreal (x - b) (Rgt_minus _ _ Hxb)). intros h hneq Hcond. destruct(Rlt_dec (x+h) a) as [Hxha | Hxha]. apply False_ind, (RIneq.Rle_not_lt _ _ Hab). apply Rlt_le_trans with (x+h). assert(- h <= x - b) as Hf. apply Rle_trans with (Rabs h). rewrite <- Rabs_Ropp; apply RRle_abs. intuition (auto with real). lra. intuition (auto with real). destruct (Rle_dec (x + h) b) as [Hh | Hh]. apply False_ind, (RIneq.Rle_not_lt _ _ Hh). assert(- h <= x - b) as Hf. apply Rle_trans with (Rabs h). rewrite <- Rabs_Ropp; apply RRle_abs. intuition (auto with real). lra. rewrite Hrew2, Rabs_R0; assumption; apply Heps. intros eps Heps. apply Rnot_le_lt in Hxb. exists (mkposreal (x - b) (Rgt_minus _ _ Hxb)). intros h hneq Hcond. destruct(Rlt_dec (x+h) a) as [Hxha | Hxha]. apply False_ind, (RIneq.Rle_not_lt _ _ Hab). apply Rlt_le_trans with (x+h). assert(- h <= x - b) as Hf. apply Rle_trans with (Rabs h). rewrite <- Rabs_Ropp; apply RRle_abs. intuition (auto with real). lra. intuition (auto with real). destruct (Rle_dec (x + h) b) as [Hh | Hh]. apply False_ind, (RIneq.Rle_not_lt _ _ Hh). assert(- h < x - b) as Hf. apply Rle_lt_trans with (Rabs h). rewrite <- Rabs_Ropp; apply RRle_abs. intuition (auto with real). lra. rewrite Hrew2, Rabs_R0; assumption. assert(derivable (C1_continuation f a b d)) as der_c by (intro x; exists (C1_continuation_derive d a b x); apply H). exists der_c. intro x. unfold derive. apply uniqueness_limite with (C1_continuation f a b d) x. eapply derive_pt_eq_1. reflexivity. apply H. Qed.
imports: Reals Lra Rfunctions