Library Coqtail.Reals.Rintegral


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.