Library Interval.Integral.Integral

This file is part of the Coq.Interval library for proving bounds of real-valued expressions in Coq: https://coqinterval.gitlabpages.inria.fr/

Copyright (C) 2015-2016, Inria

This library is governed by the CeCILL-C license under French law and abiding by the rules of distribution of free software. You can use, modify and/or redistribute the library under the terms of the CeCILL-C license as circulated by CEA, CNRS and Inria at the following URL: http://www.cecill.info/

As a counterpart to the access to the source code and rights to copy, modify and redistribute granted by the license, users are provided only with a limited warranty and the library's author, the holder of the economic rights, and the successive licensors have only limited liability. See the COPYING file for more details.

From Coq Require Import Reals List Psatz.
From Coquelicot Require Import Coquelicot.
From mathcomp.ssreflect Require Import ssreflect ssrfun ssrbool.

Require Import Stdlib.
Require Import Coquelicot.
Require Import Xreal.
Require Import Interval.
Require Import Taylor_model.
Require Import Interval_compl.

Section Missing.

Lemma filter_prod_at_point_infty :
  ∀ a (P : R → R → Prop),
  (∀ x y, a ≤ x ≤ y → P x y ) →
  filter_prod (at_point a) (Rbar_locally p_infty)
  (fun ab : R × R ⇒ P ab .1 ab .2).

Lemma filter_prod_at_point :
  ∀ {T F} { FF : Filter F} a (P : R → T → Prop) Q,
  F Q →
  (∀ y, Q y → P a y ) →
  filter_prod (at_point a) F
  (fun ab : R × T ⇒ P ab .1 ab .2).

Lemma filter_prod_at_point_l :
  ∀ {T F} { FF : Filter F} a (P : T → R → Prop) Q,
  F Q →
  (∀ y, Q y → P y a ) →
  filter_prod F (at_point a)
  (fun ab : T × R ⇒ P ab .1 ab .2).

Lemma at_point_filter_prod :
  ∀ {T F} { FF : Filter F} a (P : R → T → Prop),
  filter_prod (at_point a) F
              (fun ab : R × T ⇒ P ab .1 ab .2) →
  F (P a).

Lemma at_point_filter_prod_l :
  ∀ {T F} { FF : Filter F} a (P : T → R → Prop),
  filter_prod F (at_point a)
              (fun ab : T × R ⇒ P ab .1 ab .2) →
  F (fun y ⇒ P y a).

Lemma filterlimi_const_loc {T} {U : UniformSpace}
  {F : (T → Prop) → Prop} {FF : Filter F} :
  ∀ (f : T → U → Prop) (a : U),
  F (fun x ⇒ f x a) →
  filterlimi f F (locally a).

Lemma filterlimi_const {T} {U : UniformSpace}
  {F : (T → Prop) → Prop} {FF : Filter F} :
  ∀ (f : T → U → Prop) (a : U),
  (∀ x, f x a ) →
  filterlimi f F (locally a).

Lemma is_RInt_gen_0 {Fa Fb : (R → Prop) → Prop}
  {FFa : Filter Fa} {FFb : Filter Fb} :
  is_RInt_gen (fun y ⇒ 0) Fa Fb zero.

Lemma is_RInt_gen_filterlim {V : CompleteNormedModule R_AbsRing}
  {Fa Fb : (R → Prop) → Prop}
  {FFa : ProperFilter Fa} {FFb : ProperFilter Fb} (f : R → V) (lf : V) :
  is_RInt_gen f Fa Fb lf →
  filterlim (fun x ⇒ RInt f x .1 x .2) (filter_prod Fa Fb) (locally lf).

Lemma ex_RInt_ex_RInt_gen {V : CompleteNormedModule R_AbsRing}
  {Fa Fb : (R → Prop) → Prop}
  {FFa : ProperFilter Fa} {FFb : ProperFilter Fb} (f : R → V) :
  ex_RInt_gen f Fa Fb →
  (filter_prod Fa Fb (fun ab ⇒ ex_RInt f ab .1 ab .2)).

Lemma RInt_gen_le {Fa Fb : (R → Prop) → Prop}
  {FFa : ProperFilter Fa} {FFb : ProperFilter Fb} (f : R → R) (g : R → R) (lf : R) (lg : R) :
  filter_prod Fa Fb (fun ab ⇒ fst ab ≤ snd ab)
  → filter_prod Fa Fb (fun ab ⇒ ∀ x, fst ab ≤ x ≤ snd ab → f x ≤ g x)
  → is_RInt_gen f Fa Fb lf → is_RInt_gen g Fa Fb lg
    → lf ≤ lg.

Lemma ex_RInt_gen_cauchy {V : CompleteNormedModule R_AbsRing}
  {Fb : (R → Prop) → Prop} {FFb : ProperFilter Fb}
  (a : R) (f : R → V) :
  ex_RInt_gen f (at_point a) Fb ↔
  (filter_prod (at_point a) Fb (fun ab ⇒ ex_RInt f ab .1 ab .2) ∧
   ∀ eps : posreal, ∃ P ,
     Fb P ∧
     (∀ u v,
        P u → P v →
        ∀ I, is_RInt f u v I → norm I ≤ eps )).

Lemma ex_RInt_gen_cauchy_left {V : CompleteNormedModule R_AbsRing}
  {Fb : (R → Prop) → Prop} {FFb : ProperFilter Fb}
  (a : R) (f : R → V) :
  ex_RInt_gen f Fb (at_point a) ↔
  (filter_prod Fb (at_point a) (fun ab ⇒ ex_RInt f ab .1 ab .2) ∧
   ∀ eps : posreal, ∃ P ,
     Fb P ∧
     (∀ u v,
        P u → P v →
        ∀ I, is_RInt f u v I → norm I ≤ eps )).

Lemma at_right_le_at_point a b (Hab : a < b) : (filter_prod (at_right a) (at_point b) (fun x ⇒ x .1 ≤ x .2)).

Lemma RInt_gen_pos
  {Fa : (R → Prop) → Prop} {FFa : ProperFilter Fa}
  {Fb : (R → Prop) → Prop} {FFb : ProperFilter Fb}
  (P Q : R → Prop) (f : R → R) (If : R) :
  (Fa P ) →
  (Fb Q ) →
  (∀ x y z, P x → Q y → x ≤ z ≤ y → 0 ≤ f z ) →
  filter_prod Fa Fb (fun ab : R × R ⇒ ab .1 ≤ ab .2) →
  is_RInt_gen f Fa Fb If →
  0 ≤ If.

Lemma RInt_gen_neg
  {Fa : (R → Prop) → Prop} {FFa : ProperFilter Fa}
  {Fb : (R → Prop) → Prop} {FFb : ProperFilter Fb}
  (P Q : R → Prop) (f : R → R) (If : R) :
  (Fa P ) →
  (Fb Q ) →
  (∀ x y z, P x → Q y → x ≤ z ≤ y → f z ≤ 0) →
  filter_prod Fa Fb (fun ab : R × R ⇒ ab .1 ≤ ab .2) →
  is_RInt_gen f Fa Fb If →
  If ≤ 0.

End Missing.

Module IntegralTactic (I : IntervalOps).

Module J := IntervalExt I.

Lemma bounded_ex {xi} (Hne : not_empty (I.convert xi)) (Hbnded : I.bounded xi) :
  (∃ l u : R , I.convert xi = Ibnd (Xreal l) (Xreal u)).

Lemma at_right_open_interval a lb : (lb < a ) → at_right lb (fun x : R ⇒ lb < x < a).

Lemma at_right_semi_open_interval a lb : (lb < a ) → at_right lb (fun x : R ⇒ lb < x ≤ a).

Definition constant_sign (S : R → Prop) (f : R → R) :=
  (∀ x, S x → 0 ≤ f x ) ∨ (∀ x, S x → f x ≤ 0).

Lemma is_RInt_le_0 :
∀ (f : R → R) (a b If : R),
a ≤ b →
is_RInt f a b If → (∀ x : R, a < x < b → f x ≤ 0) → If ≤ 0.

Lemma is_RInt_const_sign (f : R → R) (If : R) a b (le_ab : a ≤ b) :
  constant_sign (fun x ⇒ Rmin a b ≤ x ≤ Rmax a b) f →
  is_RInt f a b If →
  is_RInt (fun x ⇒ Rabs (f x)) a b (Rabs If).

Lemma integral_interval_mul_sing :
  ∀ prec sing a ia f fi g Ig Igi,
  (sing < a ) →
  contains (I.convert ia) (Xreal a) →
  (∀ x, sing ≤ x ≤ a → contains (I.convert fi) (Xreal (f x))) →
  I.bounded fi →
  (∀ x, sing ≤ x ≤ a → continuous f x ) →
  (∀ x, sing < x ≤ a → continuous g x ) →
  constant_sign (fun x ⇒ sing < x ≤ a) g →
  is_RInt_gen g (at_right sing) (at_point a) Ig →
  contains (I.convert Igi) (Xreal Ig) →
  ∃ Ifg ,
  is_RInt_gen (fun t ⇒ f t × g t) (at_right sing) (at_point a) Ifg ∧
  contains (I.convert (I.mul prec fi Igi)) (Xreal Ifg).

Lemma integral_interval_mul_zero :
  ∀ prec a ia f fi g Ig Igi,
  (0 < a ) →
  contains (I.convert ia) (Xreal a) →
  (∀ x, 0 ≤ x ≤ a → contains (I.convert fi) (Xreal (f x))) →
  I.bounded fi →
  (∀ x, 0 ≤ x ≤ a → continuous f x ) →
  (∀ x, 0 < x ≤ a → continuous g x ) →
  constant_sign (fun x ⇒ 0 < x ≤ a) g →
  is_RInt_gen g (at_right 0) (at_point a) Ig →
  contains (I.convert Igi) (Xreal Ig) →
  ∃ Ifg ,
  is_RInt_gen (fun t ⇒ f t × g t) (at_right 0) (at_point a) Ifg ∧
  contains (I.convert (I.mul prec fi Igi)) (Xreal Ifg).

Lemma integral_interval_mul_infty :
  ∀ prec a ia f fi g Ig Igi,
  contains (I.convert ia) (Xreal a) →
  (∀ x, a ≤ x → contains (I.convert fi) (Xreal (f x))) →
  I.bounded fi →
  (∀ x, a ≤ x → continuous f x ) →
  (∀ x, a ≤ x → continuous g x ) →
  (∀ x, a ≤ x → 0 ≤ g x ) →
  is_RInt_gen g (at_point a) (Rbar_locally p_infty) Ig →
  contains (I.convert Igi) (Xreal Ig) →
  ∃ Ifg ,
  is_RInt_gen (fun t ⇒ f t × g t) (at_point a) (Rbar_locally p_infty) Ifg ∧
  contains (I.convert (I.mul prec fi Igi)) (Xreal Ifg).

End IntegralTactic.

Module IntegralTaylor (I : IntervalOps).

Module J := IntervalExt I.
Module TM := TM I.

Section DepthZeroPol.

Variable prec : I.precision.

Variables (f : R → R) (iF : I.type → I.type).

Hypothesis HiFIntExt : ∀ xi x, contains (I.convert xi) (Xreal x) → contains (I.convert (iF xi)) (Xreal (f x)).

Variable Mf : TM.TMI.rpa.
Variables X : I.type.
Let x0 := proj_val (I.F.convert (I.midpoint X)).
Let X0 := J.midpoint X.
Let iX := I.convert X.
Let iX0 := I.convert X0.

Hypothesis validMf : TM.TMI.i_validTM x0 iX Mf (fun x ⇒ Xreal (f x)).

Variables (a b : R).

Hypothesis Hintegrable : ex_RInt f a b.

Variables ia ib : I.type.

Hypothesis Hconta : contains (I.convert ia) (Xreal a).
Hypothesis Hcontb : contains (I.convert ib) (Xreal b).
Hypothesis Hcontxa : contains iX (Xreal a).
Hypothesis Hcontxb : contains iX (Xreal b).

Definition taylor_integral :=
  TM.TMI.integralEnclosure prec X0 Mf ia ib.

Definition taylor_integral_naive_intersection :=
  let temp := I.mul prec (I.sub prec ib ia) (iF (I.join ia ib)) in
  if I.real temp then I.meet temp taylor_integral else temp.

Lemma taylor_integral_correct :
  contains
    (I.convert taylor_integral)
    (Xreal (RInt f a b)).

Lemma taylor_integral_naive_intersection_correct :
  contains
    (I.convert taylor_integral_naive_intersection)
    (Xreal (RInt f a b)).

End DepthZeroPol.

End IntegralTaylor.