Library Coq.Reals.Ranalysis5

Require Import Rbase.
Require Import Ranalysis_reg.
Require Import Rfunctions.
Require Import Rseries.
Require Import Lra.
Require Import RiemannInt.
Require Import SeqProp.
Require Import Max.
Require Import Omega.
Require Import Lra.
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}.

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
<> 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