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.

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.

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

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.

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.

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

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