Library Coqtail.Reals.Rseries.Rseries_RiemannInt
Properties involving series and integrals
Require Import Reals.
Require Import Rseries_def.
Require Import Rseries_facts.
Require Import RiemannInt.
Require Import Fourier.
Require Import Rsequence_facts.
Require Import Rsequence_subsequence.
Require Import Riemann_integrable.
Require Import Rintegral.
Open Local Scope R_scope.
Section Rseries_RiemannInt.
Local Coercion INR : nat >-> R.
Lemma Telescoping_series : ∀ a n, sum_f_R0 (fun i ⇒ a (S i) - a i) n = a (S n) - a O.
Proof.
intros a n.
rewrite tech11 with (fun i ⇒ a (S i) - a i) (fun i ⇒ a (S i)) a _; [|reflexivity].
destruct n; [reflexivity|].
rewrite tech2 with a O (S n); [|intuition].
rewrite tech5.
simpl (sum_f_R0 a 0).
replace (S n - 1)%nat with n by (simpl; apply minus_n_O).
assert (REW : ∀ S S' A B, S = S' → S + A - (B + S') = A - B) by (intros; subst; ring).
apply REW.
reflexivity.
Qed.
Lemma Telescoping_series_opp : ∀ a n, sum_f_R0 (fun i ⇒ a i - a (S i)) n = a O - a (S n).
Proof.
intros a n.
rewrite tech11 with (fun i ⇒ a i - a (S i)) a (fun i ⇒ a (S i)) _; [|reflexivity].
destruct n; [reflexivity|].
rewrite tech2 with a O (S n); [|intuition].
rewrite tech5.
simpl (sum_f_R0 a 0).
replace (S n - 1)%nat with n by (simpl; apply minus_n_O).
assert (REW : ∀ S S' A B, S = S' → A + S - (S' + B) = A - B) by (intros; subst; ring).
apply REW.
reflexivity.
Qed.
Require Import Rseries_def.
Require Import Rseries_facts.
Require Import RiemannInt.
Require Import Fourier.
Require Import Rsequence_facts.
Require Import Rsequence_subsequence.
Require Import Riemann_integrable.
Require Import Rintegral.
Open Local Scope R_scope.
Section Rseries_RiemannInt.
Local Coercion INR : nat >-> R.
Lemma Telescoping_series : ∀ a n, sum_f_R0 (fun i ⇒ a (S i) - a i) n = a (S n) - a O.
Proof.
intros a n.
rewrite tech11 with (fun i ⇒ a (S i) - a i) (fun i ⇒ a (S i)) a _; [|reflexivity].
destruct n; [reflexivity|].
rewrite tech2 with a O (S n); [|intuition].
rewrite tech5.
simpl (sum_f_R0 a 0).
replace (S n - 1)%nat with n by (simpl; apply minus_n_O).
assert (REW : ∀ S S' A B, S = S' → S + A - (B + S') = A - B) by (intros; subst; ring).
apply REW.
reflexivity.
Qed.
Lemma Telescoping_series_opp : ∀ a n, sum_f_R0 (fun i ⇒ a i - a (S i)) n = a O - a (S n).
Proof.
intros a n.
rewrite tech11 with (fun i ⇒ a i - a (S i)) a (fun i ⇒ a (S i)) _; [|reflexivity].
destruct n; [reflexivity|].
rewrite tech2 with a O (S n); [|intuition].
rewrite tech5.
simpl (sum_f_R0 a 0).
replace (S n - 1)%nat with n by (simpl; apply minus_n_O).
assert (REW : ∀ S S' A B, S = S' → A + S - (S' + B) = A - B) by (intros; subst; ring).
apply REW.
reflexivity.
Qed.
Lemma Rint_generalized_Chasles : ∀ f An,
(∀ n : nat, Rint f n (S n) (An n)) →
∀ n : nat, Rint f 0 (S n) (sum_f_R0 An n).
Proof.
intros f An H.
induction n.
apply (H O).
apply Rint_Chasles with (S n).
apply IHn.
apply H.
Qed.
Section Rser_RiemannInt_link.
Variable f : R → R.
Hypothesis Hcont : ∀ x, 0 ≤ x → continuity_pt f x.
Hypothesis Hpos : ∀ x, 0 ≤ x → 0 ≤ f x.
Hypothesis Hdec : ∀ x y : R, 0 ≤ x ≤ y → f y ≤ f x.
Lemma Riemann_integrable_f_n_Sn : ∀ (n : nat), Riemann_integrable f (INR n) (INR (S n)).
Proof.
intro n.
apply continuity_implies_RiemannInt.
apply le_INR; do 2 constructor.
intros x [Hnx HxSn]; apply Hcont.
apply (Rle_trans 0 (INR n) x (le_INR _ _ (le_O_n n)) Hnx).
Qed.
Lemma Rser_RiemannInt_link_general_term_integrable : ∀ (n : nat),
Riemann_integrable (fun x ⇒ fct_cte (f (INR n)) x - f x) (INR n) (INR (S n)).
Proof.
intros n.
apply RiemannInt_integrable_minus.
apply RiemannInt_P6.
auto with ×.
intros x Hx.
apply continuity_const.
intros y z; reflexivity.
apply (Riemann_integrable_f_n_Sn n).
Qed.
Lemma Rser_RiemannInt_link_general_term_bound (n : nat) :
RiemannInt (Rser_RiemannInt_link_general_term_integrable n) ≤ f (INR n) - f (INR (S n)).
Proof.
intros.
rewrite <- Rmult_1_r.
replace 1 with (INR (S n) - (INR n)).
assert (pr:Riemann_integrable (fct_cte (f (INR n) - f (INR (S n)))) (INR n) (INR (S n))) by apply RiemannInt_P14.
rewrite <- RiemannInt_P15 with _ _ _ pr.
apply RiemannInt_P19; [intuition|].
unfold fct_cte.
intros x [xn xsn].
apply Rminus_le_compat_r.
apply Hdec.
split.
apply Rle_trans with (INR n).
auto with ×.
left; apply xn.
apply (Rlt_le _ _ xsn).
rewrite <- minus_INR by intuition.
replace (S n - n)%nat with 1%nat by intuition.
reflexivity.
Qed.
(∀ n : nat, Rint f n (S n) (An n)) →
∀ n : nat, Rint f 0 (S n) (sum_f_R0 An n).
Proof.
intros f An H.
induction n.
apply (H O).
apply Rint_Chasles with (S n).
apply IHn.
apply H.
Qed.
Section Rser_RiemannInt_link.
Variable f : R → R.
Hypothesis Hcont : ∀ x, 0 ≤ x → continuity_pt f x.
Hypothesis Hpos : ∀ x, 0 ≤ x → 0 ≤ f x.
Hypothesis Hdec : ∀ x y : R, 0 ≤ x ≤ y → f y ≤ f x.
Lemma Riemann_integrable_f_n_Sn : ∀ (n : nat), Riemann_integrable f (INR n) (INR (S n)).
Proof.
intro n.
apply continuity_implies_RiemannInt.
apply le_INR; do 2 constructor.
intros x [Hnx HxSn]; apply Hcont.
apply (Rle_trans 0 (INR n) x (le_INR _ _ (le_O_n n)) Hnx).
Qed.
Lemma Rser_RiemannInt_link_general_term_integrable : ∀ (n : nat),
Riemann_integrable (fun x ⇒ fct_cte (f (INR n)) x - f x) (INR n) (INR (S n)).
Proof.
intros n.
apply RiemannInt_integrable_minus.
apply RiemannInt_P6.
auto with ×.
intros x Hx.
apply continuity_const.
intros y z; reflexivity.
apply (Riemann_integrable_f_n_Sn n).
Qed.
Lemma Rser_RiemannInt_link_general_term_bound (n : nat) :
RiemannInt (Rser_RiemannInt_link_general_term_integrable n) ≤ f (INR n) - f (INR (S n)).
Proof.
intros.
rewrite <- Rmult_1_r.
replace 1 with (INR (S n) - (INR n)).
assert (pr:Riemann_integrable (fct_cte (f (INR n) - f (INR (S n)))) (INR n) (INR (S n))) by apply RiemannInt_P14.
rewrite <- RiemannInt_P15 with _ _ _ pr.
apply RiemannInt_P19; [intuition|].
unfold fct_cte.
intros x [xn xsn].
apply Rminus_le_compat_r.
apply Hdec.
split.
apply Rle_trans with (INR n).
auto with ×.
left; apply xn.
apply (Rlt_le _ _ xsn).
rewrite <- minus_INR by intuition.
replace (S n - n)%nat with 1%nat by intuition.
reflexivity.
Qed.
Lemma Rser_RiemannInt_link : { l | Rser_cv (fun n ⇒ f (INR n) - RiemannInt (Riemann_integrable_f_n_Sn n) ) l}.
Proof.
apply Rser_pos_bound_cv with (f 0).
intro n.
destruct (Rint_constant (f n) n (S n)) as [ pr int].
replace (f n × (S n -n)) with (f n) in int by (rewrite S_INR; ring).
rewrite <- int.
apply Rle_minus'.
apply RiemannInt_P19; [intuition|].
intros x [xn snx].
assert(Hcond : 0 ≤ (INR n) ≤ x).
split.
auto with ×.
left; apply xn.
apply (Hdec _ _ Hcond).
intro n.
apply Rle_trans with (sum_f_R0 (fun n ⇒ f (INR n) - f (INR (S n))) n).
apply sum_Rle.
intros i ni.
destruct (Rint_constant (f i) i (S i)) as [ pr int].
replace (f i × (S i -i)) with (f i) in int by (rewrite S_INR; ring).
rewrite <- int.
rewrite <- RiemannInt_minus with _ _ _ _ _ _ (Rser_RiemannInt_link_general_term_integrable i); [|intuition].
rewrite RiemannInt_P15.
replace (INR (S i) - INR i) with 1.
rewrite Rmult_1_r.
apply (Rser_RiemannInt_link_general_term_bound i).
rewrite <- minus_INR by intuition.
replace (S i - i)%nat with 1%nat by intuition.
reflexivity.
rewrite Telescoping_series_opp.
rewrite <- Rminus_0_r.
apply Rminus_le_compat_r.
apply Hpos.
auto with ×.
Qed.
Lemma Rser_RiemannInt_cv_pos_infty :
∃ pr : ∀ (n : nat), Riemann_integrable f 0 (INR n),
Rseq_cv_pos_infty (fun n ⇒ RiemannInt (pr (S n))) →
(sum_f_R0 (fun n ⇒ f (INR n))) ¬ (fun n ⇒ RiemannInt (pr (S n))).
Proof.
assert (pr : ∀ n : nat, Riemann_integrable f 0 n).
intro n.
apply continuity_implies_RiemannInt.
intuition.
intros x [Hx _]; apply (Hcont x Hx).
∃ pr.
intro Hdiv.
destruct Rser_RiemannInt_link as [ l Hl].
apply Rseq_equiv_sym.
unfold Rseq_equiv, Rseq_minus.
apply Rseq_cv_little_O_cv_pos_infty with (-l).
apply Rseq_cv_eq_compat with
(sum_f_R0 (fun n : nat ⇒- (f (INR n) - RiemannInt (Riemann_integrable_f_n_Sn n)))).
intro n.
destruct (Rint_generalized_Chasles f
(fun n ⇒RiemannInt (Riemann_integrable_f_n_Sn n))
(fun n ⇒ Rint_RiemannInt_link f n (S n) (Riemann_integrable_f_n_Sn n)) n) as [prn H].
rewrite RiemannInt_P5 with _ _ _ (pr (S n)) prn.
rewrite H.
rewrite <- minus_sum.
apply sum_eq; intros p Hp.
unfold Rminus.
ring.
unfold Rser_cv in Hl.
apply Rser_cv_opp_compat; apply Hl.
apply Hdiv.
Qed.
End Rser_RiemannInt_link.
Section Applications.
Definition ln1 := comp ln (fun x ⇒ x+1).
Lemma Rint_inv1 : ∀ a b,
-1 < a ≤ b → Rint (/(id + fct_cte 1))%F a b (ln (b + 1) - ln (a + 1)).
Proof.
intros a b Hab.
replace (ln (b + 1)) with (comp ln (id + fct_cte 1) b) by reflexivity.
replace (ln (a + 1)) with (comp ln (id + fct_cte 1) a) by reflexivity.
apply Rint_derive.
intuition.
intros x Hx.
replace ((/ (id + fct_cte 1))%F x) with ((/ (id + fct_cte 1))%F x × (1+0)) by ring.
apply derivable_pt_lim_comp.
apply derivable_pt_lim_plus.
apply derivable_pt_lim_id.
apply derivable_pt_lim_const.
apply derivable_pt_lim_ln.
unfold plus_fct, fct_cte, id.
intuition.
apply Rlt_le_trans with (a + 1); fourier.
intros x Hx.
apply continuity_pt_inv.
apply continuity_pt_plus.
apply derivable_continuous, derivable_id.
apply continuity_pt_const.
unfold fct_cte; intros u v; reflexivity.
unfold fct_cte, id, plus_fct.
assert(0 < x + 1).
apply Rlt_le_trans with (a + 1).
replace 0 with (- 1 + 1) by ring.
apply Rplus_lt_compat_r; intuition.
apply Rplus_le_compat_r; intuition.
auto with ×.
Qed.
Proof.
apply Rser_pos_bound_cv with (f 0).
intro n.
destruct (Rint_constant (f n) n (S n)) as [ pr int].
replace (f n × (S n -n)) with (f n) in int by (rewrite S_INR; ring).
rewrite <- int.
apply Rle_minus'.
apply RiemannInt_P19; [intuition|].
intros x [xn snx].
assert(Hcond : 0 ≤ (INR n) ≤ x).
split.
auto with ×.
left; apply xn.
apply (Hdec _ _ Hcond).
intro n.
apply Rle_trans with (sum_f_R0 (fun n ⇒ f (INR n) - f (INR (S n))) n).
apply sum_Rle.
intros i ni.
destruct (Rint_constant (f i) i (S i)) as [ pr int].
replace (f i × (S i -i)) with (f i) in int by (rewrite S_INR; ring).
rewrite <- int.
rewrite <- RiemannInt_minus with _ _ _ _ _ _ (Rser_RiemannInt_link_general_term_integrable i); [|intuition].
rewrite RiemannInt_P15.
replace (INR (S i) - INR i) with 1.
rewrite Rmult_1_r.
apply (Rser_RiemannInt_link_general_term_bound i).
rewrite <- minus_INR by intuition.
replace (S i - i)%nat with 1%nat by intuition.
reflexivity.
rewrite Telescoping_series_opp.
rewrite <- Rminus_0_r.
apply Rminus_le_compat_r.
apply Hpos.
auto with ×.
Qed.
Lemma Rser_RiemannInt_cv_pos_infty :
∃ pr : ∀ (n : nat), Riemann_integrable f 0 (INR n),
Rseq_cv_pos_infty (fun n ⇒ RiemannInt (pr (S n))) →
(sum_f_R0 (fun n ⇒ f (INR n))) ¬ (fun n ⇒ RiemannInt (pr (S n))).
Proof.
assert (pr : ∀ n : nat, Riemann_integrable f 0 n).
intro n.
apply continuity_implies_RiemannInt.
intuition.
intros x [Hx _]; apply (Hcont x Hx).
∃ pr.
intro Hdiv.
destruct Rser_RiemannInt_link as [ l Hl].
apply Rseq_equiv_sym.
unfold Rseq_equiv, Rseq_minus.
apply Rseq_cv_little_O_cv_pos_infty with (-l).
apply Rseq_cv_eq_compat with
(sum_f_R0 (fun n : nat ⇒- (f (INR n) - RiemannInt (Riemann_integrable_f_n_Sn n)))).
intro n.
destruct (Rint_generalized_Chasles f
(fun n ⇒RiemannInt (Riemann_integrable_f_n_Sn n))
(fun n ⇒ Rint_RiemannInt_link f n (S n) (Riemann_integrable_f_n_Sn n)) n) as [prn H].
rewrite RiemannInt_P5 with _ _ _ (pr (S n)) prn.
rewrite H.
rewrite <- minus_sum.
apply sum_eq; intros p Hp.
unfold Rminus.
ring.
unfold Rser_cv in Hl.
apply Rser_cv_opp_compat; apply Hl.
apply Hdiv.
Qed.
End Rser_RiemannInt_link.
Section Applications.
Definition ln1 := comp ln (fun x ⇒ x+1).
Lemma Rint_inv1 : ∀ a b,
-1 < a ≤ b → Rint (/(id + fct_cte 1))%F a b (ln (b + 1) - ln (a + 1)).
Proof.
intros a b Hab.
replace (ln (b + 1)) with (comp ln (id + fct_cte 1) b) by reflexivity.
replace (ln (a + 1)) with (comp ln (id + fct_cte 1) a) by reflexivity.
apply Rint_derive.
intuition.
intros x Hx.
replace ((/ (id + fct_cte 1))%F x) with ((/ (id + fct_cte 1))%F x × (1+0)) by ring.
apply derivable_pt_lim_comp.
apply derivable_pt_lim_plus.
apply derivable_pt_lim_id.
apply derivable_pt_lim_const.
apply derivable_pt_lim_ln.
unfold plus_fct, fct_cte, id.
intuition.
apply Rlt_le_trans with (a + 1); fourier.
intros x Hx.
apply continuity_pt_inv.
apply continuity_pt_plus.
apply derivable_continuous, derivable_id.
apply continuity_pt_const.
unfold fct_cte; intros u v; reflexivity.
unfold fct_cte, id, plus_fct.
assert(0 < x + 1).
apply Rlt_le_trans with (a + 1).
replace 0 with (- 1 + 1) by ring.
apply Rplus_lt_compat_r; intuition.
apply Rplus_le_compat_r; intuition.
auto with ×.
Qed.
Equivalent of the harmonic series
Lemma harmonic_series_equiv : (sum_f_R0 (fun n ⇒ / (S n))) ¬ (fun n ⇒ ln (S (S n))).
Proof.
destruct (Rser_RiemannInt_cv_pos_infty (/(id + fct_cte 1))%F) as [int_f_0_n Hi];
unfold plus_fct, fct_cte, id, inv_fct.
intros x Hx.
apply continuity_pt_inv.
apply (continuity_pt_plus _ _ _
(derivable_continuous id derivable_id x)
(derivable_continuous _ (derivable_const 1) x)).
auto with ×.
auto with ×.
intros x y [Hxpos Hxy].
apply Rle_Rinv; fourier.
assert (Heq2 : (fun n : nat ⇒ ln (INR (S (S n)))) ==
(fun n : nat ⇒ RiemannInt (int_f_0_n (S n)))).
intro n.
replace (ln (S (S n))) with ((ln (S n + 1)%R - ln (O + 1))).
destruct (Rint_inv1 0%nat (S n)) as [Hint Heq].
auto with ×.
rewrite <- Heq.
apply RiemannInt_P18.
auto with ×.
reflexivity.
replace (INR (S n) + 1) with (INR (S (S n))) by trivial.
replace (INR 0 + 1) with 1 by (simpl; ring).
rewrite ln_1.
ring.
assert(Rseq_cv_pos_infty (fun n : nat ⇒ RiemannInt (int_f_0_n (S n)))) as Hdiv.
apply Rseq_cv_pos_infty_eq_compat with (fun n : nat ⇒ ln (S (S n))).
apply Heq2.
apply Rseq_subseq_cv_pos_infty_compat with (fun n ⇒ ln n).
assert (Hex : is_extractor (fun n ⇒ (S (S n)))).
constructor.
∃ (exist _ _ Hex).
trivial.
apply Rseq_ln_cv.
assert(Heq1 : (sum_f_R0 (fun n : nat ⇒ (/ (id + fct_cte 1))%F (INR n))) ==
(sum_f_R0 (fun n : nat ⇒ / INR (S n)))).
intro n; apply sum_eq; intros k Hk.
unfold inv_fct, id, plus_fct, fct_cte.
rewrite S_INR.
reflexivity.
apply Rseq_eq_sym in Heq2.
apply (Rseq_equiv_eq_compat
_ _ _ _ Heq1 Heq2 (Hi Hdiv)).
Qed.
End Applications.
End Rseries_RiemannInt.
Proof.
destruct (Rser_RiemannInt_cv_pos_infty (/(id + fct_cte 1))%F) as [int_f_0_n Hi];
unfold plus_fct, fct_cte, id, inv_fct.
intros x Hx.
apply continuity_pt_inv.
apply (continuity_pt_plus _ _ _
(derivable_continuous id derivable_id x)
(derivable_continuous _ (derivable_const 1) x)).
auto with ×.
auto with ×.
intros x y [Hxpos Hxy].
apply Rle_Rinv; fourier.
assert (Heq2 : (fun n : nat ⇒ ln (INR (S (S n)))) ==
(fun n : nat ⇒ RiemannInt (int_f_0_n (S n)))).
intro n.
replace (ln (S (S n))) with ((ln (S n + 1)%R - ln (O + 1))).
destruct (Rint_inv1 0%nat (S n)) as [Hint Heq].
auto with ×.
rewrite <- Heq.
apply RiemannInt_P18.
auto with ×.
reflexivity.
replace (INR (S n) + 1) with (INR (S (S n))) by trivial.
replace (INR 0 + 1) with 1 by (simpl; ring).
rewrite ln_1.
ring.
assert(Rseq_cv_pos_infty (fun n : nat ⇒ RiemannInt (int_f_0_n (S n)))) as Hdiv.
apply Rseq_cv_pos_infty_eq_compat with (fun n : nat ⇒ ln (S (S n))).
apply Heq2.
apply Rseq_subseq_cv_pos_infty_compat with (fun n ⇒ ln n).
assert (Hex : is_extractor (fun n ⇒ (S (S n)))).
constructor.
∃ (exist _ _ Hex).
trivial.
apply Rseq_ln_cv.
assert(Heq1 : (sum_f_R0 (fun n : nat ⇒ (/ (id + fct_cte 1))%F (INR n))) ==
(sum_f_R0 (fun n : nat ⇒ / INR (S n)))).
intro n; apply sum_eq; intros k Hk.
unfold inv_fct, id, plus_fct, fct_cte.
rewrite S_INR.
reflexivity.
apply Rseq_eq_sym in Heq2.
apply (Rseq_equiv_eq_compat
_ _ _ _ Heq1 Heq2 (Hi Hdiv)).
Qed.
End Applications.
End Rseries_RiemannInt.