Library Coquelicot.KHInt
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-2015 Guillaume Melquiond
Copyright (C) 2014 Xavier Onfroy
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-2015 Guillaume Melquiond
Copyright (C) 2014 Xavier Onfroy
From Coq Require Import Reals ssreflect ssrbool.
From mathcomp Require Import seq.
Require Import Rcomplements Hierarchy SF_seq RInt.
This file describes the definition and properties of the
Henstock–Kurzweil (KH) integral.
Definition ith_step (ptd : @SF_seq R) i := nth 0 (SF_lx ptd) (S i) - nth 0 (SF_lx ptd) i.
Definition fine (delta : R → posreal) ptd :=
∀ i : nat, (i < SF_size ptd)%nat → ith_step ptd i < delta (nth 0 (SF_ly ptd) i).
Definition KH_filter (P : SF_seq → Prop) :=
∃ delta, ∀ ptd, fine delta ptd → P ptd.
Global Instance KH_filter_filter : Filter KH_filter.
Definition KH_fine (a b : R) :=
within (fun ptd ⇒ pointed_subdiv ptd ∧ SF_h ptd = Rmin a b ∧ last (SF_h ptd) (SF_lx ptd) = Rmax a b) KH_filter.
Lemma lub_cara :
∀ E l, is_lub E l → ∀ e : posreal, ¬ ¬ (∃ x, E x ∧ l - e < x).
Lemma cousin :
∀ a b delta, ¬ ¬ ∃ ptd,
pointed_subdiv ptd ∧ fine delta ptd ∧
SF_h ptd = Rmin a b ∧ last (SF_h ptd) (SF_lx ptd) = Rmax a b.
Global Instance KH_fine_proper_filter a b : ProperFilter' (KH_fine a b).
Section is_KHInt.
Context {V : NormedModule R_AbsRing}.
Definition is_KHInt (f : R → V) (a b : R) (If : V) :=
filterlim (fun ptd ⇒ scal (sign (b-a)) (Riemann_sum f ptd)) (KH_fine a b) (locally If).
Definition ex_KHInt f a b :=
∃ If : V, is_KHInt f a b If.
Lemma is_KHInt_point :
∀ (f : R → V) (a : R),
is_KHInt f a a zero.
Lemma ex_KHInt_point :
∀ (f : R → V) (a : R),
ex_KHInt f a a.
Lemma is_KHInt_const :
∀ (a b : R) (c : V),
is_KHInt (fun x : R ⇒ c) a b (scal (b-a) c).
Lemma ex_KHInt_const :
∀ (a b : R) (c : V),
ex_KHInt (fun x : R ⇒ c) a b.
End is_KHInt.
Section KHInt.
Context {V : CompleteNormedModule R_AbsRing}.
Definition KHInt (f : R → V) (a b : R) :=
iota (is_KHInt f a b).
Lemma KHInt_correct :
∀ (f : R → V) (a b : R),
ex_KHInt f a b → is_KHInt f a b (KHInt f a b).
Lemma is_KHInt_unique :
∀ (f : R → V) (a b : R) (l : V),
is_KHInt f a b l → KHInt f a b = l.
Lemma KHInt_point :
∀ (f : R → V) (a : R),
KHInt f a a = zero.
Lemma KHInt_const :
∀ (a b : R) (v : V),
KHInt (fun _ ⇒ v) a b = scal (b - a) v.
Lemma is_RInt_KHInt :
∀ (f : R → V) (a b : R) (l : V),
is_RInt f a b l → is_KHInt f a b l.
End KHInt.