Library Coquelicot.RInt_gen

This file is part of the Coquelicot formalization of real analysis in Coq: http://coquelicot.saclay.inria.fr/
Copyright (C) 2011-2015 Sylvie Boldo
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2020 Guillaume Melquiond
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.
This file describes improper integrals, such as integrals with an infinity endpoint or integrals of a function with a singularity. A few properties are given: Chasles, operations, composition, derivation.

Open Scope R_scope.

Improper Riemann integral


Section is_RInt_gen.

Context {V : NormedModule R_AbsRing}.

Definition is_RInt_gen (f : R V) (Fa Fb : (R Prop) Prop) (l : V) :=
  filterlimi (fun abis_RInt f (fst ab) (snd ab)) (filter_prod Fa Fb) (locally l).
Definition ex_RInt_gen (f : R V) (Fa Fb : (R Prop) Prop) :=
   l : V, is_RInt_gen f Fa Fb l.

Definition is_RInt_gen_at_point f a b l :
  is_RInt_gen f (at_point a) (at_point b) l
     is_RInt f a b l.

Basic properties of integrals


Lemma is_RInt_gen_ext {Fa Fb : (R Prop) Prop}
  {FFa : Filter Fa} {FFb : Filter Fb} (f g : R V) (l : V) :
  filter_prod Fa Fb (fun ab x, Rmin (fst ab) (snd ab) < x < Rmax (fst ab) (snd ab)
                                f x = g x)
  is_RInt_gen f Fa Fb l is_RInt_gen g Fa Fb l.

Lemma ex_RInt_gen_ext {Fa Fb : (R Prop) Prop}
  {FFa : Filter Fa} {FFb : Filter Fb} (f g : R V) :
  filter_prod Fa Fb (fun ab x, Rmin (fst ab) (snd ab) < x < Rmax (fst ab) (snd ab)
                                f x = g x)
  ex_RInt_gen f Fa Fb ex_RInt_gen g Fa Fb.

Lemma ex_RInt_gen_ext_eq {Fa Fb : (R Prop) Prop}
  {FFa : Filter Fa} {FFb : Filter Fb} (f g : R V) :
  ( x, f x = g x) ex_RInt_gen f Fa Fb ex_RInt_gen g Fa Fb.

Lemma is_RInt_gen_point (f : R V) (a : R) :
  is_RInt_gen f (at_point a) (at_point a) zero.

Lemma is_RInt_gen_swap {Fa Fb : (R Prop) Prop}
  {FFa : Filter Fa} {FFb : Filter Fb} (f : R V) (l : V) :
  is_RInt_gen f Fb Fa l is_RInt_gen f Fa Fb (opp l).

Lemma is_RInt_gen_Chasles {Fa Fc : (R Prop) Prop}
  {FFa : Filter Fa} {FFc : Filter Fc}
  (f : R V) (b : R) (l1 l2 : V) :
  is_RInt_gen f Fa (at_point b) l1 is_RInt_gen f (at_point b) Fc l2
   is_RInt_gen f Fa Fc (plus l1 l2).

Lemma ex_RInt_gen_Chasles :
   {Fa Fc : (R Prop) Prop},
   {FFa : Filter Fa} {FFc : Filter Fc},
   (f : R V) (b : R),
  ex_RInt_gen f Fa (at_point b)
  ex_RInt_gen f (at_point b) Fc
  ex_RInt_gen f Fa Fc.

Composition



Operations


Lemma is_RInt_gen_scal {Fa Fb : (R Prop) Prop}
  {FFa : Filter Fa} {FFb : Filter Fb} (f : R V) (k : R) (l : V) :
  is_RInt_gen f Fa Fb l
  is_RInt_gen (fun yscal k (f y)) Fa Fb (scal k l).

Lemma is_RInt_gen_opp {Fa Fb : (R Prop) Prop}
  {FFa : Filter Fa} {FFb : Filter Fb} (f : R V) (l : V) :
  is_RInt_gen f Fa Fb l
  is_RInt_gen (fun yopp (f y)) Fa Fb (opp l).

Lemma is_RInt_gen_plus {Fa Fb : (R Prop) Prop}
  {FFa : Filter Fa} {FFb : Filter Fb} (f g : R V) (lf lg : V) :
  is_RInt_gen f Fa Fb lf
  is_RInt_gen g Fa Fb lg
  is_RInt_gen (fun yplus (f y) (g y)) Fa Fb (plus lf lg).

Lemma is_RInt_gen_minus {Fa Fb : (R Prop) Prop}
  {FFa : Filter Fa} {FFb : Filter Fb} (f g : R V) (lf lg : V) :
  is_RInt_gen f Fa Fb lf
  is_RInt_gen g Fa Fb lg
  is_RInt_gen (fun yminus (f y) (g y)) Fa Fb (minus lf lg).

End is_RInt_gen.

Section RInt_gen.

Context {V : CompleteNormedModule R_AbsRing}.

Definition RInt_gen (f : R V) (a b : (R Prop) Prop) :=
  iota (is_RInt_gen f a b).

Lemma is_RInt_gen_unique {Fa Fb : (R Prop) Prop}
  {FFa : ProperFilter' Fa} {FFb : ProperFilter' Fb} (f : R V) (l : V) :
  is_RInt_gen f Fa Fb l RInt_gen f Fa Fb = l.

Lemma RInt_gen_correct {Fa Fb : (R Prop) Prop}
  {FFa : ProperFilter' Fa} {FFb : ProperFilter' Fb} (f : R V) :
  ex_RInt_gen f Fa Fb is_RInt_gen f Fa Fb (RInt_gen f Fa Fb).

Lemma RInt_gen_norm {Fa Fb : (R Prop) Prop}
  {FFa : ProperFilter Fa} {FFb : ProperFilter Fb} (f : R V) (g : R R) (lf : V) (lg : R) :
  filter_prod Fa Fb (fun abfst ab snd ab)
  filter_prod Fa Fb (fun ab x, fst ab x snd ab norm (f x) g x)
  is_RInt_gen f Fa Fb lf is_RInt_gen g Fa Fb lg
  norm lf lg.

Lemma RInt_gen_ext {Fa Fb : (R Prop) Prop}
  {FFa : ProperFilter Fa} {FFb : ProperFilter Fb} (f g : R V) :
  filter_prod Fa Fb (fun ab x, Rmin (fst ab) (snd ab) < x < Rmax (fst ab) (snd ab)
                                f x = g x)
  ex_RInt_gen f Fa Fb RInt_gen f Fa Fb = RInt_gen g Fa Fb.

Lemma RInt_gen_ext_eq {Fa Fb : (R Prop) Prop}
  {FFa : ProperFilter Fa} {FFb : ProperFilter Fb} (f g : R V):
  ( x, f x = g x)
  ex_RInt_gen f Fa Fb RInt_gen f Fa Fb = RInt_gen g Fa Fb.

Lemma RInt_gen_Chasles :
   {Fa Fc : (R Prop) Prop},
   {FFa : ProperFilter' Fa} {FFc : ProperFilter' Fc},
   (f : R V) (b : R),
  ex_RInt_gen f Fa (at_point b)
  ex_RInt_gen f (at_point b) Fc
  plus (RInt_gen f Fa (at_point b)) (RInt_gen f (at_point b) Fc) = RInt_gen f Fa Fc.

End RInt_gen.

Lemma is_RInt_gen_Derive {Fa Fb : (R Prop) Prop} {FFa : Filter Fa} {FFb : Filter Fb}
  (f : R R) (la lb : R) :
  filter_prod Fa Fb
    (fun ab x : R, Rmin (fst ab) (snd ab) x Rmax (fst ab) (snd ab) ex_derive f x)
   filter_prod Fa Fb
    (fun ab x : R, Rmin (fst ab) (snd ab) x Rmax (fst ab) (snd ab) continuous (Derive f) x)
   filterlim f Fa (locally la) filterlim f Fb (locally lb)
   is_RInt_gen (Derive f) Fa Fb (lb - la).

Section Complements_RInt_gen.

Context {V : CompleteNormedModule R_AbsRing}.

Lemma ex_RInt_gen_at_point f a b : @ex_RInt_gen V f (at_point a) (at_point b) ex_RInt f a b.

Lemma RInt_gen_at_point f a b :
  ex_RInt f a b @RInt_gen V f (at_point a) (at_point b) = RInt f a b.

End Complements_RInt_gen.