Library Coqtail.mytheories.myReals.MyRfunctions
Power
Lemma Rpow_mult_distr : ∀ x y n, (x × y) ^ n = x ^ n × y ^ n.
Proof.
intros x y n; induction n; simpl.
field.
repeat (rewrite Rmult_assoc); apply Rmult_eq_compat_l.
rewrite IHn; field.
Qed.
Distance
Lemma R_dist_ge_l : ∀ x y z, R_dist x y ≤ z → Rabs x ≤ Rabs y + z.
Proof.
unfold R_dist; unfold Rabs.
intros x y z H.
repeat destruct Rcase_abs; fourier.
Qed.
Lemma R_dist_gt_l : ∀ x y z, R_dist x y < z → Rabs x < Rabs y + z.
Proof.
unfold R_dist; unfold Rabs.
intros x y z H.
repeat destruct Rcase_abs; fourier.
Qed.
Lemma R_dist_ge_r : ∀ x y z, R_dist x y ≤ z → Rabs y - z ≤ Rabs x.
Proof.
unfold R_dist; unfold Rabs.
intros x y z H.
repeat destruct Rcase_abs; fourier.
Qed.
Lemma R_dist_gt_r : ∀ x y z, R_dist x y < z → Rabs y - z < Rabs x.
Proof.
unfold R_dist; unfold Rabs.
intros x y z H.
repeat destruct Rcase_abs; fourier.
Qed.
Lemma continuity_pt_constant : ∀ c x, continuity_pt (fct_cte c) x.
Proof.
intros c x ; apply continuity_const.
intros u y; reflexivity.
Qed.
Lemma continuity_constant : ∀ c, continuity (fct_cte c).
Proof.
intro c; apply continuity_const.
intros x y; reflexivity.
Qed.
C1 continuation of a C1 function on a segment
Section Rint_C1.
Definition C1_continuation f a b d:=
fun x : R ⇒
if Rlt_dec x a then d a × (x - a) + f a
else if Rle_dec x b then f x else d b × (x - b) + f b .
Definition C1_continuation_derive d a b : R → R :=
fun x : R ⇒
if Rlt_dec x a then d a
else if Rle_dec x b then d x else d b.
Lemma C1_continuation_eq : ∀ f a b d x,
a ≤ x ≤ b → C1_continuation f a b d x = f x.
Proof.
intros f a b d x Hx.
unfold C1_continuation.
destruct (Rlt_dec x a).
apply False_ind; apply (Rlt_not_le _ _ r), (proj1 Hx).
destruct (Rle_dec x b).
reflexivity.
apply False_ind, n0, (proj2 Hx).
Qed.
Lemma C1_continuation_derive_eq : ∀ a b d x,
a ≤ x ≤ b → C1_continuation_derive d a b x = d x.
Proof.
intros a b d x Hx.
unfold C1_continuation_derive.
destruct (Rlt_dec x a).
apply False_ind; apply (Rlt_not_le _ _ r), (proj1 Hx).
destruct (Rle_dec x b).
reflexivity.
apply False_ind, n0, (proj2 Hx).
Qed.
Lemma prolongement_C1_derivable : ∀ (f d : R → R) (a b : R),
a ≤ b →
(∀ c, a ≤ c ≤ b → derivable_pt_abs f c (d c)) →
{ derg | ∀ x, derive (C1_continuation f a b d) derg x =
C1_continuation_derive d a b x}.
Proof.
intros f d a b Hab Hder.
assert (Hrew : ∀ 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 : ∀ 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(∀ 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.
∃ (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.
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; fourier.
∃ (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.
fourier.
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.
fourier.
∃ (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.
fourier.
∃ (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.
apply Rmin_r.
fourier.
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. ∃ 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.
∃ (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.
fourier.
intuition.
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.
fourier.
rewrite Hrew2, Rabs_R0; assumption; apply Heps.
intros eps Heps.
apply Rnot_le_lt in Hxb.
∃ (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.
fourier.
intuition.
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.
fourier.
rewrite Hrew2, Rabs_R0; assumption.
assert(derivable (C1_continuation f a b d)) as der_c by
(intro x; ∃ (C1_continuation_derive d a b x); apply H).
∃ 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.
Lemma C0_sticking_one_pt : ∀ f gl gr a,
continuity gl → continuity gr →
(∀ x, x ≤ a → f x = gl x) →
(∀ x, a ≤ x → f x = gr x) →
continuity f.
Proof.
intros f gl gr a Hl Hr Hfl Hfr x.
destruct (Rtotal_order x a).
intros eps Heps.
destruct (Hl x eps); try assumption.
destruct H0.
destruct (Rlt_dec x0 (a - x)).
∃ x0; split; try assumption.
intro.
destruct (Rlt_dec a x1).
intros.
assert False; try contradiction.
apply (Rgt_asym a x1); try assumption.
destruct H2; simpl in H3; unfold R_dist in H3.
assert ((x1 - x) ≤ Rabs (x1 - x)) by apply RRle_abs.
fourier.
repeat rewrite Hfl.
apply (H1 x1). fourier.
apply Rnot_lt_le; assumption.
apply Rnot_lt_le in n.
∃ (a - x); split; try fourier.
intro.
destruct (Rlt_dec a x1).
intros.
assert False; try contradiction.
apply (Rgt_asym a x1); try assumption.
destruct H2; simpl in H3; unfold R_dist in H3.
assert ((x1 - x) ≤ Rabs (x1 - x)) by apply RRle_abs.
fourier.
assert (D_x no_cond x x1 ∧ dist R_met x1 x < x0 →
dist R_met (gl x1) (gl x) < eps) by (exact (H1 x1)).
apply Rnot_lt_le in n0.
repeat rewrite Hfl; try fourier.
intros; destruct H3.
apply H2.
split; try assumption.
fourier.
destruct H.
intros eps Heps.
rewrite H in |-*; clear x H.
destruct (Hl a eps); try assumption.
destruct (Hr a eps); try assumption.
destruct H; destruct H0.
∃ (Rmin x x0); split.
apply Rmin_pos; assumption.
intro x1; destruct (Rlt_dec x1 a).
repeat rewrite Hfl; try fourier.
assert (D_x no_cond a x1 ∧ dist R_met x1 a < x →
dist R_met (gl x1) (gl a) < eps) by (exact (H1 x1)).
intros; destruct H4.
apply H3.
split; try assumption.
assert (Rmin x x0 ≤ x) by exact (Rmin_l x x0).
fourier.
apply Rnot_lt_le in n.
repeat rewrite Hfr; try fourier.
assert (D_x no_cond a x1 ∧ dist R_met x1 a < x0 →
dist R_met (gr x1) (gr a) < eps) by (exact (H2 x1)).
intros; destruct H4.
apply H3.
split; try assumption.
assert (Rmin x x0 ≤ x0) by exact (Rmin_r x x0).
fourier.
intros eps Heps.
destruct (Hr x eps); try assumption.
destruct H0.
destruct (Rlt_dec x0 (x - a)).
∃ x0; split; try assumption.
intro.
destruct (Rlt_dec x1 a).
intros.
assert False; try contradiction.
apply (Rgt_asym a x1); try assumption.
destruct H2; simpl in H3; unfold R_dist in H3.
assert (x - x1 ≤ Rabs (x1 - x)).
rewrite Rabs_minus_sym; apply RRle_abs.
fourier.
repeat rewrite Hfr.
apply (H1 x1). fourier.
apply Rnot_lt_le; assumption.
∃ (x - a); split; try fourier.
intro.
destruct (Rlt_dec x1 a).
intros.
assert False; try contradiction.
apply (Rgt_asym a x1); try assumption.
destruct H2; simpl in H3; unfold R_dist in H3.
assert (x - x1 ≤ Rabs (x1 - x)).
rewrite Rabs_minus_sym; apply RRle_abs.
fourier.
apply Rnot_lt_le in n0.
repeat rewrite Hfr; try fourier.
apply Rnot_lt_le in n.
assert (D_x no_cond x x1 ∧ dist R_met x1 x < x0 →
dist R_met (gr x1) (gr x) < eps) by (exact (H1 x1)).
intros; destruct H3.
apply H2.
split; try assumption.
fourier.
Qed.
Lemma C0_sticking_one_pt_strong : ∀ f gl gr a,
(∀ x, x ≤ a → continuity_pt gl x) →
(∀ x, a ≤ x → continuity_pt gr x) →
(∀ x, x ≤ a → f x = gl x) →
(∀ x, a ≤ x → f x = gr x) →
continuity f.
Proof.
intros f gl gr a Hl Hr Hfl Hfr x.
destruct (Rtotal_order x a) as [|[]].
intros eps Heps.
destruct (Hl x (Rlt_le _ _ H) eps); try assumption.
destruct H0.
destruct (Rlt_dec x0 (a - x)).
∃ x0; split; try assumption.
intro.
destruct (Rlt_dec a x1).
intros.
assert False; try contradiction.
apply (Rgt_asym a x1); try assumption.
destruct H2; simpl in H3; unfold R_dist in H3.
assert ((x1 - x) ≤ Rabs (x1 - x)) by apply RRle_abs.
fourier.
repeat rewrite Hfl.
apply (H1 x1). fourier.
apply Rnot_lt_le; assumption.
apply Rnot_lt_le in n.
∃ (a - x); split; try fourier.
intro.
destruct (Rlt_dec a x1).
intros.
assert False; try contradiction.
apply (Rgt_asym a x1); try assumption.
destruct H2; simpl in H3; unfold R_dist in H3.
assert ((x1 - x) ≤ Rabs (x1 - x)) by apply RRle_abs.
fourier.
assert (D_x no_cond x x1 ∧ dist R_met x1 x < x0 →
dist R_met (gl x1) (gl x) < eps) by (exact (H1 x1)).
apply Rnot_lt_le in n0.
repeat rewrite Hfl; try fourier.
intros; destruct H3.
apply H2.
split; try assumption.
fourier.
intros eps Heps.
rewrite H in |-*; clear H x.
destruct (Hl a (Rle_refl a) eps); try assumption.
destruct (Hr a (Rle_refl a) eps); try assumption.
destruct H; destruct H0.
∃ (Rmin x x0); split.
apply Rmin_pos; assumption.
intro x1; destruct (Rlt_dec x1 a).
repeat rewrite Hfl; try fourier.
assert (D_x no_cond a x1 ∧ dist R_met x1 a < x →
dist R_met (gl x1) (gl a) < eps) by (exact (H1 x1)).
intros; destruct H4.
apply H3.
split; try assumption.
assert (Rmin x x0 ≤ x) by exact (Rmin_l x x0).
fourier.
apply Rnot_lt_le in n.
repeat rewrite Hfr; try fourier.
assert (D_x no_cond a x1 ∧ dist R_met x1 a < x0 →
dist R_met (gr x1) (gr a) < eps) by (exact (H2 x1)).
intros; destruct H4.
apply H3.
split; try assumption.
assert (Rmin x x0 ≤ x0) by exact (Rmin_r x x0).
fourier.
intros eps Heps.
destruct (Hr x (Rlt_le _ _ H) eps); try assumption.
destruct H0.
destruct (Rlt_dec x0 (x - a)).
∃ x0; split; try assumption.
intro.
destruct (Rlt_dec x1 a).
intros.
assert False; try contradiction.
apply (Rgt_asym a x1); try assumption.
destruct H2; simpl in H3; unfold R_dist in H3.
assert (x - x1 ≤ Rabs (x1 - x)).
rewrite Rabs_minus_sym; apply RRle_abs.
fourier.
repeat rewrite Hfr.
apply (H1 x1). fourier.
apply Rnot_lt_le; assumption.
∃ (x - a); split; try fourier.
intro.
destruct (Rlt_dec x1 a).
intros.
assert False; try contradiction.
apply (Rgt_asym a x1); try assumption.
destruct H2; simpl in H3; unfold R_dist in H3.
assert (x - x1 ≤ Rabs (x1 - x)).
rewrite Rabs_minus_sym; apply RRle_abs.
fourier.
apply Rnot_lt_le in n0.
repeat rewrite Hfr; try fourier.
apply Rnot_lt_le in n.
assert (D_x no_cond x x1 ∧ dist R_met x1 x < x0 →
dist R_met (gr x1) (gr x) < eps) by (exact (H1 x1)).
intros; destruct H3.
apply H2.
split; auto.
fourier.
Qed.
Lemma C0_sticking_two_pt : ∀ f gl gc gr a b,
a ≤ b →
continuity gl →
(∀ x, a ≤ x ≤ b → continuity_pt gc x) →
continuity gr →
(∀ x, x ≤ a → f x = gl x) →
(∀ x, a ≤ x ≤ b → f x = gc x) →
(∀ x, b ≤ x → f x = gr x) →
continuity f.
Proof.
intros f gl gc gr a b Hab Hl Hc Hr Hfl Hfc Hfr x.
destruct ((Rle_lt_or_eq_dec a b) Hab).
destruct (Rtotal_order x a).
intros eps Heps.
destruct (Hl x eps); try assumption.
destruct H0.
∃ (Rmin x0 (a-x)); split.
repeat (apply Rmin_pos); fourier.
intro.
destruct (Rlt_dec a x1).
intros.
assert False; try contradiction.
apply (Rgt_asym a x1); try assumption.
destruct H2; simpl in H3; unfold R_dist in H3.
assert ((x1 - x) ≤ Rabs (x1 - x)) by apply RRle_abs.
assert (Rmin x0 (a - x) ≤ a - x) by exact (Rmin_r x0 (a - x)).
fourier.
apply Rnot_lt_le in n.
repeat rewrite Hfl; try fourier.
assert (D_x no_cond x x1 ∧ dist R_met x1 x < x0 →
dist R_met (gl x1) (gl x) < eps) by (exact (H1 x1)).
intros; destruct H3.
apply H2.
split; try assumption.
assert (Rmin x0 (a - x) ≤ x0) by exact (Rmin_l x0 (a - x)).
fourier.
destruct H.
rewrite H in |-*; clear x H.
intros eps Heps.
destruct (Hl a eps); try assumption.
destruct (Hc a (conj (Rle_refl a) (Rlt_le _ _ r)) eps); try assumption.
destruct H; destruct H0.
∃ (Rmin x (Rmin x0 (b-a))); split.
repeat (apply Rmin_pos); fourier.
intro x1; destruct (Rlt_dec x1 a).
repeat rewrite Hfl; try fourier.
assert (D_x no_cond a x1 ∧ dist R_met x1 a < x →
dist R_met (gl x1) (gl a) < eps) by (exact (H1 x1)).
intros; destruct H4.
apply H3.
split; try assumption.
assert (Rmin x (Rmin x0 (b-a)) ≤ x) by exact (Rmin_l x (Rmin x0 (b-a))).
fourier.
apply Rnot_lt_le in n.
destruct (Rlt_dec b x1).
intros.
assert False; try contradiction.
apply (Rgt_asym b x1); try assumption.
destruct H3; simpl in H4; unfold R_dist in H4.
assert ((x1 - a) ≤ Rabs (x1 - a)) by apply RRle_abs.
assert (Rmin x (Rmin x0 (b-a)) ≤ (b-a)).
assert (Rmin x (Rmin x0 (b-a)) ≤ (Rmin x0 (b-a)))
by exact (Rmin_r x (Rmin x0 (b-a))).
assert ((Rmin x0 (b-a)) ≤ (b-a)) by exact (Rmin_r x0 (b-a)).
fourier.
fourier.
apply Rnot_lt_le in n0.
repeat rewrite Hfc; try split; try fourier.
assert (D_x no_cond a x1 ∧ dist R_met x1 a < x0 →
dist R_met (gc x1) (gc a) < eps) by (exact (H2 x1)).
intros; destruct H4.
apply H3.
split; try assumption.
assert (Rmin x (Rmin x0 (b-a)) ≤ x0).
assert (Rmin x (Rmin x0 (b-a)) ≤ (Rmin x0 (b-a)))
by exact (Rmin_r x (Rmin x0 (b-a))).
assert ((Rmin x0 (b-a)) ≤ x0) by exact (Rmin_l x0 (b-a)).
fourier.
fourier.
destruct (Rtotal_order x b).
intros eps Heps.
destruct (Hc x (conj (Rlt_le _ _ H) (Rlt_le _ _ H0)) eps); try assumption.
destruct H1.
∃ (Rmin (Rmin (x-a) (b-x)) x0); split.
repeat (apply Rmin_pos); fourier.
intro x1.
destruct (Rlt_dec x1 a).
intros.
assert False; try contradiction.
apply (Rgt_asym a x1); try assumption.
destruct H3; simpl in H4; unfold R_dist in H4.
assert (x - x1 ≤ Rabs (x1 - x)).
rewrite Rabs_minus_sym; apply RRle_abs.
assert ((Rmin (Rmin (x-a) (b-x)) x0) ≤ (x-a)).
assert ((Rmin (Rmin (x-a) (b-x)) x0) ≤ (Rmin (x-a) (b-x)))
by exact (Rmin_l (Rmin (x-a) (b-x)) x0).
assert ((Rmin (x-a) (b-x)) ≤ x-a) by exact (Rmin_l (x-a) (b-x)).
fourier.
fourier.
destruct (Rlt_dec b x1).
intros.
assert False; try contradiction.
apply (Rgt_asym x1 b); try assumption.
destruct H3; simpl in H4; unfold R_dist in H4.
assert (x1 - x ≤ Rabs (x1 - x)) by apply RRle_abs.
assert ((Rmin (Rmin (x-a) (b-x)) x0) ≤ (b-x)).
assert ((Rmin (Rmin (x-a) (b-x)) x0) ≤ (Rmin (x-a) (b-x)))
by exact (Rmin_l (Rmin (x-a) (b-x)) x0).
assert ((Rmin (x-a) (b-x)) ≤ b-x) by exact (Rmin_r (x-a) (b-x)).
fourier.
fourier.
apply Rnot_lt_le in n.
apply Rnot_lt_le in n0.
assert (D_x no_cond x x1 ∧ dist R_met x1 x < x0 →
dist R_met (gc x1) (gc x) < eps) by (exact (H2 x1)).
repeat rewrite Hfc; try split; try fourier.
intros; destruct H4.
apply H3.
split; try assumption.
assert ((Rmin (Rmin (x-a) (b-x)) x0) ≤ x0)
by exact (Rmin_r (Rmin (x-a) (b-x)) x0).
fourier.
destruct H0.
rewrite H0 in |-*; clear H x H0.
intros eps Heps.
destruct (Hc b (conj (Rlt_le _ _ r) (Rle_refl b)) eps); try assumption.
destruct (Hr b eps); try assumption.
destruct H; destruct H0.
∃ (Rmin x (Rmin x0 (b-a))); split.
repeat (apply Rmin_pos); fourier.
intro x1; destruct (Rlt_dec b x1).
repeat rewrite Hfr; try fourier.
assert (D_x no_cond b x1 ∧ dist R_met x1 b < x0 →
dist R_met (gr x1) (gr b) < eps) by (exact (H2 x1)).
intros; destruct H4.
apply H3.
split; try assumption.
assert (Rmin x (Rmin x0 (b-a)) ≤ x0).
assert (Rmin x (Rmin x0 (b-a)) ≤ (Rmin x0 (b-a)))
by exact (Rmin_r x (Rmin x0 (b-a))).
assert ((Rmin x0 (b-a)) ≤ x0) by exact (Rmin_l x0 (b-a)).
fourier.
fourier.
destruct (Rlt_dec x1 a).
intros.
assert False; try contradiction.
apply (Rgt_asym x1 a); try assumption.
destruct H3; simpl in H4; unfold R_dist in H4.
assert ((b - x1) ≤ Rabs (x1 - b)).
rewrite Rabs_minus_sym; apply RRle_abs.
assert (Rmin x (Rmin x0 (b-a)) ≤ (b-a)).
assert (Rmin x (Rmin x0 (b-a)) ≤ (Rmin x0 (b-a)))
by exact (Rmin_r x (Rmin x0 (b-a))).
assert ((Rmin x0 (b-a)) ≤ (b-a)) by exact (Rmin_r x0 (b-a)).
fourier.
fourier.
apply Rnot_lt_le in n.
apply Rnot_lt_le in n0.
repeat rewrite Hfc; try split; try fourier.
assert (D_x no_cond b x1 ∧ dist R_met x1 b < x →
dist R_met (gc x1) (gc b) < eps) by (exact (H1 x1)).
intros; destruct H4.
apply H3.
split; try assumption.
assert (Rmin x (Rmin x0 (b-a)) ≤ x) by exact (Rmin_l x (Rmin x0 (b-a))).
fourier.
intros eps Heps.
destruct (Hr x eps); try assumption.
destruct H1.
∃ (Rmin x0 (x - b)); split.
repeat (apply Rmin_pos); fourier.
intro.
destruct (Rlt_dec x1 b).
intros.
assert False; try contradiction.
apply (Rgt_asym b x1); try assumption.
destruct H3; simpl in H4; unfold R_dist in H4.
assert ((x - x1) ≤ Rabs (x1 - x)).
rewrite Rabs_minus_sym; apply RRle_abs.
assert (Rmin x0 (x - b) ≤ x - b) by exact (Rmin_r x0 (x - b)).
fourier.
apply Rnot_lt_le in n.
repeat rewrite Hfr; try fourier.
assert (D_x no_cond x x1 ∧ dist R_met x1 x < x0 →
dist R_met (gr x1) (gr x) < eps) by (exact (H2 x1)).
intros; destruct H4.
apply H3.
split; try assumption.
assert (Rmin x0 (x - b) ≤ x0) by exact (Rmin_l x0 (x - b)).
fourier.
rewrite e in *|-.
apply (C0_sticking_one_pt f gl gr b); assumption.
Qed.
Lemma C1_continuation_derive_continuous : ∀ d a b, a ≤ b →
(∀ c, a ≤ c ≤ b → continuity_pt d c) →
continuity (C1_continuation_derive d a b).
Proof.
intros d a b Hab Cd.
apply (C0_sticking_two_pt _ (fct_cte (d a)) d (fct_cte (d b)) a b Hab);
try (apply continuity_constant); auto; intros;
unfold C1_continuation_derive;
destruct (Rlt_dec x a);
destruct (Rle_dec x b); auto.
assert (x = a) by (apply Rle_antisym; auto; apply Rnot_lt_le; auto).
subst; trivial.
pose proof Rle_antisym a x (Rnot_lt_le _ _ n) H; subst.
apply (False_ind _ (n0 Hab)).
apply (False_ind _ (RIneq.Rle_not_lt _ _ (proj1 H) r)).
apply (False_ind _ (RIneq.Rle_not_lt _ _ (proj1 H) r)).
apply (False_ind _ (n0 (proj2 H))).
assert (x = b) by (apply Rle_antisym; auto; apply Rnot_lt_le; auto); subst.
apply (False_ind _ (RIneq.Rle_not_lt _ _ Hab r)).
apply False_ind; apply (RIneq.Rle_not_lt _ _ H).
apply Rlt_le_trans with a; auto.
assert (x = b) by (apply Rle_antisym; auto; apply Rnot_lt_le; auto); subst.
trivial.
Qed.
Lemma prolongement_C1_C1 : ∀ (f d : R → R) (a b : R),
a ≤ b →
(∀ c, a ≤ c ≤ b → derivable_pt_abs f c (d c)) →
(∀ c, a ≤ c ≤ b → continuity_pt d c) →
{g : C1_fun |
(∀ c : R, a ≤ c ≤ b → f c = g c) ∧
(∀ c : R, a ≤ c ≤ b → d c = derive g (diff0 g) c)}.
Proof.
intros f d a b Hab Hder Hcont.
pose proof (prolongement_C1_derivable f d a b Hab Hder) as [diff0 Heq].
pose proof (C1_continuation_derive_continuous d a b Hab Hcont) as cont.
assert(c1 : continuity (derive (C1_continuation f a b d) diff0)).
intros x eps Heps.
destruct (cont x eps Heps) as [alpha [Halpha1 Halpha2]].
∃ alpha.
split.
assumption.
intros.
do 2 rewrite Heq; intuition.
∃ (mkC1 c1).
split.
intros x Hx.
rewrite <- (C1_continuation_eq f a b d x Hx);
reflexivity.
intros x Hx.
rewrite <- (C1_continuation_derive_eq a b d x Hx), Heq;
reflexivity.
Qed.
End Rint_C1.
Create HintDb Rcont.
Hint Resolve continuity_pt_plus : Rcont.
Hint Resolve continuity_pt_mult : Rcont.
Hint Resolve continuity_pt_minus : Rcont.
Hint Resolve continuity_pt_opp : Rcont.
Hint Resolve continuity_pt_const : Rcont.
Hint Resolve continuity_pt_inv : Rcont.
Hint Resolve continuity_pt_div : Rcont.
Hint Resolve continuity_pt_comp : Rcont.
Hint Resolve continuity_pt_sqrt : Rcont.
Hint Resolve continuity_pt_constant : Rcont.
Hint Resolve derivable_continuous_pt : Rcont.
Hint Resolve continuity_plus : Rcont.
Hint Resolve continuity_mult : Rcont.
Hint Resolve continuity_minus : Rcont.
Hint Resolve continuity_opp : Rcont.
Hint Resolve continuity_const : Rcont.
Hint Resolve continuity_inv : Rcont.
Hint Resolve continuity_div : Rcont.
Hint Resolve continuity_constant : Rcont.
Hint Resolve continuity_comp : Rcont.
Hint Resolve derivable_continuous : Rcont.
Hint Resolve derivable_pt_plus : Rcont.
Hint Resolve derivable_pt_mult : Rcont.
Hint Resolve derivable_pt_minus: Rcont.
Hint Resolve derivable_pt_opp : Rcont.
Hint Resolve derivable_pt_const : Rcont.
Hint Resolve derivable_pt_inv : Rcont.
Hint Resolve derivable_pt_div : Rcont.
Hint Resolve derivable_pt_comp : Rcont.
Hint Resolve derivable_pt_sqrt : Rcont.
Hint Resolve derivable_pt_exp : Rcont.
Hint Resolve derivable_pt_id : Rcont.
Hint Resolve derivable_pt_pow : Rcont.
Hint Resolve derivable_pt_cosh : Rcont.
Hint Resolve derivable_plus : Rcont.
Hint Resolve derivable_mult : Rcont.
Hint Resolve derivable_minus : Rcont.
Hint Resolve derivable_opp : Rcont.
Hint Resolve derivable_const : Rcont.
Hint Resolve derivable_inv : Rcont.
Hint Resolve derivable_div : Rcont.
Hint Resolve derivable_comp : Rcont.
Hint Resolve derivable_continuous : Rcont.
Hint Resolve derivable_cos : Rcont.
Hint Resolve derivable_sin : Rcont.
Hint Resolve derivable_exp : Rcont.
Hint Resolve derivable_id : Rcont.
Hint Resolve derivable_id : Rcont.
Hint Resolve derivable_pow : Rcont.
Hint Resolve derivable_cosh : Rcont.
Hint Resolve derivable_pt_lim_sin : Rcont.
Hint Resolve derivable_pt_lim_cos : Rcont.
Hint Resolve derivable_pt_lim_sqrt : Rcont.
Hint Resolve derivable_pt_lim_ln : Rcont.
Hint Resolve derivable_pt_lim_exp : Rcont.
Hint Resolve derivable_pt_lim_plus: Rcont.
Hint Resolve derivable_pt_lim_mult: Rcont.
Hint Resolve derivable_pt_lim_minus : Rcont.
Hint Resolve derivable_pt_lim_opp : Rcont.
Hint Resolve derivable_pt_lim_const : Rcont.
Hint Resolve derivable_pt_lim_id : Rcont.
Hint Resolve derivable_pt_lim_div : Rcont.
Hint Resolve derivable_pt_lim_comp : Rcont.
Hint Resolve derivable_pt_lim_pow : Rcont.
Hint Resolve derivable_pt_lim_power : Rcont.
Hint Resolve derivable_pt_lim_id : Rcont.
Hint Resolve derivable_pt_lim_cosh : Rcont.