Real riemannian integrals

Require Import Reals.
Require Import RiemannInt.
Require Import RIneq.
Require Import Fourier.
Require Import R_sqr.
Require Import MyRfunctions.
Open Local Scope R_scope.

Definition of the integral of f between a and b using Riemann_integrable

Definition Rint f a b I := {pr : Riemann_integrable f a b | RiemannInt pr = I}.

Common results on integrals

Section Rint_facts.

The integral from a to b is the opposite of the integral from b to a

Lemma Rint_reverse_1 : f a b x, Rint f a b (-x) → Rint f b a x.
Proof.
intros f a b x [pr H]. pose proof RiemannInt_P1 pr as pr2.
pr2;
assert(RiemannInt pr2 = - RiemannInt pr) as Hrew;
[ apply RiemannInt_P8 | rewrite Hrew];
rewrite H; intuition.
Qed.

Lemma Rint_reverse_2 : f a b x, Rint f a b xRint f b a (-x).
Proof.
intros f a b x [pr H].
pose proof RiemannInt_P1 pr as pr2;
pr2;
assert(RiemannInt pr2 = - RiemannInt pr) as Hrew;
[ apply RiemannInt_P8 | rewrite Hrew];
rewrite H; intuition.
Qed.

Lemma Riemann_integrable_eq_compat : f g a b,
( x, Rmin a b x Rmax a bg x = f x) →
Riemann_integrable f a b
Riemann_integrable g a b.
Proof.
intros f g a b Heq prf;
case(Rle_dec a b); intro Hab;
[ | apply RiemannInt_P1 in prf;
apply RiemannInt_P1];
intro eps; destruct (prf eps) as [phi [psi Hpsi]];
[ | rewrite Rmin_comm, Rmax_comm in Heq ];
phi; psi.
split; [
intros t Ht; rewrite Heq; [ apply Hpsi | apply Ht] ;
apply Ht |
apply Hpsi ] .
split; [
intros t Ht; rewrite Heq; [ apply Hpsi | apply Ht] ;
apply Ht |
apply Hpsi ] .
Qed.

Lemma Rint_eq_compat : f g a b x,
( x, Rmin a b x Rmax a bg x = f x) →
Rint f a b xRint g a b x.
Proof.
intros f g a b x Heq.
case(Rle_dec a b); intros Hab.
intros [prf Hf].
pose proof (Riemann_integrable_eq_compat f g a b Heq prf) as prg.
prg.
erewrite RiemannInt_P18.
apply Hf.
apply Hab.
rewrite (Rmin_def _ _ Hab), (Rmax_def _ _ Hab) in Heq.
intuition.
rewrite Rmin_comm, Rmax_comm in Heq.
intro RIf.
apply Rint_reverse_1.
apply Rint_reverse_2 in RIf.
destruct RIf as [prf Hf].
pose proof (Riemann_integrable_eq_compat f g b a Heq prf) as prg.
prg.
apply Rnot_le_lt, Rlt_le in Hab.
erewrite RiemannInt_P18.
apply Hf.
apply Hab.
rewrite (Rmin_def _ _ Hab), (Rmax_def _ _ Hab) in Heq.
intuition.
Qed.

Lemma Rint_RiemannInt_link : f a b (pr : Riemann_integrable f a b),
Rint f a b (RiemannInt pr).
Proof.
intros f a b pr.
pr.
reflexivity.
Qed.

Continuous functions are integrable

Lemma Rint_continuity : f a b,
a b
( x, a x bcontinuity_pt f x) →
{x : R & (Rint f a b x)}.
Proof.
intros f a b Hab f_cont.
(RiemannInt (continuity_implies_RiemannInt Hab f_cont)).
apply Rint_RiemannInt_link.
Qed.

Chasles relation on integrals

Lemma Rint_Chasles : f a b c x y,
Rint f a b xRint f b c yRint f a c (x+y).
Proof.
intros f a b c x y [prab Hab] [prbc Hbc].
pose proof (RiemannInt_P24 prab prbc) as prac.
prac.
rewrite <- Hab, <- Hbc.
symmetry.
apply RiemannInt_P26.
Qed.

Lemma Rint_singleton : f a, Rint f a a 0.
Proof.
intros f a.
pose proof RiemannInt_P7 f a as pr.
pr.
apply RiemannInt_P9.
Qed.

Lemma Rint_constant : c a b, Rint (fct_cte c) a b (c*(b-a)).
Proof.
intros c a b.
pose proof RiemannInt_P14 a b c as pr.
pr.
apply RiemannInt_P15.
Qed.

The value of the integral is unique

Lemma Rint_uniqueness : f a b x y, Rint f a b xRint f a b yx = y.
Proof.
intros f a b x y [pr1 H1] [pr2 H2].
rewrite <- H1, <- H2.
apply RiemannInt_P5.
Qed.

Lemma Rint_subinterval : f a b c x, (a b c) →
Rint f a c x{y : R & Rint f a b y & Rint f b c (x-y)}.
Proof.
intros f a b c x Hb [prac Hf].
pose proof RiemannInt_P22 prac Hb as prab.
(RiemannInt prab).
apply Rint_RiemannInt_link.
pose proof RiemannInt_P23 prac Hb as prbc.
prbc.
rewrite <- Hf.
rewrite <- RiemannInt_P26 with _ _ _ _ prab prbc prac.
ring.
Qed.

End Rint_facts.

Compatibility of integrals with operations

Section Rint_operations.

Lemma Rint_eq : x y f a b, Rint f a b xx = yRint f a b y.
Proof.
intros x y f a b H Heq.
subst. apply H.
Qed.

Lemma Rint_plus : f g a b x y, Rint f a b xRint g a b yRint (f + g)%F a b (x + y).
Proof.
intros f g a b x y [prf Hf] [prg Hg]; unfold plus_fct.
apply Rint_eq_compat with (fun uf u + 1 × g u).
intros; ring.
replace (x+y) with (x+1×y) by ring.
pose proof RiemannInt_P10 1 prf prg as prfg.
prfg.
rewrite RiemannInt_P13 with _ _ _ _ _ prf prg prfg.
rewrite Hf, Hg; reflexivity.
Qed.

Lemma Rint_minus : f g a b x y, Rint f a b xRint g a b yRint (f - g)%F a b (x - y).
Proof.
intros f g a b x y [prf Hf] [prg Hg]; unfold minus_fct.
apply Rint_eq_compat with (fun uf u + (-1) × g u).
intros; ring.
replace (x - y) with (x+(-1)*y) by ring.
pose proof RiemannInt_P10 (-1) prf prg as prfg.
prfg.
rewrite RiemannInt_P13 with _ _ _ _ _ prf prg prfg.
rewrite Hf, Hg; reflexivity.
Qed.

Lemma Rint_opp1 : f a b x, Rint f a b xRint (- f)%F a b (- x).
Proof.
intros f a b x; intros [prf Hf]; unfold opp_fct.
apply Rint_eq_compat with (fun ufct_cte 0 u + (-1) × f u).
unfold fct_cte; intros; ring.
replace (- x) with (0 + (-1)* x) by ring.
pose proof Rint_constant 0 a b as [prg Hg].
pose proof RiemannInt_P10 (-1) prg prf as prfg.
prfg.
rewrite RiemannInt_P13 with _ _ _ _ _ prg prf prfg.
rewrite Hf, Hg; ring.
Qed.

Lemma Rint_opp2 : f a b x, Rint (-f)%F a b (- x) → Rint f a b x.
Proof.
intros f a b x; intros [prf Hf]; unfold opp_fct.
apply Rint_eq_compat with (fun ufct_cte 0 u + (-1) ×(- f)%F u).
unfold fct_cte, opp_fct; intros; ring.
replace (x) with (0 + (-1)*(- x)) by ring.
pose proof Rint_constant 0 a b as [prg Hg].
pose proof RiemannInt_P10 (-1) prg prf as prfg.
prfg.
rewrite RiemannInt_P13 with _ _ _ _ _ prg prf prfg.
rewrite Hf, Hg; ring.
Qed.

Lemma Rint_scalar_mult_compat_l : f a b x C, Rint f a b xRint (fct_cte C × f)%F a b (C×x).
Proof.
intros f a b x C [prf Hf].
apply Rint_eq_compat with (fun ufct_cte 0 u + C × f u).
unfold fct_cte, mult_fct; intros; ring.
replace (C × x) with (0 + C× x) by ring.
pose proof Rint_constant 0 a b as [prg Hg].
pose proof RiemannInt_P10 C prg prf as prfg.
prfg.
rewrite RiemannInt_P13 with _ _ _ _ _ prg prf prfg.
rewrite Hf, Hg; ring.
Qed.

Lemma Rint_scalar_mult_compat_r : f a b x C, Rint f a b xRint (f × fct_cte C)%F a b (x × C).
Proof.
intros f a b x C [prf Hf].
apply Rint_eq_compat with (fun ufct_cte 0 u + C × f u).
unfold fct_cte, mult_fct; intros; ring.
replace (C × x) with (0 + C× x) by ring.
pose proof Rint_constant 0 a b as [prg Hg].
pose proof RiemannInt_P10 C prg prf as prfg.
prfg.
rewrite RiemannInt_P13 with _ _ _ _ _ prg prf prfg.
rewrite Hf, Hg; ring.
Qed.

End Rint_operations.

Create HintDb Rint.

Hint Resolve Rint_reverse_2 : Rint.
Hint Resolve Rint_RiemannInt_link : Rint.
Hint Resolve Rint_Chasles : Rint.
Hint Resolve Rint_constant : Rint.
Hint Resolve Rint_plus : Rint.
Hint Resolve Rint_minus : Rint.
Hint Resolve Rint_opp1 : Rint.
Hint Resolve Rint_scalar_mult_compat_l : Rint.
Hint Resolve Rint_scalar_mult_compat_r : Rint.
Hint Resolve Rint_uniqueness : Rint.
Hint Resolve RiemannInt_P6 : Rint.
Hint Resolve RiemannInt_P7 : Rint.
Hint Resolve RiemannInt_P10 : Rint.
Hint Resolve RiemannInt_P14 : Rint.
Hint Resolve RiemannInt_P16 : Rint.

Section Rint_props.

Inequalities involving integrals

Lemma Rint_le_compat : f g a b x y,
a b → ( u, a < u < bf u g u) →
Rint f a b xRint g a b yx y.
Proof.
intros f g a b x y Hab Heq [prh Hf] [prg Hg].
rewrite <- Hf, <- Hg.
apply RiemannInt_P19.
apply Hab.
apply Heq.
Qed.

A positive function has positive growing integral

Lemma Rint_pos : f a b x,
a b → ( u, a u b → 0 f u) → Rint f a b x → 0 x.
Proof.
intros f a b x Hab Hpos Hf.
destruct(Rint_constant 0 a b) as [pr0 H0].
ring_simplify in H0.
apply Rint_le_compat with (fct_cte 0) f a b.
apply Hab.
intros u Hu; apply Hpos; intuition.
pr0.
apply H0.
apply Hf.
Qed.

Inequality between integral of the absolute value and absolute value of the integral

Lemma Rint_abs_le_int : f a b x,
a bRint f a b x
{y : R & (Rint (fun uRabs (f u)) a b y) & (Rabs x y)}.
Proof.
intros f a b x Hab [prf Hf].
pose proof RiemannInt_P16 prf as prabs.
(RiemannInt prabs).
prabs.
reflexivity.
rewrite <- Hf.
apply RiemannInt_P17.
apply Hab.
Qed.

A non always null, non negative, continuous function on a non trivial segment has positive integral

Lemma Rint_continuous_gt_0 : f a b u X,
a < b
a u b
( x, a x bcontinuity_pt f x) →
( x, a x b → 0 f x) →
f u 0 → Rint f a b X → 0 < X.
Proof.
intros f a b u X Hab Haub Hcont Hpos Hu HX.
destruct (continuous_neq_0 f u (Hcont u Haub) Hu) as [eps Heps].
assert( c, d, a c b a d b c < d x, c x d → 0 < f x).
(Rmax a (u -eps/2)).
(Rmin b (u+ eps/2)).
assert(Heps2 : 0 < eps/2) .
apply Rlt_mult_inv_pos.
apply cond_pos.
auto with ×.
repeat split.
apply RmaxLess1.

apply Rmax_le.
left; apply Hab.

apply Rle_trans with u; [fourier | intuition].

apply Rmin_ge.
left; apply Hab.
apply Rle_trans with u; [intuition | fourier].

apply Rmin_l.

case(Rle_lt_or_eq_dec a u(proj1 Haub)); intro Hau.
apply Rlt_le_trans with u.
apply Rmax_lt; [intuition | fourier].
apply Rmin_ge; [intuition | fourier].
subst.
apply Rle_lt_trans with u.
apply Rmax_le; fourier.
apply Rmin_2; fourier.
intros x Hx.
rewrite <- Rabs_pos_eq.
apply Rabs_pos_lt.
replace x with (u+ (x-u)) by ring.
apply (Heps (x-u)).
assert( u - eps < x < u + eps) as [ Hu1 Hu2].
split.
apply Rlt_le_trans with (Rmax a (u - eps/2)).
apply Rlt_le_trans with (u-eps/2).
fourier.
apply RmaxLess2.
apply Hx.
apply Rle_lt_trans with (Rmin b (u + eps/2)).
apply Hx.
apply Rle_lt_trans with (u + eps/2).
apply Rmin_r.
fourier.
apply Rabs_def1; fourier.
apply Hpos.
split.
eapply Rle_trans.
apply RmaxLess1.
apply (proj1 Hx).
eapply Rle_trans.
apply (proj2 Hx).
apply Rmin_l.
destruct H as [c [d [ Hacb [Hadb [Hcd Hstp]]]]].
destruct (Rint_subinterval _ _ _ _ _ Hacb HX) as [Y HY HZ'].
assert(c db) as Hcdb by intuition.
destruct (Rint_subinterval _ _ _ _ _ Hcdb HZ') as [T HV HT'].
destruct (continuity_ab_min f c d) as [m Hm].
apply Hcdb.

intros x Hcxd.
apply Hcont.
split; eapply Rle_trans; [apply Hacb | apply Hcxd | apply Hcxd | apply Hadb].
apply Rlt_le_trans with ((f m) × (d - c)).
apply Rmult_lt_0_compat; [apply Hstp; apply Hm | fourier].
apply Rle_trans with T.
apply Rint_le_compat with (fct_cte (f m)) f c d.
apply Hcdb.

intros; apply Hm; split; apply Rlt_le; apply H.

apply Rint_constant.

apply HV.
apply Rle_trans with (X - Y).
assert(Hcbpos : x : R, c x b → 0 f x).
intros x [H1 H2]; apply Hpos; split;[apply Rle_trans with c| ]; intuition.
pose proof (Rint_pos _ _ _ _ (proj2 Hacb) Hcbpos HZ') as H.
assert(0 X - Y - T).
assert(Hdbpos : x : R, d x b → 0 f x).
intros x [H1 H2]; apply Hpos; split;[apply Rle_trans with d| ]; intuition.
apply (Rint_pos _ _ _ _ (proj2 Hadb) Hdbpos HT').
fourier.
assert(Hacpos : x : R, a x c → 0 f x).
intros x [H1 H2]; apply Hpos; split; [ | apply Rle_trans with c]; intuition.
pose proof (Rint_pos _ _ _ _ (proj1 Hacb) Hacpos HY) as H.
assert(0 X - Y - T).
assert(Hdbpos : x : R, d x b → 0 f x).
intros x [H1 H2]; apply Hpos; split;[apply Rle_trans with d| ]; intuition.
apply (Rint_pos _ _ _ _ (proj2 Hadb) Hdbpos HT').
fourier.
Qed.

A non negative function with null integral in a non trivial segment is null on it

Lemma Rint_continuous_pos_eq_0 : f a b,
a < b
( x, a x bcontinuity_pt f x) →
( x, a x b → 0 f x) →
Rint f a b 0 → ( x, a x bf x = 0).
Proof.
intros f a b Hab Hcont Hpos Hint x Hx.
case (Req_dec (f x) 0); intro Hcase.
apply Hcase.
pose proof Rint_continuous_gt_0 _ _ _ _ 0 Hab Hx Hcont Hpos Hcase Hint as pr.
exact (False_ind _ (Rlt_irrefl 0 pr)).
Qed.

Cauchy-Schwarz's theorem for integrals

Lemma Rint_Cauchy_Schwarz : f g a b x y z,
a b
( x, a x bcontinuity_pt f x) →
( x, a x bcontinuity_pt g x) →
Rint (f × f)%F a b xRint (g × g)%F a b yRint (f × g)%F a b z
z^2 x × y.
Proof.
intros f g a b x y z Hle Hfc Hgc Hf Hg Hfg.
assert (H0 : {y = 0} + {y 0}).
destruct (total_order_T y 0) as [[H|H]|H].
right; apply Rlt_not_eq; assumption.
left; assumption.
right; apply Rgt_not_eq; assumption.
destruct H0 as [H0|H0].
assert (Hz : z = 0).
destruct (Rle_lt_or_eq_dec a b Hle); [|
subst; apply (Rint_uniqueness (f × g)%F b b z 0 Hfg
(Rint_singleton (f × g)%F b))].
eapply Rint_uniqueness; [apply Hfg|].
eapply Rint_eq_compat with (fun _ ⇒ 0).
intros.
unfold mult_fct.
apply Rmult_eq_0_compat_l.
apply Rsqr_eq_0_reg.
replace (g x0 × g x0) with ((g × g)%F x0) by auto.
replace (Rmin a b) with a in × by (symmetry; apply Rmin_def; apply Hle).
replace (Rmax a b) with b in × by (symmetry; apply Rmax_def; apply Hle).
apply Rint_continuous_pos_eq_0 with a b; auto.
intros; apply continuity_pt_mult; apply Hgc; assumption.
intros; apply Rle_0_sqr.
subst; assumption.
pose (fun _:R ⇒ 0) as null; fold null.
replace 0 with (0 × (b - a)) by ring.
apply Rint_constant.
subst y; subst z.
repeat rewrite Rmult_0_r.
rewrite pow_ne_zero; auto with ×.
assert (Hy : 0 y).
eapply Rint_pos with (f := (g × g)%F).
eexact Hle.
intros u Hu; apply Rle_0_sqr.
assumption.
pose (F k x := (f x - k × g x).
assert (Hpos : k i, Rint (F k) a b i → 0 i).
intros k i H.
eapply Rint_pos with (f := F k).
eexact Hle.
intros u Hu; apply Rle_0_sqr.
assumption.
assert (Heq : k, Rint (F k) a b (x - 2 × k × z + k² × y)).
intros k.
apply Rint_eq_compat with (f := ((f × f) - (fct_cte (2 × k)) × (f × g) + (fct_cte k² )* (g × g))%F).
intros; unfold fct_cte, F, plus_fct, mult_fct, minus_fct, Rsqr; ring.
auto with Rint.
assert (Hcs : 0 x - z² / y).
eapply Hpos.
replace (x - z² / y) with (x - 2 × (z / y) × z + (z / y × y).
apply Heq.
unfold Rsqr; field; assumption.
apply Rle_ge in Hcs; apply Rminus_ge in Hcs; apply Rge_le in Hcs.
apply Rmult_le_compat_r with (r := y) in Hcs; [|assumption].
replace (z² / y × y) with z² in Hcs by (field; assumption).
unfold Rsqr in Hcs.
ring_simplify in Hcs.
apply Hcs.
Qed.

Fundamental theorem of real analysis

Lemma Rint_derive : f a b d,
a b
( x, a x bderivable_pt_abs f x (d x)) →
( x, a x bcontinuity_pt d x) →
Rint d a b (f b - f a).
Proof.
intros f a b d Hab Hder Hcont.
pose proof prolongement_C1_C1 f d a b Hab Hder Hcont as [g [Heq Hdeq]].
apply Rint_eq_compat with (derive g (diff0 g)).
rewrite Rmin_def, Rmax_def; assumption.
(RiemannInt_P32 g a b).
rewrite RiemannInt_P33; intuition.
do 2 (rewrite Heq; intuition).
Qed.

Lemma Rint_derive2 : f a b d,
( x, Rmin a b x Rmax a bderivable_pt_abs f x (d x)) →
( x, Rmin a b x Rmax a bcontinuity_pt d x) →
Rint d a b (f b - f a).
Proof.
intros f a b d Hder Hcont.
destruct (Rle_dec a b) as [n|n].
rewrite Rmin_def, Rmax_def in *; try assumption.
apply Rint_derive; assumption.
apply Rnot_le_lt, Rlt_le in n.
rewrite Rmin_comm, Rmax_comm, Rmin_def, Rmax_def in *; try assumption.
apply Rint_reverse_1; replace (- (f b - f a)) with (f a - f b) by ring.
apply Rint_derive; assumption.
Qed.

Integration by parts

Lemma Rint_parts : f g a b f' g' Ifg' If'g,
a b
( x : R, a x bderivable_pt_lim f x (f' x)) →
( x : R, a x bderivable_pt_lim g x (g' x)) →
( x : R, a x bcontinuity_pt f' x) →
( x : R, a x bcontinuity_pt g' x) →
Rint (f × g')%F a b Ifg'Rint (f' × g)%F a b If'g
Ifg' = f b × g b - f a × g a - If'g.
Proof.
intros f g a b f' g' Ifg' If'g Hab Hderf Hderg Hcontf' Hcontg' Hfg' Hf'g.
assert (H : a b c, a + b = ca = c - b) by (intros; subst; ring);
apply H; clear H.
apply Rint_uniqueness with (f × g' + f' × g)%F a b.
apply Rint_plus; assumption.
replace (f b × g b - f a × g a) with ((f × g)%F b - (f × g)%F a) by reflexivity.

apply Rint_derive.
assumption.

intros; unfold mult_fct, plus_fct; rewrite Rplus_comm;
apply derivable_pt_lim_mult; intuition.

intros; apply continuity_pt_plus;
apply continuity_pt_mult; try intuition;
apply derivable_continuous_pt.
(f' x); apply Hderf; intuition.
(g' x); apply Hderg; intuition.
Qed.

Variable change theorem

Lemma Rint_substitution : f g g' a b I,
a b → ( x, a x bg a g x g b) →
( x, g a x g bcontinuity_pt f x) →
( x, a x bderivable_pt_lim g x (g' x)) →
( x, a x bcontinuity_pt g' x) →
Rint (fun xf (g x) × g' x) a b I
Rint f (g a) (g b) I.
Proof.
intros f g g' a b I Hab Habgab Hcontf Hder Hcontg' HI.
destruct (Habgab a) as [_ Hgab]; auto with ×.

assert (Hpr : x : R, g a xx g bRiemann_integrable f (g a) x).
intros.
apply continuity_implies_RiemannInt; trivial.
intros; apply Hcontf; split.
tauto.
apply Rle_trans with x; intuition; trivial.

pose (primitive Hgab (FTC_P1 Hgab Hcontf)) as F.

assert(Hfab : Riemann_integrable f (g a) (g b)).
apply Hpr; auto with ×.

assert(HF := RiemannInt_P20 Hgab (FTC_P1 Hgab Hcontf) Hfab).

assert(Heq : Rint f (g a) (g b) (F(g b) - (F(g a)))).
unfold F; rewrite <- HF.
apply Rint_RiemannInt_link.
replace I with (comp F g b - comp F g a).
apply Heq.

symmetry.
eapply Rint_uniqueness.
apply HI.

apply Rint_derive.
trivial.
intros.
apply derivable_pt_lim_comp.
auto.
apply RiemannInt_P28; auto.

intros.
apply continuity_pt_mult.
apply continuity_pt_comp.
apply derivable_continuous_pt.
(g' x); apply Hder; apply H.

auto.

auto.
Qed.

End Rint_props.