# Library Coq.Reals.Ranalysis5

Require Import Rbase.
Require Import Ranalysis_reg.
Require Import Rfunctions.
Require Import Rseries.
Require Import RiemannInt.
Require Import SeqProp.
Require Import Lia.
Require Import Lra.
Local Open Scope R_scope.

Local Ltac Tauto.intuition_solver ::= auto with rorders real.

# 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}.

# 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 -> lb <= g x <= ub) ->
(forall a : R, lb <= a <= ub -> derivable_pt f a) ->
derivable_pt f (g x).

Lemma derivable_pt_recip_interv_prelim1_decr : forall (f g:R->R) (lb ub x : R),
lb < ub ->
f ub < x < f lb ->
(forall x : R, f ub <= x -> x <= f lb -> lb <= g x <= ub) ->
(forall a : R, lb <= a <= ub -> derivable_pt f a) ->
derivable_pt f (g x).

Lemma derivable_pt_recip_interv
(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
<> 0 ->
derivable_pt g x.

Lemma derivable_pt_recip_interv_decr (f g:R->R) (lb ub x : R)
(lb_lt_ub:lb < ub)
(x_encad:f ub < x < f lb)
(f_eq_g:forall x : R, f ub <= x -> x <= f lb -> comp f g x = id x)
(g_wf:forall x : R, f ub <= x -> x <= f lb -> lb <= g x <= ub)
(f_decr:forall x y : R, lb <= x -> x < y -> y <= ub -> f y < f x)
(f_derivable:forall a : R, lb <= a <= ub -> derivable_pt f a)
: derive_pt f (g x)
(derivable_pt_recip_interv_prelim1_decr f g lb ub x lb_lt_ub
<> 0 ->
derivable_pt g x.

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

Lemma derivable_pt_lim_CVU (fn fn':nat -> R -> R) (f g:R->R)
(x:R) : forall 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).

Require Import Max.