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.
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2020 Guillaume Melquiond
From Coq Require Import Reals ssreflect.
Require Import Rbar Hierarchy RInt Lim_seq Continuity Derive Rcomplements RInt_analysis.
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.
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 ab ⇒ is_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.
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.
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 y ⇒ scal 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 y ⇒ opp (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 y ⇒ plus (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 y ⇒ minus (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 ab ⇒ fst 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.