Library Coquelicot.KHInt

This file is part of the Coquelicot formalization of real analysis in Coq: http://coquelicot.saclay.inria.fr/

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.

Require Import Reals mathcomp.ssreflect.ssreflect mathcomp.ssreflect.ssrbool mathcomp.ssreflect.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.