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.

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 -> 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
                                                 x_encad g_wf f_derivable)
    <> 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
                                                      x_encad g_wf f_derivable)
    <> 0 ->
    derivable_pt g x.

Lemma derive_pt_recip_interv_prelim0 (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_prelim1_1_decr : forall (f g:R->R) (lb ub x:R),
       lb < ub ->
       f ub < x < f lb ->
       (forall x y : R, lb <= x -> x < y -> y <= ub -> f y < f x) ->
       (forall x : R, f ub <= x -> x <= f lb -> lb <= g x <= ub) ->
       (forall x, f ub <= x -> x <= f lb -> (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 g_wf 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 derive_pt_recip_interv_decr : forall (f g:R->R) (lb ub x:R)
       (lb_lt_ub:lb < ub)
       (x_encad:f ub < x < f lb)
       (f_decr:forall x y : R, lb <= x -> x < y -> y <= ub -> f y < f x)
       (g_wf:forall x : R, f ub <= x -> x <= f lb -> lb <= g x <= ub)
       (Prf:forall a : R, lb <= a <= ub -> derivable_pt f a)
       (f_eq_g:forall x, f ub <= x -> x <= f lb -> (comp f g) x = id x)
       (Df_neq:derive_pt f (g x) (derivable_pt_recip_interv_prelim1_decr f g lb ub x
                 lb_lt_ub x_encad g_wf Prf) <> 0),
       derive_pt g x (derivable_pt_recip_interv_decr f g lb ub x lb_lt_ub x_encad f_eq_g
                 g_wf f_decr Prf Df_neq)
       =
       1 / (derive_pt f (g x) (Prf (g x) (derive_pt_recip_interv_prelim1_1_decr f g lb ub x
       lb_lt_ub x_encad f_decr g_wf f_eq_g))).

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.