proposition: Lemma antiderivative_P2 : forall (f F0 F1:R -> R) (a b c:R), antiderivative f F0 a b -> antiderivative f F1 b c -> antiderivative f (fun x:R => match Rle_dec x b with | left _ => F0 x | right _ => F1 x + (F0 b - F1 b) end) a c.
proof: Proof. intros; destruct H as (H,H1), H0 as (H0,H2); split. 2: apply Rle_trans with b; assumption. intros x (H3,H4); destruct (total_order_T x b) as [[Hlt|Heq]|Hgt]. - assert (H5 : a <= x <= b). { split; [ assumption | left; assumption ]. } destruct (H _ H5) as (x0,H6). assert (H7 : derivable_pt_lim (fun x:R => match Rle_dec x b with | left _ => F0 x | right _ => F1 x + (F0 b - F1 b) end) x (f x)). { unfold derivable_pt_lim. intros eps H9. assert (H7 : derive_pt F0 x x0 = f x) by (symmetry; assumption). destruct (derive_pt_eq_1 F0 x (f x) x0 H7 _ H9) as (x1,H10); set (D := Rmin x1 (b - x)). assert (H11 : 0 < D). { unfold D, Rmin; case (Rle_dec x1 (b - x)); intro. { apply (cond_pos x1). } apply Rlt_0_minus; assumption. } exists (mkposreal _ H11); intros h H12 H13. case (Rle_dec x b) as [|[]]. 2:left;assumption. case (Rle_dec (x + h) b) as [|[]]. { apply H10. { assumption. } apply Rlt_le_trans with D; [ assumption | unfold D; apply Rmin_l ]. } left; apply Rlt_le_trans with (x + D). { apply Rplus_lt_compat_l; apply Rle_lt_trans with (Rabs h). { apply RRle_abs. } apply H13. } apply Rplus_le_reg_l with (- x); rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l; rewrite Rplus_comm; unfold D; apply Rmin_r. } assert (H8 : derivable_pt (fun x:R => match Rle_dec x b with | left _ => F0 x | right _ => F1 x + (F0 b - F1 b) end) x). { unfold derivable_pt; exists (f x); apply H7. } exists H8; symmetry ; apply derive_pt_eq_0; apply H7. - assert (H5 : a <= x <= b). { split; [ assumption | right; assumption ]. } assert (H6 : b <= x <= c). { split; [ right; symmetry ; assumption | assumption ]. } elim (H _ H5); elim (H0 _ H6); intros; assert (H9 : derive_pt F0 x x1 = f x). { symmetry ; assumption. } assert (H10 : derive_pt F1 x x0 = f x). { symmetry ; assumption. } assert (H11 := derive_pt_eq_1 F0 x (f x) x1 H9); assert (H12 := derive_pt_eq_1 F1 x (f x) x0 H10); assert (H13 : derivable_pt_lim (fun x:R => match Rle_dec x b with | left _ => F0 x | right _ => F1 x + (F0 b - F1 b) end) x (f x)). { unfold derivable_pt_lim; unfold derivable_pt_lim in H11, H12; intros; elim (H11 _ H13); elim (H12 _ H13); intros; set (D := Rmin x2 x3); assert (H16 : 0 < D). { unfold D; unfold Rmin; case (Rle_dec x2 x3); intro. { apply (cond_pos x2). } apply (cond_pos x3). } exists (mkposreal _ H16); intros; case (Rle_dec x b) as [|[]]. 2:right;assumption. case (Rle_dec (x + h) b); intro. { apply H15. { assumption. } apply Rlt_le_trans with D; [ assumption | unfold D; apply Rmin_r ]. } replace (F1 (x + h) + (F0 b - F1 b) - F0 x) with (F1 (x + h) - F1 x). { apply H14. { assumption. } apply Rlt_le_trans with D; [ assumption | unfold D; apply Rmin_l ]. } rewrite Heq; ring. } assert (H14 : derivable_pt (fun x:R => match Rle_dec x b with | left _ => F0 x | right _ => F1 x + (F0 b - F1 b) end) x). { unfold derivable_pt; exists (f x); apply H13. } exists H14; symmetry ; apply derive_pt_eq_0; apply H13. - assert (H5 : b <= x <= c). { split; [ left; assumption | assumption ]. } assert (H6 := H0 _ H5); elim H6; clear H6; intros; assert (H7 : derivable_pt_lim (fun x:R => match Rle_dec x b with | left _ => F0 x | right _ => F1 x + (F0 b - F1 b) end) x (f x)). { unfold derivable_pt_lim; assert (H7 : derive_pt F1 x x0 = f x). { symmetry ; assumption. } assert (H8 := derive_pt_eq_1 F1 x (f x) x0 H7); unfold derivable_pt_lim in H8; intros; elim (H8 _ H9); intros; set (D := Rmin x1 (x - b)); assert (H11 : 0 < D). { unfold D; unfold Rmin; case (Rle_dec x1 (x - b)); intro. { apply (cond_pos x1). } apply Rlt_0_minus; assumption. } exists (mkposreal _ H11); intros; destruct (Rle_dec x b) as [Hle|Hnle]. { elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle Hgt)). } destruct (Rle_dec (x + h) b) as [Hle'|Hnle']. { cut (b < x + h). { intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle' H14)). } apply Rplus_lt_reg_l with (- h - b); replace (- h - b + b) with (- h); [ idtac | ring ]; replace (- h - b + (x + h)) with (x - b); [ idtac | ring ]; apply Rle_lt_trans with (Rabs h). { rewrite <- Rabs_Ropp; apply RRle_abs. } apply Rlt_le_trans with D. { apply H13. } unfold D; apply Rmin_r. } replace (F1 (x + h) + (F0 b - F1 b) - (F1 x + (F0 b - F1 b))) with (F1 (x + h) - F1 x); [ idtac | ring ]; apply H10. { assumption. } apply Rlt_le_trans with D. { assumption. } unfold D; apply Rmin_l. } assert (H8 : derivable_pt (fun x:R => match Rle_dec x b with | left _ => F0 x | right _ => F1 x + (F0 b - F1 b) end) x). { unfold derivable_pt; exists (f x); apply H7. } exists H8; symmetry ; apply derive_pt_eq_0; apply H7. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis