Library Coq.Reals.Ranalysis5
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
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 -> 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 :
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 g_wf f_derivable)
<> 0
->
derivable_pt g x.
Lemma derivable_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_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.
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_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))
).
Existence of the derivative of a function which is the limit of a sequence of functions