Library CoqApprox.xreal_ssr_compat

This file is part of the CoqApprox formalization of rigorous polynomial approximation in Coq: http://tamadi.gforge.inria.fr/CoqApprox/
Copyright (c) 2010-2013, ENS de Lyon and 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.

Require Import Reals.
Require Import Psatz.
Require Import taylor_thm.
Require Import Interval_missing.
Require Import Interval_xreal.
Require Import Interval_xreal_derive.
Require Import Interval_interval.
Require Import Interval_generic_proof.
Require Import Rstruct.
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
Require Import div fintype finfun path bigop choice ssralg.

Set Implicit Arguments.

Delimit Scope ring_scope with Ri.
Delimit Scope R_scope with Re.
Delimit Scope XR_scope with XR.

Local Open Scope XR_scope.

Notation "x + y" := (Xadd x y) : XR_scope.
Notation "x - y" := (Xsub x y) : XR_scope.
Notation " - y" := (Xneg y) : XR_scope.
Notation "x * y" := (Xmul x y) : XR_scope.
Notation "x / y" := (Xdiv x y) : XR_scope.

Definition Xpow x n := Xpower_int x (Z_of_nat n).

Notation "x ^ n" := (Xpow x n) : XR_scope.



Implicit Types n k : nat.
Implicit Type r : R.
Implicit Types x y : ExtendedR.
Implicit Type X : interval.

Definition Xpow_iter x n := iter_nat n _ (Xmul x) (Xmask (Xreal 1) x).

Lemma Xpow_idem x n : Xpow x n = Xpow_iter x n.

Lemma Xpow_Xreal r n : Xpow_iter (Xreal r) n = Xreal (pow r n).

Lemma Xpow_Xnan n : Xpow_iter Xnan n = Xnan.

Lemma Xmul_Xreal a b : Xreal a * Xreal b = Xreal (a * b).

Lemma zeroF r : (r <> 0)%Re -> is_zero r = false.

Lemma zeroT r : (r = 0)%Re -> is_zero r = true.

Lemma fact_zeroF i : is_zero (INR (fact i)) = false.

Lemma XReq_EM_T : forall r1 r2:ExtendedR, {r1 = r2} + {r1 <> r2}.

Definition eqX x1 x2 : bool :=
  match XReq_EM_T x1 x2 with
    | left _ => true
    | right _ => false
  end.

Lemma eqXP : Equality.axiom eqX.

Canonical Structure Xreal_eqMixin := EqMixin eqXP.
Canonical Structure Xreal_eqType := Eval hnf in
  EqType ExtendedR Xreal_eqMixin.

Lemma Xreal_irrelevance (x y : ExtendedR) (E E' : x = y) : E = E'.

Lemma XaddA : associative Xadd.

Lemma XaddC : commutative Xadd.

Lemma Xadd0 : left_id (Xreal 0%Re) Xadd.

Lemma X0add : right_id (Xreal 0%Re) Xadd.

Lemma XmulA : associative Xmul.

Lemma Xmul0 : left_id (Xreal 1%Re) Xmul.

Lemma X0mul : right_id (Xreal 1%Re) Xmul.

Lemma left_distr_Xmul_Xadd : left_distributive Xmul Xadd.

Lemma right_distr_Rmult_Rplus : right_distributive Xmul Xadd.

Lemma XmulC : commutative Xmul.

Import Monoid.
Canonical Xadd_monoid := Law XaddA Xadd0 X0add.
Canonical Xadd_comoid := ComLaw XaddC.

Canonical Xmul_monoid := Law XmulA Xmul0 X0mul.
Canonical Xmul_comoid := ComLaw XmulC.

Lemma ordinal1 : all_equal_to (ord0 : 'I_1).

Local Open Scope XR_scope.

Lemma Xderive_pt_Xpow n (f : ExtendedR -> ExtendedR) (f' x : ExtendedR) :
  Xderive_pt f x f' ->
  Xderive_pt (fun x0 : ExtendedR => (f x0) ^ n) x
 ((Xreal (INR n)) * (f x) ^ n.-1 * f').

Lemma Xderive_pt_mulXmask r x :
  Xderive_pt
  (fun x0 => ((Xreal r) * Xmask (Xreal 1) x0)%XR) x
  (Xmask (Xreal 0) x).

Lemma not_Xnan_Xreal_fun T F :
  (forall i : T, F i <> Xnan) ->
  exists g, forall i : T, F i = Xreal (g i).

Lemma bigXadd_Xnan n (F : 'I_n -> ExtendedR) :
  \big[Xadd/Xreal 0]_(i < n) F i = Xnan ->
  exists i, F i = Xnan.

Lemma bigXadd_Xnan_i n (F : 'I_n -> ExtendedR) i :
  F i = Xnan -> \big[Xadd/Xreal 0]_(i < n) F i = Xnan.

Lemma bigXadd_Xreal n (F : 'I_n -> ExtendedR) sx:
  \big[Xadd/Xreal 0]_(i < n) F i = Xreal sx ->
  forall i, exists gi, F i = Xreal (gi).

Lemma bigXadd_Xreal1 n (F : 'I_n -> ExtendedR) r :
  \big[Xadd/Xreal 0]_(i < n) F i = Xreal r ->
  exists g : 'I_n -> R, forall i, F i = Xreal (g i).

Lemma bigXadd_Xreal_i n (g : 'I_n -> R) :
  \big[Xadd/Xreal 0]_(i < n) Xreal (g i) =
  Xreal (\big[Rplus/R0]_(i < n) g i).

Lemma sum_f_to_big n (f : nat -> R) :
  sum_f_R0 f n = \big[Rplus/R0]_(i < n.+1) f i.

Lemma big_Xmul_Xadd_distr n (f : 'I_n -> ExtendedR) r :
  ((\big[Xadd/Xreal 0]_(i < n) f i) * (Xreal r)
  = \big[Xadd/Xreal 0]_(i < n) (f i * (Xreal r)))%XR.

Lemma contains_Xnan (X : interval) :
  contains X Xnan -> X = Interval_interval.Inan.

Lemma Xsub_Xadd_distr (a b c : ExtendedR) : (a - (b + c) = a - b - c)%XR.

Lemma Xinv_1 : Xinv (Xreal 1%Re)= Xreal 1%Re.

Section NDerive.
Variable XD : nat -> ExtendedR -> ExtendedR.
Variable X : interval.
Variable n : nat.
Let dom r := contains X (Xreal r).
Let Hdom : connected dom.

Hypothesis Hder : forall n, Xderive (XD n) (XD (S n)).

Hypothesis Hdif : forall r k, (k <= n.+1)%N -> dom r -> XD k (Xreal r) <> Xnan.

Hypothesis XD0_Xnan : XD 0%N Xnan = Xnan.

Lemma XD_Xnan_propagate x (k m : nat) :
  (k <= m)%N -> XD k x = Xnan -> XD m x = Xnan.

Lemma XD_Xreal k r :
  (k <= n.+1)%N -> dom r ->
  XD k (Xreal r) = Xreal (proj_val (XD k (Xreal r))).

Theorem Rneq_lt r1 r2 : r1 <> r2 -> (r1 < r2 \/ r2 < r1)%Re.

Lemma Xderive_propagate (f f' : ExtendedR -> ExtendedR) x :
  Xderive f f' -> f x = Xnan -> f' x = Xnan.

Lemma Xderive_propagate' (f f' : ExtendedR -> ExtendedR) :
  Xderive f f' -> f' Xnan = Xnan.

Lemma bigXadd_bigRplus (r s : R) :
  dom r ->
  let xi0 := Xreal r in
  \big[Xadd/Xreal 0]_(i < n.+1)
    ((XD i xi0) / Xreal (INR (fact i)) * Xreal s ^ i)%XR =
  Xreal (\big[Rplus/R0]_(i < n.+1)
    (proj_val (XD i xi0) / (INR (fact i)) * s ^ i)%Re).

Lemma Xsub_Xreal_l x y :
  Xsub x y <> Xnan -> x = Xreal (proj_val x).

Lemma Xsub_Xreal_r x y :
  Xsub x y <> Xnan -> y = Xreal (proj_val y).

Lemma Xsub_Xnan_r x :
  Xsub x Xnan = Xnan.

Theorem XTaylor_Lagrange x0 x :
  contains X x0 ->
  contains X x ->
  exists xi : R,
  contains X (Xreal xi) /\
  (XD 0 x - (\big[Xadd/Xreal 0]_(i < n.+1)
    (XD i x0 / Xreal (INR (fact i)) * (x - x0)^i)))%XR =
  (XD n.+1 (Xreal xi) / Xreal (INR (fact n.+1)) * (x - x0) ^ n.+1)%XR /\
  (contains (Interval_interval.Ibnd x x0) (Xreal xi) \/
   contains (Interval_interval.Ibnd x0 x) (Xreal xi)).

End NDerive.