Library Coqtail.Reals.Rintegral.Riemann_integrable
Require Import Max.
Require Import Reals.
Require Import Fourier.
Require Import RiemannInt.
Require Import Rfunction_classes_def.
Require Import Rextensionality.
Open Scope R_scope.
Section Copy_stdlib.
Lemma Riemann_integrable_opp_bound :
∀ (f:R → R) (a b:R),
Riemann_integrable f a b → Riemann_integrable f b a.
Proof.
apply RiemannInt_P1.
Qed.
Definition RinvN (N:nat) : posreal := mkposreal _ (RinvN_pos N).
Lemma Riemann_integrable_PI :
∀ (f:R → R) (a b:R) (pr1 pr2:Riemann_integrable f a b),
RiemannInt pr1 = RiemannInt pr2.
Proof.
apply RiemannInt_P5.
Qed.
Lemma Riemann_integrable_continuity :
∀ (f:R → R) (a b:R),
a < b →
(∀ x:R, a ≤ x ≤ b → continuity_pt f x) → Riemann_integrable f a b.
Proof.
apply RiemannInt_P6.
Qed.
Lemma Riemann_integrable_singleton : ∀ (f:R → R) (a:R), Riemann_integrable f a a.
Proof.
apply RiemannInt_P7.
Qed.
Lemma Riemann_integrable_continuity_gen :
∀ (f:R → R) (a b:R),
a ≤ b →
(∀ x:R, a ≤ x ≤ b → continuity_pt f x) → Riemann_integrable f a b.
Proof.
apply continuity_implies_RiemannInt.
Qed.
Lemma RiemannInt_bound_exchange :
∀ (f:R → R) (a b:R) (pr1:Riemann_integrable f a b)
(pr2:Riemann_integrable f b a), RiemannInt pr1 = - RiemannInt pr2.
Proof.
apply RiemannInt_P8.
Qed.
Lemma RiemannInt_bound_exchange_1 :
∀ (f : R → R) (a b : R) (pr1 : Riemann_integrable f a b),
RiemannInt pr1 = - RiemannInt (Riemann_integrable_opp_bound f a b pr1).
Proof.
intros. rewrite (RiemannInt_bound_exchange f a b pr1 (Riemann_integrable_opp_bound f a b pr1)).
reflexivity.
Qed.
Lemma RiemannInt_singleton :
∀ (f:R → R) (a:R) (pr:Riemann_integrable f a a), RiemannInt pr = 0.
Proof.
apply RiemannInt_P9.
Qed.
Lemma Riemann_integrable_linear :
∀ (f g:R → R) (a b l:R),
Riemann_integrable f a b →
Riemann_integrable g a b →
Riemann_integrable (fun x:R ⇒ f x + l × g x) a b.
Proof.
apply RiemannInt_P10.
Qed.
Lemma RiemannInt_linear :
∀ (f g:R → R) (a b l:R) (pr1:Riemann_integrable f a b)
(pr2:Riemann_integrable g a b)
(pr3:Riemann_integrable (fun x:R ⇒ f x + l × g x) a b),
RiemannInt pr3 = RiemannInt pr1 + l × RiemannInt pr2.
Proof.
apply RiemannInt_P13.
Qed.
Lemma Riemann_integrable_constant : ∀ a b c:R, Riemann_integrable (fct_cte c) a b.
Proof.
apply RiemannInt_P14.
Qed.
Lemma RiemannInt_constant :
∀ (a b c:R) (pr:Riemann_integrable (fct_cte c) a b),
RiemannInt pr = c × (b - a).
Proof.
apply RiemannInt_P15.
Qed.
Lemma Riemann_integrable_Rabs :
∀ (f:R → R) (a b:R),
Riemann_integrable f a b → Riemann_integrable (fun x:R ⇒ Rabs (f x)) a b.
Proof.
apply RiemannInt_P16.
Qed.
Lemma RiemannInt_le_Rabs :
∀ (f:R → R) (a b:R) (pr1:Riemann_integrable f a b)
(pr2:Riemann_integrable (fun x:R ⇒ Rabs (f x)) a b),
a ≤ b → Rabs (RiemannInt pr1) ≤ RiemannInt pr2.
Proof.
apply RiemannInt_P17.
Qed.
Lemma RiemannInt_ext :
∀ (f g:R → R) (a b:R) (pr1:Riemann_integrable f a b)
(pr2:Riemann_integrable g a b),
a ≤ b →
(∀ x:R, a < x < b → f x = g x) → RiemannInt pr1 = RiemannInt pr2.
Proof.
apply RiemannInt_P18.
Qed.
Lemma RiemannInt_le_ext :
∀ (f g:R → R) (a b:R) (pr1:Riemann_integrable f a b)
(pr2:Riemann_integrable g a b),
a ≤ b →
(∀ x:R, a < x < b → f x ≤ g x) → RiemannInt pr1 ≤ RiemannInt pr2.
Proof.
apply RiemannInt_P19.
Qed.
Lemma RiemannInt_primitive :
∀ (f:R → R) (a b:R) (h:a ≤ b)
(pr:∀ x:R, a ≤ x → x ≤ b → Riemann_integrable f a x)
(pr0:Riemann_integrable f a b),
RiemannInt pr0 = primitive h pr b - primitive h pr a.
Proof.
apply RiemannInt_P20.
Qed.
Lemma Riemann_integrable_included_left :
∀ (f:R → R) (a b c:R),
Riemann_integrable f a b → a ≤ c ≤ b → Riemann_integrable f a c.
Proof.
apply RiemannInt_P22.
Qed.
Lemma Riemann_integrable_included_right :
∀ (f:R → R) (a b c:R),
Riemann_integrable f a b → a ≤ c ≤ b → Riemann_integrable f c b.
Proof.
apply RiemannInt_P23.
Qed.
Lemma Riemann_integrable_Chasles :
∀ (f:R → R) (a b c:R),
Riemann_integrable f a b →
Riemann_integrable f b c → Riemann_integrable f a c.
Proof.
apply RiemannInt_P24.
Qed.
Lemma RiemannInt_Chasles :
∀ (f:R → R) (a b c:R) (pr1:Riemann_integrable f a b)
(pr2:Riemann_integrable f b c) (pr3:Riemann_integrable f a c),
RiemannInt pr1 + RiemannInt pr2 = RiemannInt pr3.
Proof.
apply RiemannInt_P26.
Qed.
Lemma derivable_primitive :
∀ (f:R → R) (a b x:R) (h:a ≤ b)
(C0:∀ x:R, a ≤ x ≤ b → continuity_pt f x),
a ≤ x ≤ b → derivable_pt_lim (primitive h (FTC_P1 h C0)) x (f x).
Proof.
apply RiemannInt_P28.
Qed.
End Copy_stdlib.
Lemma RiemannInt_integrable_eq_compat : ∀ f g a b, (∀ x, f x = g x) →
Riemann_integrable f a b → Riemann_integrable g a b.
intros f g a b H X eps.
elim X with eps;intros x p; ∃ x.
elim p; intros x0 [p01 p02]; ∃ x0.
split; intros; [ rewrite <- (H t); apply p01 | ]; assumption.
Qed.
Lemma RiemannInt_integrable_minus : ∀ (f g:R → R) (a b:R)
(prf:Riemann_integrable f a b)
(prg:Riemann_integrable g a b), (Riemann_integrable (fun x ⇒ f x - g x) a b).
Proof.
intros.
apply RiemannInt_integrable_eq_compat with (fun x ⇒ f x + (-1) × g x); [intros; ring|].
apply RiemannInt_P10; assumption.
Qed.
Lemma RiemannInt_minus :
∀ (f g:R → R) (a b:R)
(prf:Riemann_integrable f a b)
(prg:Riemann_integrable g a b)
(prfg:Riemann_integrable (fun x:R ⇒ f x - g x) a b),
a≤b → RiemannInt prfg = RiemannInt prf - RiemannInt prg.
Proof.
intros.
assert (REW: ∀ x y, x - y = x + (-1)*y) by (intros; ring); rewrite REW; clear REW.
pose proof (RiemannInt_P10 (-1) prf prg) as prfg'.
replace (RiemannInt prfg) with (RiemannInt prfg').
apply RiemannInt_P13.
apply RiemannInt_P18 ; intuition.
ring.
Qed.
Lemma RiemannInt_minus_1 :
∀ (f g:R → R) (a b:R)
(prf:Riemann_integrable f a b)
(prg:Riemann_integrable g a b),
a≤b → RiemannInt prf - RiemannInt prg = RiemannInt (RiemannInt_integrable_minus f g a b prf prg).
Proof.
intros. rewrite (RiemannInt_minus _ _ _ _ prf prg) ; intuition.
Qed.
Lemma RiemannInt_linear_1 :
∀ (f g:R → R) (a b l:R) (pr1:Riemann_integrable f a b)
(pr2:Riemann_integrable g a b),
RiemannInt pr1 + l × RiemannInt pr2 = RiemannInt (Riemann_integrable_linear f g a b l pr1 pr2).
Proof.
intros. symmetry. apply RiemannInt_linear.
Qed.
Lemma Riemann_integrable_add :
∀ (f g:R → R) (a b:R) (pr1:Riemann_integrable f a b)
(pr2:Riemann_integrable g a b),
Riemann_integrable (f + g)%F a b.
Proof.
intros. apply RiemannInt_integrable_eq_compat with (fun x ⇒ f x + 1 × g x).
intros. unfold plus_fct. ring. apply Riemann_integrable_linear ; assumption.
Qed.
Lemma RiemannInt_add :
∀ (f g:R → R) (a b:R) (prf:Riemann_integrable f a b)
(prg:Riemann_integrable g a b) (prfg:Riemann_integrable (f + g)%F a b), a ≤ b →
RiemannInt prf + RiemannInt prg = RiemannInt prfg.
Proof.
intros.
pose proof (RiemannInt_P10 1 prf prg) as prfg'.
replace (RiemannInt prfg) with (RiemannInt prfg').
replace (RiemannInt prg) with (1 × RiemannInt prg) by ring.
symmetry. apply RiemannInt_P13.
apply RiemannInt_P18 ; intuition. unfold plus_fct. ring.
Qed.
Lemma RiemannInt_add_1 :
∀ (f g:R → R) (a b:R) (prf:Riemann_integrable f a b)
(prg:Riemann_integrable g a b), a ≤ b →
RiemannInt prf + RiemannInt prg = RiemannInt (Riemann_integrable_add f g a b prf prg).
Proof.
intros.
apply RiemannInt_add. apply H.
Qed.
Hint Rewrite RiemannInt_minus_1 : Rintegrals.
Hint Rewrite RiemannInt_linear_1 : Rintegrals.
Hint Rewrite RiemannInt_add_1 : Rintegrals.
Lemma continuity_RiemannInt_1 :
∀ (f:R → R) (a b:R),
(∀ x:R, a ≤ x ≤ b ∨ b ≤ x ≤ a → continuity_pt f x) → Riemann_integrable f a b.
Proof.
intros; case (total_order_T a b); intro.
elim s ; intro.
apply RiemannInt_P6. assumption. intros. apply H. intuition.
subst; apply RiemannInt_P7.
apply Riemann_integrable_opp_bound. apply RiemannInt_P6. intuition.
intros. apply H. intuition.
Qed.
Lemma RiemannInt_derivable_pt_lim :
∀ (f:R → R) (a x:R)
(pr:∀ x y:R, Riemann_integrable f x y)
(Hcont:continuity_pt f x),
derivable_pt_lim (fun t1 ⇒ @RiemannInt f a t1 (pr a t1)) x (f x).
Proof.
intros.
unfold derivable_pt_lim. intros.
assert (H4:0 < eps / 2) by fourier.
destruct (Hcont _ H4) as [x1 [Hcont1 Hcont2]].
∃ (mkposreal _ Hcont1). intros.
rewrite <- (RiemannInt_Chasles f a x (x+h) (pr a x) (pr x (x + h)) (pr a (x + h))).
ring_simplify ((RiemannInt (pr a x) + RiemannInt (pr x (x + h)) - RiemannInt (pr a x))).
replace (f x) with (RiemannInt (Riemann_integrable_constant x (x + h) (f x)) / h)
by (rewrite RiemannInt_constant; field; assumption).
replace
(RiemannInt (pr x (x + h)) / h - RiemannInt (Riemann_integrable_constant x (x + h) (f x)) / h)
with ((RiemannInt (pr x (x + h)) + (-1) × RiemannInt (Riemann_integrable_constant x (x + h) (f x))) / h)
by (unfold Rdiv ; ring).
rewrite RiemannInt_linear_1.
unfold Rdiv in |- *; rewrite Rabs_mult; case (Rle_dec x (x + h)); intro.
apply Rle_lt_trans with
(RiemannInt
(Riemann_integrable_Rabs _ _ _
(Riemann_integrable_linear _ _ _ _ (-1) (pr x (x + h)) (Riemann_integrable_constant x (x + h) (f x)))) ×
Rabs (/ h)).
do 2 rewrite <- (Rmult_comm (Rabs (/ h))); apply Rmult_le_compat_l.
apply Rabs_pos. apply RiemannInt_le_Rabs. assumption.
apply Rle_lt_trans with
(RiemannInt (Riemann_integrable_constant x (x + h) (eps / 2)) × Rabs (/ h)).
do 2 rewrite <- (Rmult_comm (Rabs (/ h))); apply Rmult_le_compat_l.
apply Rabs_pos.
apply RiemannInt_P19; try assumption.
intros; replace (f x0 + -1 × fct_cte (f x) x0) with (f x0 - f x) by (intros ; unfold fct_cte ; simpl ; ring).
unfold fct_cte.
assert (x ≠ x0) by (intro ; subst ; destruct H2 ; fourier).
left. simpl in ×. unfold R_dist in ×. apply Hcont2.
unfold D_x, no_cond. repeat split. assumption.
eapply Rlt_trans ; [|apply H1].
assert (0 < x0 - x < h) by (intuition ; fourier).
rewrite Rabs_pos_eq. rewrite Rabs_pos_eq. intuition.
apply Rle_trans with (x0 - x) ; intuition. intuition.
rewrite RiemannInt_constant.
rewrite Rmult_assoc; replace ((x + h - x) × Rabs (/ h)) with 1.
ring_simplify. fourier.
rewrite Rabs_right.
replace (x + h - x) with h; [ idtac | ring ].
apply Rinv_r_sym.
assumption.
apply Rle_ge; left; apply Rinv_0_lt_compat.
elim r; intro.
apply Rplus_lt_reg_r with x; rewrite Rplus_0_r; assumption.
elim H0; symmetry in |- *; apply Rplus_eq_reg_l with x; rewrite Rplus_0_r;
assumption.
apply Rle_lt_trans with
(RiemannInt
(Riemann_integrable_Rabs _ _ _
(Riemann_integrable_opp_bound _ _ _
(Riemann_integrable_linear f (fct_cte (f x)) x
(x + h) (-1) (pr x (x + h))
(Riemann_integrable_constant x (x + h) (f x))))) ×
Rabs (/ h)).
do 2 rewrite <- (Rmult_comm (Rabs (/ h))); apply Rmult_le_compat_l.
apply Rabs_pos.
rewrite RiemannInt_bound_exchange_1.
rewrite Rabs_Ropp.
apply RiemannInt_le_Rabs. left. intuition.
apply Rle_lt_trans with
(RiemannInt (Riemann_integrable_constant (x + h) x (eps / 2)) × Rabs (/ h)).
do 2 rewrite <- (Rmult_comm (Rabs (/ h))); apply Rmult_le_compat_l.
apply Rabs_pos.
apply RiemannInt_le_ext.
auto with real.
intros. unfold fct_cte in ×. ring_simplify (-1 × f x).
intros; replace (f x0 + -1 × fct_cte (f x) x0) with (f x0 - f x).
unfold fct_cte in |- *; case (Req_dec x x0); intro.
rewrite H3. ring_simplify (f x0 + - f x0). rewrite Rabs_R0; left;
assumption.
left; simpl in Hcont2 ; ring_simplify (f x0 + -1 × f x) ; apply Hcont2.
repeat split.
assumption.
unfold R_dist. rewrite Rabs_left.
apply Rplus_lt_reg_r with (x0 - x1); replace (x0 - x1 + x1) with x0;
[ idtac | ring ].
replace (x0 - x1 + - (x0 - x)) with (x - x1); [ idtac | ring ].
apply Rle_lt_trans with (x + h).
unfold Rminus in |- *; apply Rplus_le_compat_l; apply Ropp_le_cancel.
rewrite Ropp_involutive; apply Rle_trans with (Rabs h).
rewrite <- Rabs_Ropp; apply RRle_abs.
apply Rle_trans with x1;
[ left; assumption | idtac ]. right. reflexivity.
elim H2; intros; assumption.
apply Rplus_lt_reg_r with x; rewrite Rplus_0_r;
replace (x + (x0 - x)) with x0; [ elim H2; intros; assumption | ring ].
unfold fct_cte in |- *; ring.
rewrite RiemannInt_P15.
rewrite Rmult_assoc; replace ((x - (x + h)) × Rabs (/ h)) with 1.
rewrite Rmult_1_r; unfold Rdiv in |- *; apply Rmult_lt_reg_l with 2;
[ prove_sup0
| rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
rewrite <- Rinv_r_sym;
[ rewrite Rmult_1_l; pattern eps at 1 in |- *; rewrite <- Rplus_0_r;
rewrite double; apply Rplus_lt_compat_l; assumption
| discrR ] ].
rewrite Rabs_left.
replace (x - (x + h)) with (- h); [ idtac | ring ].
rewrite Ropp_mult_distr_l_reverse; rewrite Ropp_mult_distr_r_reverse;
rewrite Ropp_involutive; apply Rinv_r_sym.
assumption.
apply Rinv_lt_0_compat.
assert (H8 : x + h < x).
auto with real.
apply Rplus_lt_reg_r with x; rewrite Rplus_0_r; assumption.
Qed.
Lemma RiemannInt_derivable_pt :
∀ (f:R → R) (a x:R)
(pr:∀ x y:R, Riemann_integrable f x y)
(Hcont:continuity_pt f x),
derivable_pt (fun t1 ⇒ @RiemannInt f a t1 (pr a t1)) x.
Proof.
intros.
unfold derivable_pt, derivable_pt_abs.
∃ (f x). apply RiemannInt_derivable_pt_lim.
assumption.
Qed.
Lemma derive_pt_RiemannInt :
∀ (f:R → R) (a x:R)
(pr:∀ x y:R, Riemann_integrable f x y)
(Hcont:continuity_pt f x),
derive_pt (fun t ⇒ RiemannInt (pr a t)) x (RiemannInt_derivable_pt f a x pr Hcont) = f x.
Proof.
intros.
rewrite derive_pt_eq. apply RiemannInt_derivable_pt_lim.
apply Hcont.
Qed.
Lemma derive_pt_RiemannInt_1 :
∀ (f:R → R) (a x:R)
(pr:∀ x y:R, Riemann_integrable f x y)
(Hcont:continuity_pt f x) H1,
derive_pt (fun t ⇒ RiemannInt (pr a t)) x H1 = f x.
Proof.
intros.
rewrite derive_pt_eq. apply RiemannInt_derivable_pt_lim.
apply Hcont.
Qed.
Lemma derivable_pt_continuity_Riemann_implies_C1 :
∀ f t0 (pr:∀ t t0, Riemann_integrable f t t0), continuity f →
C 1 (fun t ⇒ RiemannInt (pr t0 t)).
Proof.
intros.
assert (derivable (fun t ⇒ RiemannInt (pr t0 t))).
intro. apply RiemannInt_derivable_pt. apply H.
apply (C_S _ _ H0).
apply C_0. apply continuity_ext with f.
intro. unfold derive. rewrite derive_pt_RiemannInt_1.
reflexivity.
apply H. apply H.
Qed.
Lemma RiemannInt_continuity : ∀ a t0 (Hconta : continuity a) (Ha : ∀ t0 t,
Riemann_integrable a t0 t), continuity (fun t ⇒ RiemannInt (Ha t0 t)).
Proof.
intros.
apply derivable_continuous. unfold derivable. intros. apply RiemannInt_derivable_pt.
apply Hconta.
Qed.
Require Import Reals.
Require Import Fourier.
Require Import RiemannInt.
Require Import Rfunction_classes_def.
Require Import Rextensionality.
Open Scope R_scope.
Section Copy_stdlib.
Lemma Riemann_integrable_opp_bound :
∀ (f:R → R) (a b:R),
Riemann_integrable f a b → Riemann_integrable f b a.
Proof.
apply RiemannInt_P1.
Qed.
Definition RinvN (N:nat) : posreal := mkposreal _ (RinvN_pos N).
Lemma Riemann_integrable_PI :
∀ (f:R → R) (a b:R) (pr1 pr2:Riemann_integrable f a b),
RiemannInt pr1 = RiemannInt pr2.
Proof.
apply RiemannInt_P5.
Qed.
Lemma Riemann_integrable_continuity :
∀ (f:R → R) (a b:R),
a < b →
(∀ x:R, a ≤ x ≤ b → continuity_pt f x) → Riemann_integrable f a b.
Proof.
apply RiemannInt_P6.
Qed.
Lemma Riemann_integrable_singleton : ∀ (f:R → R) (a:R), Riemann_integrable f a a.
Proof.
apply RiemannInt_P7.
Qed.
Lemma Riemann_integrable_continuity_gen :
∀ (f:R → R) (a b:R),
a ≤ b →
(∀ x:R, a ≤ x ≤ b → continuity_pt f x) → Riemann_integrable f a b.
Proof.
apply continuity_implies_RiemannInt.
Qed.
Lemma RiemannInt_bound_exchange :
∀ (f:R → R) (a b:R) (pr1:Riemann_integrable f a b)
(pr2:Riemann_integrable f b a), RiemannInt pr1 = - RiemannInt pr2.
Proof.
apply RiemannInt_P8.
Qed.
Lemma RiemannInt_bound_exchange_1 :
∀ (f : R → R) (a b : R) (pr1 : Riemann_integrable f a b),
RiemannInt pr1 = - RiemannInt (Riemann_integrable_opp_bound f a b pr1).
Proof.
intros. rewrite (RiemannInt_bound_exchange f a b pr1 (Riemann_integrable_opp_bound f a b pr1)).
reflexivity.
Qed.
Lemma RiemannInt_singleton :
∀ (f:R → R) (a:R) (pr:Riemann_integrable f a a), RiemannInt pr = 0.
Proof.
apply RiemannInt_P9.
Qed.
Lemma Riemann_integrable_linear :
∀ (f g:R → R) (a b l:R),
Riemann_integrable f a b →
Riemann_integrable g a b →
Riemann_integrable (fun x:R ⇒ f x + l × g x) a b.
Proof.
apply RiemannInt_P10.
Qed.
Lemma RiemannInt_linear :
∀ (f g:R → R) (a b l:R) (pr1:Riemann_integrable f a b)
(pr2:Riemann_integrable g a b)
(pr3:Riemann_integrable (fun x:R ⇒ f x + l × g x) a b),
RiemannInt pr3 = RiemannInt pr1 + l × RiemannInt pr2.
Proof.
apply RiemannInt_P13.
Qed.
Lemma Riemann_integrable_constant : ∀ a b c:R, Riemann_integrable (fct_cte c) a b.
Proof.
apply RiemannInt_P14.
Qed.
Lemma RiemannInt_constant :
∀ (a b c:R) (pr:Riemann_integrable (fct_cte c) a b),
RiemannInt pr = c × (b - a).
Proof.
apply RiemannInt_P15.
Qed.
Lemma Riemann_integrable_Rabs :
∀ (f:R → R) (a b:R),
Riemann_integrable f a b → Riemann_integrable (fun x:R ⇒ Rabs (f x)) a b.
Proof.
apply RiemannInt_P16.
Qed.
Lemma RiemannInt_le_Rabs :
∀ (f:R → R) (a b:R) (pr1:Riemann_integrable f a b)
(pr2:Riemann_integrable (fun x:R ⇒ Rabs (f x)) a b),
a ≤ b → Rabs (RiemannInt pr1) ≤ RiemannInt pr2.
Proof.
apply RiemannInt_P17.
Qed.
Lemma RiemannInt_ext :
∀ (f g:R → R) (a b:R) (pr1:Riemann_integrable f a b)
(pr2:Riemann_integrable g a b),
a ≤ b →
(∀ x:R, a < x < b → f x = g x) → RiemannInt pr1 = RiemannInt pr2.
Proof.
apply RiemannInt_P18.
Qed.
Lemma RiemannInt_le_ext :
∀ (f g:R → R) (a b:R) (pr1:Riemann_integrable f a b)
(pr2:Riemann_integrable g a b),
a ≤ b →
(∀ x:R, a < x < b → f x ≤ g x) → RiemannInt pr1 ≤ RiemannInt pr2.
Proof.
apply RiemannInt_P19.
Qed.
Lemma RiemannInt_primitive :
∀ (f:R → R) (a b:R) (h:a ≤ b)
(pr:∀ x:R, a ≤ x → x ≤ b → Riemann_integrable f a x)
(pr0:Riemann_integrable f a b),
RiemannInt pr0 = primitive h pr b - primitive h pr a.
Proof.
apply RiemannInt_P20.
Qed.
Lemma Riemann_integrable_included_left :
∀ (f:R → R) (a b c:R),
Riemann_integrable f a b → a ≤ c ≤ b → Riemann_integrable f a c.
Proof.
apply RiemannInt_P22.
Qed.
Lemma Riemann_integrable_included_right :
∀ (f:R → R) (a b c:R),
Riemann_integrable f a b → a ≤ c ≤ b → Riemann_integrable f c b.
Proof.
apply RiemannInt_P23.
Qed.
Lemma Riemann_integrable_Chasles :
∀ (f:R → R) (a b c:R),
Riemann_integrable f a b →
Riemann_integrable f b c → Riemann_integrable f a c.
Proof.
apply RiemannInt_P24.
Qed.
Lemma RiemannInt_Chasles :
∀ (f:R → R) (a b c:R) (pr1:Riemann_integrable f a b)
(pr2:Riemann_integrable f b c) (pr3:Riemann_integrable f a c),
RiemannInt pr1 + RiemannInt pr2 = RiemannInt pr3.
Proof.
apply RiemannInt_P26.
Qed.
Lemma derivable_primitive :
∀ (f:R → R) (a b x:R) (h:a ≤ b)
(C0:∀ x:R, a ≤ x ≤ b → continuity_pt f x),
a ≤ x ≤ b → derivable_pt_lim (primitive h (FTC_P1 h C0)) x (f x).
Proof.
apply RiemannInt_P28.
Qed.
End Copy_stdlib.
Lemma RiemannInt_integrable_eq_compat : ∀ f g a b, (∀ x, f x = g x) →
Riemann_integrable f a b → Riemann_integrable g a b.
intros f g a b H X eps.
elim X with eps;intros x p; ∃ x.
elim p; intros x0 [p01 p02]; ∃ x0.
split; intros; [ rewrite <- (H t); apply p01 | ]; assumption.
Qed.
Lemma RiemannInt_integrable_minus : ∀ (f g:R → R) (a b:R)
(prf:Riemann_integrable f a b)
(prg:Riemann_integrable g a b), (Riemann_integrable (fun x ⇒ f x - g x) a b).
Proof.
intros.
apply RiemannInt_integrable_eq_compat with (fun x ⇒ f x + (-1) × g x); [intros; ring|].
apply RiemannInt_P10; assumption.
Qed.
Lemma RiemannInt_minus :
∀ (f g:R → R) (a b:R)
(prf:Riemann_integrable f a b)
(prg:Riemann_integrable g a b)
(prfg:Riemann_integrable (fun x:R ⇒ f x - g x) a b),
a≤b → RiemannInt prfg = RiemannInt prf - RiemannInt prg.
Proof.
intros.
assert (REW: ∀ x y, x - y = x + (-1)*y) by (intros; ring); rewrite REW; clear REW.
pose proof (RiemannInt_P10 (-1) prf prg) as prfg'.
replace (RiemannInt prfg) with (RiemannInt prfg').
apply RiemannInt_P13.
apply RiemannInt_P18 ; intuition.
ring.
Qed.
Lemma RiemannInt_minus_1 :
∀ (f g:R → R) (a b:R)
(prf:Riemann_integrable f a b)
(prg:Riemann_integrable g a b),
a≤b → RiemannInt prf - RiemannInt prg = RiemannInt (RiemannInt_integrable_minus f g a b prf prg).
Proof.
intros. rewrite (RiemannInt_minus _ _ _ _ prf prg) ; intuition.
Qed.
Lemma RiemannInt_linear_1 :
∀ (f g:R → R) (a b l:R) (pr1:Riemann_integrable f a b)
(pr2:Riemann_integrable g a b),
RiemannInt pr1 + l × RiemannInt pr2 = RiemannInt (Riemann_integrable_linear f g a b l pr1 pr2).
Proof.
intros. symmetry. apply RiemannInt_linear.
Qed.
Lemma Riemann_integrable_add :
∀ (f g:R → R) (a b:R) (pr1:Riemann_integrable f a b)
(pr2:Riemann_integrable g a b),
Riemann_integrable (f + g)%F a b.
Proof.
intros. apply RiemannInt_integrable_eq_compat with (fun x ⇒ f x + 1 × g x).
intros. unfold plus_fct. ring. apply Riemann_integrable_linear ; assumption.
Qed.
Lemma RiemannInt_add :
∀ (f g:R → R) (a b:R) (prf:Riemann_integrable f a b)
(prg:Riemann_integrable g a b) (prfg:Riemann_integrable (f + g)%F a b), a ≤ b →
RiemannInt prf + RiemannInt prg = RiemannInt prfg.
Proof.
intros.
pose proof (RiemannInt_P10 1 prf prg) as prfg'.
replace (RiemannInt prfg) with (RiemannInt prfg').
replace (RiemannInt prg) with (1 × RiemannInt prg) by ring.
symmetry. apply RiemannInt_P13.
apply RiemannInt_P18 ; intuition. unfold plus_fct. ring.
Qed.
Lemma RiemannInt_add_1 :
∀ (f g:R → R) (a b:R) (prf:Riemann_integrable f a b)
(prg:Riemann_integrable g a b), a ≤ b →
RiemannInt prf + RiemannInt prg = RiemannInt (Riemann_integrable_add f g a b prf prg).
Proof.
intros.
apply RiemannInt_add. apply H.
Qed.
Hint Rewrite RiemannInt_minus_1 : Rintegrals.
Hint Rewrite RiemannInt_linear_1 : Rintegrals.
Hint Rewrite RiemannInt_add_1 : Rintegrals.
Lemma continuity_RiemannInt_1 :
∀ (f:R → R) (a b:R),
(∀ x:R, a ≤ x ≤ b ∨ b ≤ x ≤ a → continuity_pt f x) → Riemann_integrable f a b.
Proof.
intros; case (total_order_T a b); intro.
elim s ; intro.
apply RiemannInt_P6. assumption. intros. apply H. intuition.
subst; apply RiemannInt_P7.
apply Riemann_integrable_opp_bound. apply RiemannInt_P6. intuition.
intros. apply H. intuition.
Qed.
Lemma RiemannInt_derivable_pt_lim :
∀ (f:R → R) (a x:R)
(pr:∀ x y:R, Riemann_integrable f x y)
(Hcont:continuity_pt f x),
derivable_pt_lim (fun t1 ⇒ @RiemannInt f a t1 (pr a t1)) x (f x).
Proof.
intros.
unfold derivable_pt_lim. intros.
assert (H4:0 < eps / 2) by fourier.
destruct (Hcont _ H4) as [x1 [Hcont1 Hcont2]].
∃ (mkposreal _ Hcont1). intros.
rewrite <- (RiemannInt_Chasles f a x (x+h) (pr a x) (pr x (x + h)) (pr a (x + h))).
ring_simplify ((RiemannInt (pr a x) + RiemannInt (pr x (x + h)) - RiemannInt (pr a x))).
replace (f x) with (RiemannInt (Riemann_integrable_constant x (x + h) (f x)) / h)
by (rewrite RiemannInt_constant; field; assumption).
replace
(RiemannInt (pr x (x + h)) / h - RiemannInt (Riemann_integrable_constant x (x + h) (f x)) / h)
with ((RiemannInt (pr x (x + h)) + (-1) × RiemannInt (Riemann_integrable_constant x (x + h) (f x))) / h)
by (unfold Rdiv ; ring).
rewrite RiemannInt_linear_1.
unfold Rdiv in |- *; rewrite Rabs_mult; case (Rle_dec x (x + h)); intro.
apply Rle_lt_trans with
(RiemannInt
(Riemann_integrable_Rabs _ _ _
(Riemann_integrable_linear _ _ _ _ (-1) (pr x (x + h)) (Riemann_integrable_constant x (x + h) (f x)))) ×
Rabs (/ h)).
do 2 rewrite <- (Rmult_comm (Rabs (/ h))); apply Rmult_le_compat_l.
apply Rabs_pos. apply RiemannInt_le_Rabs. assumption.
apply Rle_lt_trans with
(RiemannInt (Riemann_integrable_constant x (x + h) (eps / 2)) × Rabs (/ h)).
do 2 rewrite <- (Rmult_comm (Rabs (/ h))); apply Rmult_le_compat_l.
apply Rabs_pos.
apply RiemannInt_P19; try assumption.
intros; replace (f x0 + -1 × fct_cte (f x) x0) with (f x0 - f x) by (intros ; unfold fct_cte ; simpl ; ring).
unfold fct_cte.
assert (x ≠ x0) by (intro ; subst ; destruct H2 ; fourier).
left. simpl in ×. unfold R_dist in ×. apply Hcont2.
unfold D_x, no_cond. repeat split. assumption.
eapply Rlt_trans ; [|apply H1].
assert (0 < x0 - x < h) by (intuition ; fourier).
rewrite Rabs_pos_eq. rewrite Rabs_pos_eq. intuition.
apply Rle_trans with (x0 - x) ; intuition. intuition.
rewrite RiemannInt_constant.
rewrite Rmult_assoc; replace ((x + h - x) × Rabs (/ h)) with 1.
ring_simplify. fourier.
rewrite Rabs_right.
replace (x + h - x) with h; [ idtac | ring ].
apply Rinv_r_sym.
assumption.
apply Rle_ge; left; apply Rinv_0_lt_compat.
elim r; intro.
apply Rplus_lt_reg_r with x; rewrite Rplus_0_r; assumption.
elim H0; symmetry in |- *; apply Rplus_eq_reg_l with x; rewrite Rplus_0_r;
assumption.
apply Rle_lt_trans with
(RiemannInt
(Riemann_integrable_Rabs _ _ _
(Riemann_integrable_opp_bound _ _ _
(Riemann_integrable_linear f (fct_cte (f x)) x
(x + h) (-1) (pr x (x + h))
(Riemann_integrable_constant x (x + h) (f x))))) ×
Rabs (/ h)).
do 2 rewrite <- (Rmult_comm (Rabs (/ h))); apply Rmult_le_compat_l.
apply Rabs_pos.
rewrite RiemannInt_bound_exchange_1.
rewrite Rabs_Ropp.
apply RiemannInt_le_Rabs. left. intuition.
apply Rle_lt_trans with
(RiemannInt (Riemann_integrable_constant (x + h) x (eps / 2)) × Rabs (/ h)).
do 2 rewrite <- (Rmult_comm (Rabs (/ h))); apply Rmult_le_compat_l.
apply Rabs_pos.
apply RiemannInt_le_ext.
auto with real.
intros. unfold fct_cte in ×. ring_simplify (-1 × f x).
intros; replace (f x0 + -1 × fct_cte (f x) x0) with (f x0 - f x).
unfold fct_cte in |- *; case (Req_dec x x0); intro.
rewrite H3. ring_simplify (f x0 + - f x0). rewrite Rabs_R0; left;
assumption.
left; simpl in Hcont2 ; ring_simplify (f x0 + -1 × f x) ; apply Hcont2.
repeat split.
assumption.
unfold R_dist. rewrite Rabs_left.
apply Rplus_lt_reg_r with (x0 - x1); replace (x0 - x1 + x1) with x0;
[ idtac | ring ].
replace (x0 - x1 + - (x0 - x)) with (x - x1); [ idtac | ring ].
apply Rle_lt_trans with (x + h).
unfold Rminus in |- *; apply Rplus_le_compat_l; apply Ropp_le_cancel.
rewrite Ropp_involutive; apply Rle_trans with (Rabs h).
rewrite <- Rabs_Ropp; apply RRle_abs.
apply Rle_trans with x1;
[ left; assumption | idtac ]. right. reflexivity.
elim H2; intros; assumption.
apply Rplus_lt_reg_r with x; rewrite Rplus_0_r;
replace (x + (x0 - x)) with x0; [ elim H2; intros; assumption | ring ].
unfold fct_cte in |- *; ring.
rewrite RiemannInt_P15.
rewrite Rmult_assoc; replace ((x - (x + h)) × Rabs (/ h)) with 1.
rewrite Rmult_1_r; unfold Rdiv in |- *; apply Rmult_lt_reg_l with 2;
[ prove_sup0
| rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc;
rewrite <- Rinv_r_sym;
[ rewrite Rmult_1_l; pattern eps at 1 in |- *; rewrite <- Rplus_0_r;
rewrite double; apply Rplus_lt_compat_l; assumption
| discrR ] ].
rewrite Rabs_left.
replace (x - (x + h)) with (- h); [ idtac | ring ].
rewrite Ropp_mult_distr_l_reverse; rewrite Ropp_mult_distr_r_reverse;
rewrite Ropp_involutive; apply Rinv_r_sym.
assumption.
apply Rinv_lt_0_compat.
assert (H8 : x + h < x).
auto with real.
apply Rplus_lt_reg_r with x; rewrite Rplus_0_r; assumption.
Qed.
Lemma RiemannInt_derivable_pt :
∀ (f:R → R) (a x:R)
(pr:∀ x y:R, Riemann_integrable f x y)
(Hcont:continuity_pt f x),
derivable_pt (fun t1 ⇒ @RiemannInt f a t1 (pr a t1)) x.
Proof.
intros.
unfold derivable_pt, derivable_pt_abs.
∃ (f x). apply RiemannInt_derivable_pt_lim.
assumption.
Qed.
Lemma derive_pt_RiemannInt :
∀ (f:R → R) (a x:R)
(pr:∀ x y:R, Riemann_integrable f x y)
(Hcont:continuity_pt f x),
derive_pt (fun t ⇒ RiemannInt (pr a t)) x (RiemannInt_derivable_pt f a x pr Hcont) = f x.
Proof.
intros.
rewrite derive_pt_eq. apply RiemannInt_derivable_pt_lim.
apply Hcont.
Qed.
Lemma derive_pt_RiemannInt_1 :
∀ (f:R → R) (a x:R)
(pr:∀ x y:R, Riemann_integrable f x y)
(Hcont:continuity_pt f x) H1,
derive_pt (fun t ⇒ RiemannInt (pr a t)) x H1 = f x.
Proof.
intros.
rewrite derive_pt_eq. apply RiemannInt_derivable_pt_lim.
apply Hcont.
Qed.
Lemma derivable_pt_continuity_Riemann_implies_C1 :
∀ f t0 (pr:∀ t t0, Riemann_integrable f t t0), continuity f →
C 1 (fun t ⇒ RiemannInt (pr t0 t)).
Proof.
intros.
assert (derivable (fun t ⇒ RiemannInt (pr t0 t))).
intro. apply RiemannInt_derivable_pt. apply H.
apply (C_S _ _ H0).
apply C_0. apply continuity_ext with f.
intro. unfold derive. rewrite derive_pt_RiemannInt_1.
reflexivity.
apply H. apply H.
Qed.
Lemma RiemannInt_continuity : ∀ a t0 (Hconta : continuity a) (Ha : ∀ t0 t,
Riemann_integrable a t0 t), continuity (fun t ⇒ RiemannInt (Ha t0 t)).
Proof.
intros.
apply derivable_continuous. unfold derivable. intros. apply RiemannInt_derivable_pt.
apply Hconta.
Qed.