# Library Coq.Reals.Ranalysis5

Require Import Rbase.
Require Import Ranalysis_reg.
Require Import Rfunctions.
Require Import Rseries.
Require Import Fourier.
Require Import RiemannInt.
Require Import SeqProp.
Require Import Max.
Local Open Scope R_scope.

# Preliminaries lemmas

Lemma f_incr_implies_g_incr_interv : forall f g:R->R, forall lb ub,
lb < ub ->
(forall x y, lb <= x -> x < y -> y <= ub -> f x < f y) ->
(forall x, f lb <= x -> x <= f ub -> (comp f g) x = id x) ->
(forall x , f lb <= x -> x <= f ub -> lb <= g x <= ub) ->
(forall x y, f lb <= x -> x < y -> y <= f ub -> g x < g y).
Lemma derivable_pt_id_interv : forall (lb ub x:R),
lb <= x <= ub ->
derivable_pt id x.
Lemma pr_nu_var2_interv : forall (f g : R -> R) (lb ub x : R) (pr1 : derivable_pt f x)
(pr2 : derivable_pt g x),
lb < ub ->
lb < x < ub ->
(forall h : R, lb < h < ub -> f h = g h) -> derive_pt f x pr1 = derive_pt g x pr2.
Lemma leftinv_is_rightinv_interv : forall (f g:R->R) (lb ub:R),
(forall x y, lb <= x -> x < y -> y <= ub -> f x < f y) ->
(forall y, f lb <= y -> y <= f ub -> (comp f g) y = id y) ->
(forall x, f lb <= x -> x <= f ub -> lb <= g x <= ub) ->
forall x,
lb <= x <= ub ->
(comp g f) x = id x.
Intermediate Value Theorem on an Interval (Proof mainly taken from Reals.Rsqrt_def) and its corollary
Lemma IVT_interv_prelim0 : forall (x y:R) (P:R->bool) (N:nat),
x < y ->
x <= Dichotomy_ub x y P N <= y /\ x <= Dichotomy_lb x y P N <= y.
Lemma IVT_interv_prelim1 : forall (x y x0:R) (D : R -> bool),
x < y ->
Un_cv (dicho_up x y D) x0 ->
x <= x0 <= y.
Lemma IVT_interv : forall (f : R -> R) (x y : R),
(forall a, x <= a <= y -> continuity_pt f a) ->
x < y ->
f x < 0 ->
0 < f y ->
{ z : R | x <= z <= y /\ f z = 0}.
Lemma f_interv_is_interv : forall (f:R->R) (lb ub y:R),
lb < ub ->
f lb <= y <= f ub ->
(forall x, lb <= x <= ub -> continuity_pt f x) ->
{ x | lb <= x <= ub /\ f x = y }.

## The derivative of a reciprocal function

# Continuity of the reciprocal function

Lemma continuity_pt_recip_prelim : forall (f g:R->R) (lb ub : R) (Pr1:lb < ub),
(forall x y, lb <= x -> x < y -> y <= ub -> f x < f y) ->
(forall x, lb <= x <= ub -> (comp g f) x = id x) ->
(forall a, lb <= a <= ub -> continuity_pt f a) ->
forall b,
f lb < b < f ub ->
continuity_pt g b.
Lemma continuity_pt_recip_interv : forall (f g:R->R) (lb ub : R) (Pr1:lb < ub),
(forall x y, lb <= x -> x < y -> y <= ub -> f x < f y) ->
(forall x, f lb <= x -> x <= f ub -> (comp f g) x = id x) ->
(forall x, f lb <= x -> x <= f ub -> lb <= g x <= ub) ->
(forall a, lb <= a <= ub -> continuity_pt f a) ->
forall b,
f lb < b < f ub ->
continuity_pt g b.

# Derivability of the reciprocal function

Lemma derivable_pt_lim_recip_interv : forall (f g:R->R) (lb ub x:R)
(Prf:forall a : R, g lb <= a <= g ub -> derivable_pt f a) (Prg : continuity_pt g x),
lb < ub ->
lb < x < ub ->
forall (Prg_incr:g lb <= g x <= g ub),
(forall x, lb <= x <= ub -> (comp f g) x = id x) ->
derive_pt f (g x) (Prf (g x) Prg_incr) <> 0 ->
derivable_pt_lim g x (1 / derive_pt f (g x) (Prf (g x) Prg_incr)).
Lemma derivable_pt_recip_interv_prelim0 : forall (f g : R -> R) (lb ub x : R)
(Prf : forall a : R, g lb <= a <= g ub -> derivable_pt f a),
continuity_pt g x ->
lb < ub ->
lb < x < ub ->
forall Prg_incr : g lb <= g x <= g ub,
(forall x0 : R, lb <= x0 <= ub -> comp f g x0 = id x0) ->
derive_pt f (g x) (Prf (g x) Prg_incr) <> 0 ->
derivable_pt g x.
Lemma derivable_pt_recip_interv_prelim1 :forall (f g:R->R) (lb ub x : R),
lb < ub ->
f lb < x < f ub ->
(forall x : R, f lb <= x -> x <= f ub -> comp f g x = id x) ->
(forall x : R, f lb <= x -> x <= f ub -> lb <= g x <= ub) ->
(forall x y : R, lb <= x -> x < y -> y <= ub -> f x < f y) ->
(forall a : R, lb <= a <= ub -> derivable_pt f a) ->
derivable_pt f (g x).
Lemma derivable_pt_recip_interv : forall (f g:R->R) (lb ub x : R)
(lb_lt_ub:lb < ub) (x_encad:f lb < x < f ub)
(f_eq_g:forall x : R, f lb <= x -> x <= f ub -> comp f g x = id x)
(g_wf:forall x : R, f lb <= x -> x <= f ub -> lb <= g x <= ub)
(f_incr:forall x y : R, lb <= x -> x < y -> y <= ub -> f x < f y)
(f_derivable:forall a : R, lb <= a <= ub -> derivable_pt f a),
derive_pt f (g x)
(derivable_pt_recip_interv_prelim1 f g lb ub x lb_lt_ub
x_encad f_eq_g g_wf f_incr f_derivable)
<> 0 ->
derivable_pt g x.

# Value of the derivative of the reciprocal function

Lemma derive_pt_recip_interv_prelim0 : forall (f g:R->R) (lb ub x:R)
(Prf:derivable_pt f (g x)) (Prg:derivable_pt g x),
lb < ub ->
lb < x < ub ->
(forall x, lb < x < ub -> (comp f g) x = id x) ->
derive_pt f (g x) Prf <> 0 ->
derive_pt g x Prg = 1 / ( derive_pt f (g x) Prf ).
Lemma derive_pt_recip_interv_prelim1_0 : forall (f g:R->R) (lb ub x:R),
lb < ub ->
f lb < x < f ub ->
(forall x y : R, lb <= x -> x < y -> y <= ub -> f x < f y) ->
(forall x : R, f lb <= x -> x <= f ub -> lb <= g x <= ub) ->
(forall x, f lb <= x -> x <= f ub -> (comp f g) x = id x) ->
lb < g x < ub.
Lemma derive_pt_recip_interv_prelim1_1 : forall (f g:R->R) (lb ub x:R),
lb < ub ->
f lb < x < f ub ->
(forall x y : R, lb <= x -> x < y -> y <= ub -> f x < f y) ->
(forall x : R, f lb <= x -> x <= f ub -> lb <= g x <= ub) ->
(forall x, f lb <= x -> x <= f ub -> (comp f g) x = id x) ->
lb <= g x <= ub.
Lemma derive_pt_recip_interv : forall (f g:R->R) (lb ub x:R)
(lb_lt_ub:lb < ub) (x_encad:f lb < x < f ub)
(f_incr:forall x y : R, lb <= x -> x < y -> y <= ub -> f x < f y)
(g_wf:forall x : R, f lb <= x -> x <= f ub -> lb <= g x <= ub)
(Prf:forall a : R, lb <= a <= ub -> derivable_pt f a)
(f_eq_g:forall x, f lb <= x -> x <= f ub -> (comp f g) x = id x)
(Df_neq:derive_pt f (g x) (derivable_pt_recip_interv_prelim1 f g lb ub x
lb_lt_ub x_encad f_eq_g g_wf f_incr Prf) <> 0),
derive_pt g x (derivable_pt_recip_interv f g lb ub x lb_lt_ub x_encad f_eq_g
g_wf f_incr Prf Df_neq)
=
1 / ( derive_pt f (g x) (Prf (g x) (derive_pt_recip_interv_prelim1_1 f g lb ub x
lb_lt_ub x_encad f_incr g_wf f_eq_g))).

# Existence of the derivative of a function which is the limit of a sequence of functions

Definition boule_of_interval x y (h : x < y) :
{ c : R & { r : posreal | c - r = x /\ c + r = y } }.
Qed.
Definition boule_in_interval x y z (h : x < z < y) :
{ c : R & { r | Boule c r z /\ x < c - r /\ c + r < y } }.
Lemma Ball_in_inter : forall c1 c2 r1 r2 x,
Boule c1 r1 x -> Boule c2 r2 x ->
{ r3 : posreal | forall y, Boule x r3 y -> Boule c1 r1 y /\ Boule c2 r2 y }.
Lemma Boule_center : forall x r, Boule x r x.
Lemma derivable_pt_lim_CVU : forall (fn fn':nat -> R -> R) (f g:R->R)
(x:R) c r, Boule c r x ->
(forall y n, Boule c r y -> derivable_pt_lim (fn n) y (fn' n y)) ->
(forall y, Boule c r y -> Un_cv (fun n => fn n y) (f y)) ->
(CVU fn' g c r) ->
(forall y, Boule c r y -> continuity_pt g y) ->
derivable_pt_lim f x (g x).