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.

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 ptdpointed_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 ptdscal (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 : Rc) a b (scal (b-a) c).

Lemma ex_KHInt_const :
   (a b : R) (c : V),
  ex_KHInt (fun x : Rc) 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.