Library Interval.Interval.Interval_compl

This file is part of the CoqApprox formalization of rigorous polynomial approximation in Coq: http://tamadi.gforge.inria.fr/CoqApprox/

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 ZArith Reals Psatz.
From mathcomp.ssreflect Require Import ssreflect ssrbool ssrfun eqtype ssrnat bigop.
From Coquelicot Require Import Coquelicot.

Require Import Stdlib.
Require Import MathComp.
Require Import Xreal.
Require Import Interval.
Require Import Taylor.

Set Implicit Arguments.

Local Open Scope nat_scope.

Notation IInan := Interval.Inan (only parsing).

Some support results relating inequalities and contains

Definition intvl a b x := (a ≤ x ≤ b)%R.

Lemma intvl_connected a b : connected (intvl a b).

Lemma intvl_l l u x0 :
  intvl l u x0 → intvl l u l.

Lemma intvl_u l u x0 :
  intvl l u x0 → intvl l u u.

Lemma intvl_lVu l u x0 x :
  intvl l u x → intvl l u x0 → intvl l x0 x ∨ intvl x0 u x.

Some support results about monotonicity

Section PredArg.
Variable P : R → Prop.

Definition Rincr (f : R → R) :=
  ∀ x y : R,
  P x → P y →
  (x ≤ y → f x ≤ f y)%R.

Definition Rdecr (f : R → R) :=
  ∀ x y : R,
  P x → P y →
  (x ≤ y → f y ≤ f x)%R.

Definition Rmonot (f : R → R) :=
  Rincr f ∨ Rdecr f.

Definition Rpos_over (g : R → R) :=
  ∀ x : R, (P x → 0 ≤ g x)%R.

Definition Rneg_over (g : R → R) :=
  ∀ x : R, (P x → g x ≤ 0)%R.

Definition Rcst_sign (g : R → R) :=
  Rpos_over g ∨ Rneg_over g.

Definition Rderive_over (f f' : R → R) :=
  ∀ x : R, P x → is_derive f x (f' x).

Lemma Rderive_pos_imp_incr (f f' : R → R) :
  connected P → Rderive_over f f' → Rpos_over f' → Rincr f.

Lemma Rderive_neg_imp_decr (f f' : R → R) :
  connected P → Rderive_over f f' → Rneg_over f' → Rdecr f.

Lemma Rderive_cst_sign (f f' : R → R) :
  connected P → Rderive_over f f' → Rcst_sign f' → Rmonot f.

End PredArg.

Instantiation of Taylor.Cor_Taylor_Lagrange for intervals

Lemma sum_f_to_big n (f : nat → R) :
  sum_f_R0 f n = \big [Rplus /0%R]_(0 ≤ i < n .+1 ) f i.

Section NDerive.
Variable xf : R → ExtendedR.
Let f x := proj_val (xf x).
Let Dn := Derive_n f.
Variable dom : R → Prop.
Hypothesis Hdom : connected dom.
Variable n : nat.
Hypothesis Hdef : ∀ r, dom r → xf r ≠ Xnan.
Hypothesis Hder : ∀ n r, dom r → ex_derive_n f n r.

Theorem ITaylor_Lagrange x0 x :
  dom x0 →
  dom x →
  ∃ xi : R ,
  dom xi ∧
  (f x - \big [Rplus /0%R]_(0 ≤ i < n .+1 )
          (Dn i x0 / INR (fact i) × (x - x0 )^i ))%R =
  (Dn n .+1 xi / INR (fact n .+1) × (x - x0 ) ^ n .+1)%R ∧
  (x ≤ xi ≤ x0 ∨ x0 ≤ xi ≤ x)%R.

End NDerive.

The sequel of the file is parameterized by an implementation of intervals

Module IntervalAux (I : IntervalOps).

The following predicate will be used by Ztech.

Definition isNNegOrNPos (X : I.type) : bool :=
  if I.sign_large X is Xund then false else true.

Lemma isNNegOrNPos_false (X : I.type) :
  I.convert X = IInan → isNNegOrNPos X = false.

Definition gt0 xi : bool :=
  if I.sign_strict xi is Xgt then true else false.

Definition apart0 xi : bool :=
  match I.sign_strict xi with
  | Xlt | Xgt ⇒ true
  | _ ⇒ false
  end.

Lemma gt0_correct X x :
  contains (I.convert X) (Xreal x) → gt0 X → (0 < x)%R.

Lemma apart0_correct X x :
  contains (I.convert X) (Xreal x) → apart0 X → (x ≠ 0)%R.

Correctness predicates dealing with reals only, weaker than I.extension