From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
Require Import reals signed topology prodnormedzmodule normedtype landau forms.
# Differentiation
This file provides a theory of differentiation. It includes the standard
rules of differentiation (differential of a sum, of a product, of
exponentiation, of the inverse, etc.) as well as standard theorems (the
Extreme Value Theorem, Rolle's theorem, the Mean Value Theorem).
Parsable notations (in all of the following, f is not supposed to be
differentiable):
```
'd f x == the differential of a function f at a point x
differentiable f x == the function f is differentiable at a point x
'J f x == the Jacobian of f at a point x
'D_v f == the directional derivative of f along v
derivable f a v == the function f is derivable at a with direction v
The type of f is V -> W with V W : normedModType R
and R : numFieldType
f^`() == the derivative of f of domain R
f^`(n) == the nth derivative of f of domain R
```
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Theory.
Import numFieldNormedType.Exports.
Local Open Scope ring_scope.
Local Open Scope classical_set_scope.
Reserved Notation "''d' f x" (
at level 0, f at level 0, x at level 0,
format "''d' f x").
Reserved Notation "'is_diff' F" (
at level 0, F at level 0,
format "'is_diff' F").
Reserved Notation "''J' f p" (
at level 10, p, f at next level,
format "''J' f p").
Reserved Notation "''D_' v f" (
at level 10, v, f at next level,
format "''D_' v f").
Reserved Notation "''D_' v f c" (
at level 10, v, f at next level,
format "''D_' v f c").
Reserved Notation "f ^` ()" (at level 8, format "f ^` ()").
Reserved Notation "f ^` ( n )" (at level 8, format "f ^` ( n )").
Section
Differential
.
Context {K : numDomainType} {V
W
: normedModType K}.
Definition
diff
(
F
: filter_on V) (
_ : phantom (
set (
set V))
F) (
f
: V -> W)
:=
(
get (
fun (
df
: {linear V -> W})
=> continuous df /\ forall
x,
f x = f (
lim F)
+ df (
x - lim F)
+o_(
x
\near F) (
x - lim F))).
Local Notation
"''d' f x"
:= (
@diff _ (
Phantom _ [filter of x])
f).
Fact
diff_key
: forall
T,
T -> unit
Proof.
by constructor. Qed.
CoInductive
differentiable_def
(
f
: V -> W) (
x
: filter_on V)
(
phF
: phantom (
set (
set V))
x)
: Prop :=
DifferentiableDef
of
(
continuous (
'd f x)
/\
f = cst (
f (
lim x))
+ 'd f x \o center (
lim x)
+o_x (
center (
lim x))).
Local Notation
differentiable
f F := (
@differentiable_def f _ (
Phantom _ [filter of F])).
Class
is_diff_def
(
x
: filter_on V) (
Fph
: phantom (
set (
set V))
x) (
f
: V -> W)
(
df
: V -> W)
:= DiffDef {
ex_diff
: differentiable f x ;
diff_val
: 'd f x = df :> (
V -> W)
}.
Hint Mode is_diff_def - - ! - : typeclass_instances.
Lemma
diffP
(
F
: filter_on V) (
f
: V -> W)
:
differentiable f F <->
continuous (
'd f F)
/\
(
forall
x,
f x = f (
lim F)
+ 'd f F (
x - lim F)
+o_(
x
\near F) (
x - lim F)).
Proof.
by split=> [[] |]; last constructor; rewrite funeqE. Qed.
Lemma
diff_continuous
(
x
: filter_on V) (
f
: V -> W)
:
differentiable f x -> continuous (
'd f x).
Proof.
by move=> /diffP []. Qed.
Hint Extern 0 (
continuous _)
=> exact: diff_continuous : core.
Lemma
diffE
(
F
: filter_on V) (
f
: V -> W)
:
differentiable f F ->
forall
x,
f x = f (
lim F)
+ 'd f F (
x - lim F)
+o_(
x
\near F) (
x - lim F).
Proof.
by move=> /diffP []. Qed.
Lemma
littleo_center0
(
x
: V) (
f
: V -> W) (
e
: V -> V)
:
[o_x e of f] = [o_ (
0 : V) (
e \o shift x)
of f \o shift x] \o center x.
Proof.
rewrite /the_littleo /insubd /=; have [g /= _ <-{f}|/asboolP Nfe] /= := insubP.
rewrite insubT //= ?comp_shiftK //; apply/asboolP => _/posnumP[eps].
rewrite [\forall
x
\near _, _ <= _](
near_shift x)
sub0r; near=> y.
by rewrite /= subrK; near: y; have /eqoP := littleo_eqo g; apply.
rewrite insubF //; apply/asboolP => fe; apply: Nfe => _/posnumP[eps].
by rewrite [\forall
x
\near _, _ <= _](
near_shift 0)
subr0; apply: fe.
Unshelve.
all: by end_near. Qed.
End Differential.
Section
Differential_numFieldType
.
Context {K : numFieldType } {V
W
: normedModType K}.
Local Notation
differentiable
f F := (
@differentiable_def _ _ _ f _ (
Phantom _ [filter of F])).
Local Notation
"''d' f x"
:= (
@diff _ _ _ _ (
Phantom _ [filter of x])
f).
Hint Extern 0 (
continuous _)
=> exact: diff_continuous : core.
Lemma
diff_locallyxP
(
x
: V) (
f
: V -> W)
:
differentiable f x <-> continuous (
'd f x)
/\
forall
h,
f (
h + x)
= f x + 'd f x h +o_(
h
\near 0 : V)
h.
Proof.
Lemma
diff_locallyx
(
x
: V) (
f
: V -> W)
: differentiable f x ->
forall
h,
f (
h + x)
= f x + 'd f x h +o_(
h
\near 0 : V)
h.
Proof.
by move=> /diff_locallyxP []. Qed.
Lemma
diff_locallyxC
(
x
: V) (
f
: V -> W)
: differentiable f x ->
forall
h,
f (
x + h)
= f x + 'd f x h +o_(
h
\near 0 : V)
h.
Proof.
by move=> ?; apply/eqaddoEx => h; rewrite [x + h]addrC diff_locallyx. Qed.
Lemma
diff_locallyP
(
x
: V) (
f
: V -> W)
:
differentiable f x <->
continuous (
'd f x)
/\ (
f \o shift x = cst (
f x)
+ 'd f x +o_ (
0 : V)
id).
Proof.
Lemma
diff_locally
(
x
: V) (
f
: V -> W)
: differentiable f x ->
(
f \o shift x = cst (
f x)
+ 'd f x +o_ (
0 : V)
id).
Proof.
by move=> /diff_locallyP []. Qed.
End Differential_numFieldType.
Notation
"''d' f F"
:= (
@diff _ _ _ _ (
Phantom _ [filter of F])
f).
Notation
differentiable
f F := (
@differentiable_def _ _ _ f _ (
Phantom _ [filter of F])).
Notation
"'is_diff' F"
:= (
is_diff_def (
Phantom _ [filter of F])).
#[global] Hint Extern 0 (
differentiable _ _)
=> solve[apply: ex_diff] : core.
#[global] Hint Extern 0 (
{for _, continuous _})
=> exact: diff_continuous : core.
Lemma
differentiableP
(
R
: numDomainType) (
V
W
: normedModType R) (
f
: V -> W)
x
:
differentiable f x -> is_diff x f (
'd f x).
Proof.
Section
jacobian
.
Definition
jacobian
n
m
(
R
: numFieldType) (
f
: 'rV[R]_n.
+1 -> 'rV[R]_m.
+1)
p
:=
lin1_mx (
'd f p).
End jacobian.
Notation
"''J' f p"
:= (
jacobian f p).
Section
DifferentialR
.
Context {R : numFieldType} {V
W
: normedModType R}.
Lemma
differentiable_continuous
(
x
: V) (
f
: V -> W)
:
differentiable f x -> {for x, continuous f}.
Proof.
Section
littleo_lemmas
.
Variables (
X
Y
Z
: normedModType R).
Lemma
normm_littleo
x
(
f
: X -> Y)
: `| [o_(
x
\near x) (
1 : R)
of f x]| = 0.
Proof.
Lemma
littleo_lim0
(
f
: X -> Y) (
h
: _ -> Z) (
x
: X)
:
f @ x --> (
0 : Y)
-> [o_x f of h] x = 0.
Proof.
End littleo_lemmas.
Section
diff_locally_converse_tentative
.
Lemma
diff_locally_converse_part1
(
f
: R -> R) (
a
b
x
: R)
:
f \o shift x = cst a + b *: idfun +o_ (
0 : R)
id -> f x = a.
Proof.
End diff_locally_converse_tentative.
Definition
derive
(
f
: V -> W)
a
v
:=
lim ((
fun
h
=> h^-1 *: ((
f \o shift a) (
h *: v)
- f a))
@ 0^').
Local Notation
"''D_' v f"
:= (
derive f ^~ v).
Local Notation
"''D_' v f c"
:= (
derive f c v).
Definition
derivable
(
f
: V -> W)
a
v
:=
cvg ((
fun
h
=> h^-1 *: ((
f \o shift a) (
h *: v)
- f a))
@ 0^').
Class
is_derive
(
a
v
: V) (
f
: V -> W) (
df
: W)
:= DeriveDef {
ex_derive
: derivable f a v;
derive_val
: 'D_v f a = df
}.
Lemma
derivable_nbhs
(
f
: V -> W)
a
v
:
derivable f a v ->
(
fun
h
=> (
f \o shift a) (
h *: v))
= (
cst (
f a))
+
(
fun
h
=> h *: (
'D_v f a))
+o_ (
nbhs (
0 :R))
id.
Proof.
Lemma
derivable_nbhsP
(
f
: V -> W)
a
v
:
derivable f a v <->
(
fun
h
=> (
f \o shift a) (
h *: v))
= (
cst (
f a))
+
(
fun
h
=> h *: (
'D_v f a))
+o_ (
nbhs (
0 : R))
id.
Proof.
Lemma
derivable_nbhsx
(
f
: V -> W)
a
v
:
derivable f a v -> forall
h,
f (
a + h *: v)
= f a + h *: 'D_v f a
+o_(
h
\near (
nbhs (
0 : R)))
h.
Proof.
move=> /derivable_nbhs; rewrite funeqE => df.
by apply: eqaddoEx => h; have /= := (
df h)
; rewrite addrC => ->.
Qed.
Lemma
derivable_nbhsxP
(
f
: V -> W)
a
v
:
derivable f a v <-> forall
h,
f (
a + h *: v)
= f a + h *: 'D_v f a
+o_(
h
\near (
nbhs (
0 :R)))
h.
Proof.
split; first exact: derivable_nbhsx.
move=> df; apply/derivable_nbhsP; apply/eqaddoE; rewrite funeqE => h.
by rewrite /= addrC df.
Qed.
End DifferentialR.
Notation
"''D_' v f"
:= (
derive f ^~ v).
Notation
"''D_' v f c"
:= (
derive f c v).
#[global] Hint Extern 0 (
derivable _ _ _)
=> solve[apply: ex_derive] : core.
Section
DifferentialR_numFieldType
.
Context {R : numFieldType} {V
W
: normedModType R}.
Lemma
deriveE
(
f
: V -> W) (
a
v
: V)
:
differentiable f a -> 'D_v f a = 'd f a v.
Proof.
End DifferentialR_numFieldType.
Section
DifferentialR2
.
Variable
R
: numFieldType.
Implicit Type (
V : normedModType R).
Lemma
derivemxE
m
n
(
f
: 'rV[R]_m.
+1 -> 'rV[R]_n.
+1) (
a
v
: 'rV[R]_m.
+1)
:
differentiable f a -> 'D_ v f a = v *m jacobian f a.
Proof.
by move=> /deriveE->; rewrite /jacobian mul_rV_lin1. Qed.
Definition
derive1
V
(
f
: R -> V) (
a
: R)
:=
lim ((
fun
h
=> h^-1 *: (
f (
h + a)
- f a))
@ 0^').
Local Notation
"f ^` ()"
:= (
derive1 f).
Lemma
derive1E
V
(
f
: R -> V)
a
: f^`()
a = 'D_1 f a.
Proof.
rewrite /derive1 /derive; set d := (
fun _ : R => _)
; set d' := (
fun _ : R => _).
by suff -> : d = d' by []; rewrite funeqE=> h; rewrite /d /d' /= [h%:A](
mulr1).
Qed.
Lemma
derive1E'
V
f
a
: differentiable (
f : R -> V)
a ->
f^`()
a = 'd f a 1.
Proof.
Definition
derive1n
V
n
(
f
: R -> V)
:= iter n (
@derive1 V)
f.
Local Notation
"f ^` ( n )"
:= (
derive1n n f).
Lemma
derive1n0
V
(
f
: R -> V)
: f^`(
0)
= f.
Proof.
by []. Qed.
Lemma
derive1n1
V
(
f
: R -> V)
: f^`(
1)
= f^`().
Proof.
by []. Qed.
Lemma
derive1nS
V
(
f
: R -> V)
n
: f^`(
n.
+1)
= f^`(
n)
^`().
Proof.
by []. Qed.
Lemma
derive1Sn
V
(
f
: R -> V)
n
: f^`(
n.
+1)
= f^`()
^`(
n).
Proof.
End DifferentialR2.
Notation
"f ^` ()"
:= (
derive1 f).
Notation
"f ^` ( n )"
:= (
derive1n n f).
Section
DifferentialR3
.
Variable
R
: numFieldType.
Fact
dcst
(
V
W
: normedModType R) (
a
: W) (
x
: V)
: continuous (
0 : V -> W)
/\
cst a \o shift x = cst (
cst a x)
+ \0 +o_ (
0 : V)
id.
Proof.
Variables (
V
W
: normedModType R).
Fact
dadd
(
f
g
: V -> W)
x
:
differentiable f x -> differentiable g x ->
continuous (
'd f x \+ 'd g x)
/\
(
f + g)
\o shift x = cst ((
f + g)
x)
+ (
'd f x \+ 'd g x)
+o_ (
0 : V)
id.
Proof.
Fact
dopp
(
f
: V -> W)
x
:
differentiable f x -> continuous (
- (
'd f x : V -> W))
/\
(
- f)
\o shift x = cst (
- f x)
\- 'd f x +o_ (
0 : V)
id.
Proof.
Lemma
is_diff_eq
(
V'
W'
: normedModType R) (
f
f'
g
: V' -> W') (
x
: V')
:
is_diff x f f' -> f' = g -> is_diff x f g.
Proof.
by move=> ? <-. Qed.
Fact
dscale
(
f
: V -> W)
k
x
:
differentiable f x -> continuous (
k \*: 'd f x)
/\
(
k *: f)
\o shift x = cst ((
k *: f)
x)
+ k \*: 'd f x +o_ (
0 : V)
id.
Proof.
Fact
dscalel
(
k
: V -> R) (
f
: W)
x
:
differentiable k x ->
continuous (
fun
z
: V => 'd k x z *: f)
/\
(
fun
z
=> k z *: f)
\o shift x =
cst (
k x *: f)
+ (
fun
z
=> 'd k x z *: f)
+o_ (
0 : V)
id.
Proof.
move=> df; split.
move=> ?; exact/continuousZl/diff_continuous.
apply/eqaddoE; rewrite funeqE => y /=.
by rewrite diff_locallyx //= !scalerDl scaleolx.
Qed.
Fact
dlin
(
V'
W'
: normedModType R) (
f
: {linear V' -> W'})
x
:
continuous f -> f \o shift x = cst (
f x)
+ f +o_ (
0 : V')
id.
Proof.
Lemma
compoO_eqo
(
U
V'
W'
: normedModType R) (
f
: U -> V')
(
g
: V' -> W')
:
[o_ (
0 : V')
id of g] \o [O_ (
0 : U)
id of f] =o_ (
0 : U)
id.
Proof.
Lemma
compoO_eqox
(
U
V'
W'
: normedModType R) (
f
: U -> V')
(
g
: V' -> W')
:
forall
x
: U, [o_ (
0 : V')
id of g] (
[O_ (
0 : U)
id of f] x)
=o_(
x
\near 0 : U)
x.
Proof.
Lemma
compOo_eqo
(
U
V'
W'
: normedModType R) (
f
: U -> V')
(
g
: V' -> W')
:
[O_ (
0 : V')
id of g] \o [o_ (
0 : U)
id of f] =o_ (
0 : U)
id.
Proof.
apply/eqoP => _ /posnumP[e].
have /bigO_exP [_ /posnumP[k]] := bigOP [bigO of [O_ (
0 : V')
id of g]].
move=> /nbhs_ballP [_ /posnumP[d] hd].
have ekgt0 : e%:num / k%:num > 0 by [].
have /(
_ _ ekgt0)
:= littleoP [littleo of [o_ (
0 : U)
id of f]].
apply: filter_app; near=> x => leoxekx; apply: le_trans (
hd _ _)
_; last first.
by rewrite -ler_pdivl_mull // mulrA [_^-1 * _]mulrC.
by rewrite -ball_normE /= distrC subr0 (
le_lt_trans leoxekx)
// -ltr_pdivl_mull //.
Unshelve.
all: by end_near. Qed.
End DifferentialR3.
Section
DifferentialR3_numFieldType
.
Variable
R
: numFieldType.
Lemma
littleo_linear0
(
V
W
: normedModType R) (
f
: {linear V -> W})
:
(
f : V -> W)
=o_ (
0 : V)
id -> f = cst 0 :> (
V -> W).
Proof.
Lemma
diff_unique
(
V
W
: normedModType R) (
f
: V -> W)
(
df
: {linear V -> W})
x
:
continuous df -> f \o shift x = cst (
f x)
+ df +o_ (
0 : V)
id ->
'd f x = df :> (
V -> W).
Proof.
Lemma
diff_cst
(
V
W
: normedModType R)
a
x
: (
'd (
cst a)
x : V -> W)
= 0.
Proof.
by apply/diff_unique; have [] := dcst a x. Qed.
Variables (
V
W
: normedModType R).
Lemma
differentiable_cst
(
W'
: normedModType R) (
a
: W') (
x
: V)
:
differentiable (
cst a)
x.
Proof.
Global Instance
is_diff_cst
(
a
: W) (
x
: V)
: is_diff x (
cst a)
0.
Proof.
Lemma
diffD
(
f
g
: V -> W)
x
:
differentiable f x -> differentiable g x ->
'd (
f + g)
x = 'd f x \+ 'd g x :> (
V -> W).
Proof.
by move=> df dg; apply/diff_unique; have [] := dadd df dg. Qed.
Lemma
differentiableD
(
f
g
: V -> W)
x
:
differentiable f x -> differentiable g x -> differentiable (
f + g)
x.
Proof.
by move=> df dg; apply/diff_locallyP; rewrite diffD //; have := dadd df dg.
Qed.
Global Instance
is_diffD
(
f
g
df
dg
: V -> W)
x
:
is_diff x f df -> is_diff x g dg -> is_diff x (
f + g) (
df + dg).
Proof.
Lemma
differentiable_sum
n
(
f
: 'I_n -> V -> W) (
x
: V)
:
(
forall
i,
differentiable (
f i)
x)
-> differentiable (
\sum_(
i
< n)
f i)
x.
Proof.
by elim/big_ind : _ => // ? ? g h ?; apply: differentiableD; [exact:g|exact:h].
Qed.
Lemma
diffN
(
f
: V -> W)
x
:
differentiable f x -> 'd (
- f)
x = - (
'd f x : V -> W)
:> (
V -> W).
Proof.
move=> df; rewrite -[RHS]/(
@GRing.
opp _ \o _)
; apply/diff_unique;
by have [] := dopp df.
Qed.
Lemma
differentiableN
(
f
: V -> W)
x
:
differentiable f x -> differentiable (
- f)
x.
Proof.
by move=> df; apply/diff_locallyP; rewrite diffN //; have := dopp df.
Qed.
Global Instance
is_diffN
(
f
df
: V -> W)
x
:
is_diff x f df -> is_diff x (
- f) (
- df).
Proof.
Global Instance
is_diffB
(
f
g
df
dg
: V -> W)
x
:
is_diff x f df -> is_diff x g dg -> is_diff x (
f - g) (
df - dg).
Proof.
Lemma
diffB
(
f
g
: V -> W)
x
:
differentiable f x -> differentiable g x ->
'd (
f - g)
x = 'd f x \- 'd g x :> (
V -> W).
Proof.
by move=> /differentiableP df /differentiableP dg; rewrite diff_val. Qed.
Lemma
differentiableB
(
f
g
: V -> W)
x
:
differentiable f x -> differentiable g x -> differentiable (
f \- g)
x.
Proof.
by move=> /differentiableP df /differentiableP dg. Qed.
Lemma
diffZ
(
f
: V -> W)
k
x
:
differentiable f x -> 'd (
k *: f)
x = k \*: 'd f x :> (
V -> W).
Proof.
by move=> df; apply/diff_unique; have [] := dscale k df. Qed.
Lemma
differentiableZ
(
f
: V -> W)
k
x
:
differentiable f x -> differentiable (
k *: f)
x.
Proof.
by move=> df; apply/diff_locallyP; rewrite diffZ //; have := dscale k df.
Qed.
Global Instance
is_diffZ
(
f
df
: V -> W)
k
x
:
is_diff x f df -> is_diff x (
k *: f) (
k *: df).
Proof.
Lemma
diffZl
(
k
: V -> R) (
f
: W)
x
: differentiable k x ->
'd (
fun
z
=> k z *: f)
x = (
fun
z
=> 'd k x z *: f)
:> (
_ -> _).
Proof.
Lemma
differentiableZl
(
k
: V -> R) (
f
: W)
x
:
differentiable k x -> differentiable (
fun
z
=> k z *: f)
x.
Proof.
by move=> df; apply/diff_locallyP; rewrite diffZl //; have [] := dscalel f df.
Qed.
Lemma
diff_lin
(
V'
W'
: normedModType R) (
f
: {linear V' -> W'})
x
:
continuous f -> 'd f x = f :> (
V' -> W').
Proof.
by move=> fcont; apply/diff_unique => //; apply: dlin. Qed.
Lemma
linear_differentiable
(
V'
W'
: normedModType R) (
f
: {linear V' -> W'})
x
: continuous f -> differentiable f x.
Proof.
by move=> fcont; apply/diff_locallyP; rewrite diff_lin //; have := dlin x fcont.
Qed.
Global Instance
is_diff_id
(
x
: V)
: is_diff x id id.
Proof.
Global Instance
is_diff_scaler
(
k
: R) (
x
: V)
: is_diff x (
*:%R k) (
*:%R k).
Proof.
Global Instance
is_diff_scalel
(
k
: R) (
x
: V)
:
is_diff k (
*:%R ^~ x) (
*:%R ^~ x).
Proof.
Lemma
differentiable_coord
m
n
(
M
: 'M[R]_(
m.
+1, n.
+1))
i
j
:
differentiable (
fun
N
: 'M[R]_(
m.
+1, n.
+1)
=> N i j : R )
M.
Proof.
have @f : {linear 'M[R]_(
m.
+1, n.
+1)
-> R}.
by exists (
fun
N
: 'M[R]_(
_, _)
=> N i j)
; eexists; move=> ? ?; rewrite !mxE.
rewrite (
_ : (
fun _ => _)
= f)
//; exact/linear_differentiable/coord_continuous.
Qed.
Lemma
linear_lipschitz
(
V'
W'
: normedModType R) (
f
: {linear V' -> W'})
:
continuous f -> exists2
k,
k > 0 & forall
x,
`|f x| <= k * `|x|.
Proof.
Lemma
linear_eqO
(
V'
W'
: normedModType R) (
f
: {linear V' -> W'})
:
continuous f -> (
f : V' -> W')
=O_ (
0 : V')
id.
Proof.
move=> /linear_lipschitz [k kgt0 flip]; apply/eqO_exP; exists k => //.
exact: filterE.
Qed.
Lemma
diff_eqO
(
V'
W'
: normedModType R) (
x
: filter_on V') (
f
: V' -> W')
:
differentiable f x -> (
'd f x : V' -> W')
=O_ (
0 : V')
id.
Proof.
by move=> /diff_continuous /linear_eqO; apply. Qed.
Lemma
compOo_eqox
(
U
V'
W'
: normedModType R) (
f
: U -> V')
(
g
: V' -> W')
: forall
x,
[O_ (
0 : V')
id of g] (
[o_ (
0 : U)
id of f] x)
=o_(
x
\near 0 : U)
x.
Proof.
Fact
dcomp
(
U
V'
W'
: normedModType R) (
f
: U -> V') (
g
: V' -> W')
x
:
differentiable f x -> differentiable g (
f x)
->
continuous (
'd g (
f x)
\o 'd f x)
/\ forall
y,
g (
f (
y + x))
= g (
f x)
+ (
'd g (
f x)
\o 'd f x)
y +o_(
y
\near 0 : U)
y.
Proof.
Lemma
diff_comp
(
U
V'
W'
: normedModType R) (
f
: U -> V') (
g
: V' -> W')
x
:
differentiable f x -> differentiable g (
f x)
->
'd (
g \o f)
x = 'd g (
f x)
\o 'd f x :> (
U -> W').
Proof.
by move=> df dg; apply/diff_unique; have [? /funext] := dcomp df dg. Qed.
Lemma
differentiable_comp
(
U
V'
W'
: normedModType R) (
f
: U -> V')
(
g
: V' -> W')
x
: differentiable f x -> differentiable g (
f x)
->
differentiable (
g \o f)
x.
Proof.
move=> df dg; apply/diff_locallyP; rewrite diff_comp //;
by have [? /funext]:= dcomp df dg.
Qed.
Global Instance
is_diff_comp
(
U
V'
W'
: normedModType R) (
f
df
: U -> V')
(
g
dg
: V' -> W')
x
: is_diff x f df -> is_diff (
f x)
g dg ->
is_diff x (
g \o f) (
dg \o df)
| 99.
Proof.
Lemma
bilinear_schwarz
(
U
V'
W'
: normedModType R)
(
f
: {bilinear U -> V' -> W'})
: continuous (
fun
p
=> f p.
1 p.
2)
->
exists2
k,
k > 0 & forall
u
v,
`|f u v| <= k * `|u| * `|v|.
Proof.
Lemma
bilinear_eqo
(
U
V'
W'
: normedModType R) (
f
: {bilinear U -> V' -> W'})
:
continuous (
fun
p
=> f p.
1 p.
2)
-> (
fun
p
=> f p.
1 p.
2)
=o_ (
0 : U * V')
id.
Proof.
Fact
dbilin
(
U
V'
W'
: normedModType R) (
f
: {bilinear U -> V' -> W'})
p
:
continuous (
fun
p
=> f p.
1 p.
2)
->
continuous (
fun
q
=> (
f p.
1 q.
2 + f q.
1 p.
2))
/\
(
fun
q
=> f q.
1 q.
2)
\o shift p = cst (
f p.
1 p.
2)
+
(
fun
q
=> f p.
1 q.
2 + f q.
1 p.
2)
+o_ (
0 : U * V')
id.
Proof.
move=> fc; split=> [q|].
by apply: (
@continuousD _ _ _ (
fun
q
=> f p.
1 q.
2) (
fun
q
=> f q.
1 p.
2))
;
move=> A /(
fc (
_.
1, _.
2))
/= /nbhs_ballP [_ /posnumP[e] fpqe_A];
apply/nbhs_ballP; exists e%:num => //= r [? ?]; exact: (
fpqe_A (
_.
1, _.
2)).
apply/eqaddoE; rewrite funeqE => q /=.
rewrite linearDl !linearDr addrA addrC.
rewrite -[f q.
1 _ + _ + _]addrA [f q.
1 _ + _]addrC addrA [f q.
1 _ + _]addrC.
by congr (
_ + _)
; rewrite -[LHS]/((
fun
p
=> f p.
1 p.
2)
q)
bilinear_eqo.
Qed.
Lemma
diff_bilin
(
U
V'
W'
: normedModType R) (
f
: {bilinear U -> V' -> W'})
p
:
continuous (
fun
p
=> f p.
1 p.
2)
-> 'd (
fun
q
=> f q.
1 q.
2)
p =
(
fun
q
=> f p.
1 q.
2 + f q.
1 p.
2)
:> (
U * V' -> W').
Proof.
Lemma
differentiable_bilin
(
U
V'
W'
: normedModType R)
(
f
: {bilinear U -> V' -> W'})
p
:
continuous (
fun
p
=> f p.
1 p.
2)
-> differentiable (
fun
p
=> f p.
1 p.
2)
p.
Proof.
by move=> fc; apply/diff_locallyP; rewrite diff_bilin //; apply: dbilin p fc.
Qed.
Definition
mulr_rev
(
y
x
: R)
:= x * y.
Canonical
rev_mulr
:= @RevOp _ _ _ mulr_rev (
@GRing.
mul [ringType of R])
(
fun _ _ => erefl).
Lemma
mulr_is_linear
x
: linear (
@GRing.
mul [ringType of R] x : R -> R).
Proof.
Canonical
mulr_linear
x
:= Linear (
mulr_is_linear x).
Lemma
mulr_rev_is_linear
y
: linear (
mulr_rev y : R -> R).
Proof.
Canonical
mulr_rev_linear
y
:= Linear (
mulr_rev_is_linear y).
Canonical
mulr_bilinear
:=
[bilinear of @GRing.
mul [ringType of [lmodType R of R]]].
Global Instance
is_diff_mulr
(
p
: R * R)
:
is_diff p (
fun
q
=> q.
1 * q.
2) (
fun
q
=> p.
1 * q.
2 + q.
1 * p.
2).
Proof.
Lemma
eqo_pair
(
U
V'
W'
: normedModType R) (
F
: filter_on U)
(
f
: U -> V') (
g
: U -> W')
:
(
fun
t
=> (
[o_F id of f] t, [o_F id of g] t))
=o_F id.
Proof.
apply/eqoP => _/posnumP[e]; near=> x; rewrite num_le_maxl /=.
by apply/andP; split; near: x; apply: littleoP.
Unshelve.
all: by end_near. Qed.
Fact
dpair
(
U
V'
W'
: normedModType R) (
f
: U -> V') (
g
: U -> W')
x
:
differentiable f x -> differentiable g x ->
continuous (
fun
y
=> (
'd f x y, 'd g x y))
/\
(
fun
y
=> (
f y, g y))
\o shift x = cst (
f x, g x)
+
(
fun
y
=> (
'd f x y, 'd g x y))
+o_ (
0 : U)
id.
Proof.
Lemma
diff_pair
(
U
V'
W'
: normedModType R) (
f
: U -> V') (
g
: U -> W')
x
:
differentiable f x -> differentiable g x -> 'd (
fun
y
=> (
f y, g y))
x =
(
fun
y
=> (
'd f x y, 'd g x y))
:> (
U -> V' * W').
Proof.
Lemma
differentiable_pair
(
U
V'
W'
: normedModType R) (
f
: U -> V')
(
g
: U -> W')
x
: differentiable f x -> differentiable g x ->
differentiable (
fun
y
=> (
f y, g y))
x.
Proof.
by move=> df dg; apply/diff_locallyP; rewrite diff_pair //; apply: dpair.
Qed.
Global Instance
is_diff_pair
(
U
V'
W'
: normedModType R) (
f
df
: U -> V')
(
g
dg
: U -> W')
x
: is_diff x f df -> is_diff x g dg ->
is_diff x (
fun
y
=> (
f y, g y)) (
fun
y
=> (
df y, dg y)).
Proof.
Global Instance
is_diffM
(
f
g
df
dg
: V -> R)
x
:
is_diff x f df -> is_diff x g dg -> is_diff x (
f * g) (
f x *: dg + g x *: df).
Proof.
move=> dfx dgx.
have -> : f * g = (
fun
p
=> p.
1 * p.
2)
\o (
fun
y
=> (
f y, g y))
by [].
apply: is_diff_eq.
by rewrite funeqE => ?; rewrite /= [_ * g _]mulrC.
Qed.
Lemma
diffM
(
f
g
: V -> R)
x
:
differentiable f x -> differentiable g x ->
'd (
f * g)
x = f x \*: 'd g x + g x \*: 'd f x :> (
V -> R).
Proof.
by move=> /differentiableP df /differentiableP dg; rewrite diff_val. Qed.
Lemma
differentiableM
(
f
g
: V -> R)
x
:
differentiable f x -> differentiable g x -> differentiable (
f * g)
x.
Proof.
by move=> /differentiableP df /differentiableP dg. Qed.
Fact
dinv
(
x
: R)
:
x != 0 -> continuous (
fun
h
: R => - x ^- 2 *: h)
/\
(
fun
x
=> x^-1)
%R \o shift x = cst (
x^-1)
%R +
(
fun
h
: R => - x ^- 2 *: h)
+o_ (
0 : R)
id.
Proof.
Lemma
diff_Rinv
(
x
: R)
: x != 0 ->
'd GRing.inv x = (
fun
h
: R => - x ^- 2 *: h)
:> (
R -> R).
Proof.
Lemma
differentiable_Rinv
(
x
: R)
: x != 0 ->
differentiable (
GRing.inv : R -> R)
x.
Proof.
by move=> xn0; apply/diff_locallyP; rewrite diff_Rinv //; apply: dinv.
Qed.
Lemma
diffV
(
f
: V -> R)
x
: differentiable f x -> f x != 0 ->
'd (
fun
y
=> (
f y)
^-1)
x = - (
f x)
^- 2 \*: 'd f x :> (
V -> R).
Proof.
Lemma
differentiableV
(
f
: V -> R)
x
:
differentiable f x -> f x != 0 -> differentiable (
fun
y
=> (
f y)
^-1)
x.
Proof.
Global Instance
is_diffX
(
f
df
: V -> R)
n
x
:
is_diff x f df -> is_diff x (
f ^+ n.
+1) (
n.
+1%:R * f x ^+ n *: df).
Proof.
Lemma
differentiableX
(
f
: V -> R)
n
x
:
differentiable f x -> differentiable (
f ^+ n.
+1)
x.
Proof.
by move=> /differentiableP. Qed.
Lemma
diffX
(
f
: V -> R)
n
x
:
differentiable f x ->
'd (
f ^+ n.
+1)
x = n.
+1%:R * f x ^+ n \*: 'd f x :> (
V -> R).
Proof.
by move=> /differentiableP df; rewrite diff_val. Qed.
End DifferentialR3_numFieldType.
Section
DeriveRU
.
Variables (
R
: numFieldType) (
U
: normedModType R).
Implicit Types f : R -> U.
Let
der1
f
x
: derivable f x 1 ->
f \o shift x = cst (
f x)
+ (
*:%R^~ (
f^`()
x))
+o_ (
0 : R)
id.
Proof.
move=> df; apply/eqaddoE; have /derivable_nbhsP := df.
have -> : (
fun
h
=> (
f \o shift x)
h%:A)
= f \o shift x.
by rewrite funeqE=> ?; rewrite [_%:A]mulr1.
by rewrite derive1E =>->.
Qed.
Lemma
deriv1E
f
x
: derivable f x 1 -> 'd f x = (
*:%R^~ (
f^`()
x))
:> (
R -> U).
Proof.
Lemma
diff1E
f
x
:
differentiable f x -> 'd f x = (
fun
h
=> h *: f^`()
x)
:> (
R -> U).
Proof.
Lemma
derivable1_diffP
f
x
: derivable f x 1 <-> differentiable f x.
Proof.
Lemma
derivable_within_continuous
f
(
i
: interval R)
:
{in i, forall
x,
derivable f x 1} -> {within [set` i], continuous f}.
Proof.
move=> di; apply/continuous_in_subspaceT => z /[1!inE] zA.
apply/differentiable_continuous; rewrite -derivable1_diffP.
by apply: di; rewrite inE.
Qed.
End DeriveRU.
Section
DeriveVW
.
Variables (
R
: numFieldType) (
V
W
: normedModType R).
Implicit Types f : V -> W.
Lemma
derivable1P
f
x
v
:
derivable f x v <-> derivable (
fun
h
: R => f (
h *: v + x))
0 1.
Proof.
Lemma
derivableP
f
x
v
: derivable f x v -> is_derive x v f (
'D_v f x).
Proof.
Lemma
diff_derivable
f
a
v
: differentiable f a -> derivable f a v.
Proof.
move=> dfa; apply/derivable1P/derivable1_diffP.
by apply: differentiable_comp; rewrite ?scale0r ?add0r.
Qed.
Global Instance
is_derive_cst
(
a
: W) (
x
v
: V)
: is_derive x v (
cst a)
0.
Proof.
Lemma
is_derive_eq
f
(
x
v
: V) (
df
f'
: W)
:
is_derive x v f f' -> f' = df -> is_derive x v f df.
Proof.
by move=> ? <-. Qed.
End DeriveVW.
Section
Derive_lemmasVW
.
Variables (
R
: numFieldType) (
V
W
: normedModType R).
Implicit Types f g : V -> W.
Fact
der_add
f
g
(
x
v
: V)
: derivable f x v -> derivable g x v ->
(
fun
h
=> h^-1 *: (((
f + g)
\o shift x) (
h *: v)
- (
f + g)
x))
@
0^' --> 'D_v f x + 'D_v g x.
Proof.
Lemma
deriveD
f
g
(
x
v
: V)
: derivable f x v -> derivable g x v ->
'D_v (
f + g)
x = 'D_v f x + 'D_v g x.
Proof.
Lemma
derivableD
f
g
(
x
v
: V)
:
derivable f x v -> derivable g x v -> derivable (
f + g)
x v.
Proof.
Global Instance
is_deriveD
f
g
(
x
v
: V) (
df
dg
: W)
:
is_derive x v f df -> is_derive x v g dg -> is_derive x v (
f + g) (
df + dg).
Proof.
Global Instance
is_derive_sum
n
(
h
: 'I_n -> V -> W) (
x
v
: V)
(
dh
: 'I_n -> W)
: (
forall
i,
is_derive x v (
h i) (
dh i))
->
is_derive x v (
\sum_(
i
< n)
h i) (
\sum_(
i
< n)
dh i).
Proof.
Lemma
derivable_sum
n
(
h
: 'I_n -> V -> W) (
x
v
: V)
:
(
forall
i,
derivable (
h i)
x v)
-> derivable (
\sum_(
i
< n)
h i)
x v.
Proof.
Lemma
derive_sum
n
(
h
: 'I_n -> V -> W) (
x
v
: V)
:
(
forall
i,
derivable (
h i)
x v)
->
'D_v (
\sum_(
i
< n)
h i)
x = \sum_(
i
< n)
'D_v (
h i)
x.
Proof.
Fact
der_opp
f
(
x
v
: V)
: derivable f x v ->
(
fun
h
=> h^-1 *: (((
- f)
\o shift x) (
h *: v)
- (
- f)
x))
@
0^' --> - 'D_v f x.
Proof.
move=> df; evar (
g : R -> W)
; rewrite [X in X @ _](
_ : _ = g)
/=; last first.
by rewrite funeqE => h; rewrite !scalerDr !scalerN -opprD -scalerBr /g.
exact: cvgN.
Qed.
Lemma
deriveN
f
(
x
v
: V)
: derivable f x v ->
'D_v (
- f)
x = - 'D_v f x.
Proof.
Lemma
derivableN
f
(
x
v
: V)
:
derivable f x v -> derivable (
- f)
x v.
Proof.
by move=> df; apply/cvg_ex; exists (
- 'D_v f x)
; apply: der_opp. Qed.
Global Instance
is_deriveN
f
(
x
v
: V) (
df
: W)
:
is_derive x v f df -> is_derive x v (
- f) (
- df).
Proof.
Global Instance
is_deriveB
f
g
(
x
v
: V) (
df
dg
: W)
:
is_derive x v f df -> is_derive x v g dg -> is_derive x v (
f - g) (
df - dg).
Proof.
Lemma
deriveB
f
g
(
x
v
: V)
: derivable f x v -> derivable g x v ->
'D_v (
f - g)
x = 'D_v f x - 'D_v g x.
Proof.
by move=> /derivableP df /derivableP dg; rewrite derive_val. Qed.
Lemma
derivableB
f
g
(
x
v
: V)
:
derivable f x v -> derivable g x v -> derivable (
f - g)
x v.
Proof.
by move=> /derivableP df /derivableP dg. Qed.
Fact
der_scal
f
(
k
: R) (
x
v
: V)
: derivable f x v ->
(
fun
h
=> h^-1 *: ((
k \*: f \o shift x) (
h *: v)
- (
k \*: f)
x))
@
(
0 : R)
^' --> k *: 'D_v f x.
Proof.
move=> df; evar (
h : R -> W)
; rewrite [X in X @ _](
_ : _ = h)
/=; last first.
rewrite funeqE => r.
by rewrite scalerBr !scalerA mulrC -!scalerA -!scalerBr /h.
exact: cvgZr.
Qed.
Lemma
deriveZ
f
(
k
: R) (
x
v
: V)
: derivable f x v ->
'D_v (
k \*: f)
x = k *: 'D_v f x.
Proof.
Lemma
derivableZ
f
(
k
: R) (
x
v
: V)
:
derivable f x v -> derivable (
k \*: f)
x v.
Proof.
by move=> df; apply/cvg_ex; exists (
k *: 'D_v f x)
; apply: der_scal.
Qed.
Global Instance
is_deriveZ
f
(
k
: R) (
x
v
: V) (
df
: W)
:
is_derive x v f df -> is_derive x v (
k \*: f) (
k *: df).
Proof.
End Derive_lemmasVW.
Section
Derive_lemmasVR
.
Variables (
R
: numFieldType) (
V
: normedModType R).
Implicit Types f g : V -> R.
Fact
der_mult
f
g
(
x
v
: V)
:
derivable f x v -> derivable g x v ->
(
fun
h
=> h^-1 *: (((
f * g)
\o shift x) (
h *: v)
- (
f * g)
x))
@
(
0 : R)
^' --> f x *: 'D_v g x + g x *: 'D_v f x.
Proof.
Lemma
deriveM
f
g
(
x
v
: V)
: derivable f x v -> derivable g x v ->
'D_v (
f * g)
x = f x *: 'D_v g x + g x *: 'D_v f x.
Proof.
Lemma
derivableM
f
g
(
x
v
: V)
:
derivable f x v -> derivable g x v -> derivable (
f * g)
x v.
Proof.
Global Instance
is_deriveM
f
g
(
x
v
: V) (
df
dg
: R)
:
is_derive x v f df -> is_derive x v g dg ->
is_derive x v (
f * g) (
f x *: dg + g x *: df).
Proof.
Global Instance
is_deriveX
f
n
(
x
v
: V) (
df
: R)
:
is_derive x v f df -> is_derive x v (
f ^+ n.
+1) ((
n.
+1%:R * f x ^+n)
*: df).
Proof.
Lemma
derivableX
f
n
(
x
v
: V)
: derivable f x v -> derivable (
f ^+ n.
+1)
x v.
Proof.
by move/derivableP. Qed.
Lemma
deriveX
f
n
(
x
v
: V)
: derivable f x v ->
'D_v (
f ^+ n.
+1)
x = (
n.
+1%:R * f x ^+ n)
*: 'D_v f x.
Proof.
by move=> /derivableP df; rewrite derive_val. Qed.
Fact
der_inv
f
(
x
v
: V)
: f x != 0 -> derivable f x v ->
(
fun
h
=> h^-1 *: (((
fun
y
=> (
f y)
^-1)
\o shift x) (
h *: v)
- (
f x)
^-1))
@
(
0 : R)
^' --> - (
f x)
^-2 *: 'D_v f x.
Proof.
move=> fxn0 df.
have /derivable1P/derivable1_diffP/differentiable_continuous := df.
move=> /continuous_withinNx; rewrite scale0r add0r => fc.
have fn0 : (
0 : R)
^' [set
h
| f (
h *: v + x)
!= 0].
apply: (
fc [set
x
| x != 0])
; exists `|f x|; first by rewrite /= normr_gt0.
move=> y; rewrite /= => yltfx.
by apply/eqP => y0; move: yltfx; rewrite y0 subr0 ltxx.
have : (
fun
h
=> - ((
f x)
^-1 * (
f (
h *: v + x))
^-1)
*:
(
h^-1 *: (
f (
h *: v + x)
- f x)))
@ (
0 : R)
^' -->
- (
f x)
^- 2 *: 'D_v f x.
by apply: cvgM => //; apply: cvgN; rewrite expr2 invfM; apply: cvgM;
[exact: cvg_cst| exact: cvgV].
apply: cvg_trans => A [_/posnumP[e] /= Ae].
move: fn0; apply: filter_app; near=> h => /= fhvxn0.
have he : ball 0 e%:num (
h : R)
by near: h; exists e%:num => /=.
have hn0 : h != 0 by near: h; exists e%:num => /=.
suff <- :
- ((
f x)
^-1 * (
f (
h *: v + x))
^-1)
*: (
h^-1 *: (
f (
h *: v + x)
- f x))
=
h^-1 *: ((
f (
h *: v + x))
^-1 - (
f x)
^-1)
by exact: Ae.
rewrite scalerA mulrC -scalerA; congr (
_ *: _).
apply/eqP; rewrite scaleNr eqr_oppLR opprB scalerBr.
rewrite -scalerA [_ *: f _]mulVf // [_%:A]mulr1.
by rewrite mulrC -scalerA [_ *: f _]mulVf // [_%:A]mulr1.
Unshelve.
all: by end_near. Qed.
Lemma
deriveV
f
x
v
: f x != 0 -> derivable f x v ->
'D_v (
fun
y
=> (
f y)
^-1)
x = - (
f x)
^- 2 *: 'D_v f x.
Proof.
Lemma
derivableV
f
(
x
v
: V)
:
f x != 0 -> derivable f x v -> derivable (
fun
y
=> (
f y)
^-1)
x v.
Proof.
move=> df dg; apply/cvg_ex; exists (
- (
f x)
^- 2 *: 'D_v f x).
exact: der_inv.
Qed.
Lemma
derive1_cst
(
k
: V)
t
: (
cst k)
^`()
t = 0.
Proof.
End Derive_lemmasVR.
Lemma
EVT_max
(
R
: realType) (
f
: R -> R) (
a
b
: R)
:
a <= b -> {within `[a, b], continuous f} -> exists2
c,
c \in `[a, b]%R &
forall
t,
t \in `[a, b]%R -> f t <= f c.
Proof.
Lemma
EVT_min
(
R
: realType) (
f
: R -> R) (
a
b
: R)
:
a <= b -> {within `[a, b], continuous f} -> exists2
c,
c \in `[a, b]%R &
forall
t,
t \in `[a, b]%R -> f c <= f t.
Proof.
move=> leab fcont.
have /(
EVT_max leab)
[c clr fcmax] : {within `[a, b], continuous (
- f)
}.
by move=> ?; apply: continuousN => ?; exact: fcont.
by exists c => // ? /fcmax; rewrite ler_opp2.
Qed.
Lemma
__deprecated__le0r_cvg_map
(
R
: realFieldType) (
T
: topologicalType) (
F
: set (
set T))
(
FF
: ProperFilter F) (
f
: T -> R)
:
(
\forall
x
\near F, 0 <= f x)
-> cvg (
f @ F)
-> 0 <= lim (
f @ F).
Proof.
by move=> ? ?; rewrite limr_ge. Qed.
#[deprecated(
since="mathcomp-analysis 0.6.0",
note="generalized by `limr_ge`")
]
Notation
le0r_cvg_map
:= __deprecated__le0r_cvg_map (
only parsing).
Lemma
__deprecated__ler0_cvg_map
(
R
: realFieldType) (
T
: topologicalType) (
F
: set (
set T))
(
FF
: ProperFilter F) (
f
: T -> R)
:
(
\forall
x
\near F, f x <= 0)
-> cvg (
f @ F)
-> lim (
f @ F)
<= 0.
Proof.
by move=> ? ?; rewrite limr_le. Qed.
#[deprecated(
since="mathcomp-analysis 0.6.0",
note="generalized by `limr_le`")
]
Notation
ler0_cvg_map
:= __deprecated__ler0_cvg_map (
only parsing).
Lemma
__deprecated__ler_cvg_map
(
R
: realFieldType) (
T
: topologicalType) (
F
: set (
set T))
(
FF
: ProperFilter F) (
f
g
: T -> R)
:
(
\forall
x
\near F, f x <= g x)
-> cvg (
f @ F)
-> cvg (
g @ F)
->
lim (
f @ F)
<= lim (
g @ F).
Proof.
by move=> ? ? ?; rewrite ler_lim. Qed.
#[deprecated(
since="mathcomp-analysis 0.6.0",
note="subsumed by `ler_lim`")
]
Notation
ler_cvg_map
:= __deprecated__ler_cvg_map (
only parsing).
Lemma
derive1_at_max
(
R
: realFieldType) (
f
: R -> R) (
a
b
c
: R)
:
a <= b -> (
forall
t,
t \in `]a, b[%R -> derivable f t 1)
-> c \in `]a, b[%R ->
(
forall
t,
t \in `]a, b[%R -> f t <= f c)
-> is_derive c 1 f 0.
Proof.
Lemma
derive1_at_min
(
R
: realFieldType) (
f
: R -> R) (
a
b
c
: R)
:
a <= b -> (
forall
t,
t \in `]a, b[%R -> derivable f t 1)
-> c \in `]a, b[%R ->
(
forall
t,
t \in `]a, b[%R -> f c <= f t)
-> is_derive c 1 f 0.
Proof.
move=> leab fdrvbl cab cmin; apply: DeriveDef; first exact: fdrvbl.
apply/eqP; rewrite -oppr_eq0; apply/eqP.
rewrite -deriveN; last exact: fdrvbl.
suff df : is_derive c 1 (
- f)
0 by rewrite derive_val.
apply: derive1_at_max leab _ (
cab)
_ => t tab; first exact/derivableN/fdrvbl.
by rewrite ler_opp2; apply: cmin.
Qed.
Lemma
Rolle
(
R
: realType) (
f
: R -> R) (
a
b
: R)
:
a < b -> (
forall
x,
x \in `]a, b[%R -> derivable f x 1)
->
{within `[a, b], continuous f} -> f a = f b ->
exists2
c,
c \in `]a, b[%R & is_derive c 1 f 0.
Proof.
move=> ltab fdrvbl fcont faefb.
have [cmax cmaxab fcmax] := EVT_max (
ltW ltab)
fcont.
have [cmaxeaVb|] := boolP (
cmax \in [set a; b])
; last first.
rewrite notin_set => /not_orP[/eqP cnea /eqP cneb].
have {}cmaxab : cmax \in `]a, b[%R.
by rewrite in_itv /= !lt_def !(
itvP cmaxab)
cnea eq_sym cneb.
exists cmax => //; apply: derive1_at_max (
ltW ltab)
fdrvbl cmaxab _ => t tab.
by apply: fcmax; rewrite in_itv /= !ltW // (
itvP tab).
have [cmin cminab fcmin] := EVT_min (
ltW ltab)
fcont.
have [cmineaVb|] := boolP (
cmin \in [set a; b])
; last first.
rewrite notin_set => /not_orP[/eqP cnea /eqP cneb].
have {}cminab : cmin \in `]a, b[%R.
by rewrite in_itv /= !lt_def !(
itvP cminab)
cnea eq_sym cneb.
exists cmin => //; apply: derive1_at_min (
ltW ltab)
fdrvbl cminab _ => t tab.
by apply: fcmin; rewrite in_itv /= !ltW // (
itvP tab).
have midab : (
a + b)
/ 2 \in `]a, b[%R by apply: mid_in_itvoo.
exists ((
a + b)
/ 2)
=> //; apply: derive1_at_max (
ltW ltab)
fdrvbl (
midab)
_.
move=> t tab.
suff fcst s : s \in `]a, b[%R -> f s = f cmax by rewrite !fcst.
move=> sab.
apply/eqP; rewrite eq_le fcmax; last by rewrite in_itv /= !ltW ?(
itvP sab).
suff -> : f cmax = f cmin by rewrite fcmin // in_itv /= !ltW ?(
itvP sab).
by move: cmaxeaVb cmineaVb; rewrite 2!inE => -[|] -> [|] ->.
Qed.
Lemma
MVT
(
R
: realType) (
f
df
: R -> R) (
a
b
: R)
:
a < b -> (
forall
x,
x \in `]a, b[%R -> is_derive x 1 f (
df x))
->
{within `[a, b], continuous f} ->
exists2
c,
c \in `]a, b[%R & f b - f a = df c * (
b - a).
Proof.
Lemma
MVT_segment
(
R
: realType) (
f
df
: R -> R) (
a
b
: R)
:
a <= b -> (
forall
x,
x \in `]a, b[%R -> is_derive x 1 f (
df x))
->
{within `[a, b], continuous f} ->
exists2
c,
c \in `[a, b]%R & f b - f a = df c * (
b - a).
Proof.
move=> leab fdrvbl fcont; case: ltgtP leab => // [altb|aeb]; last first.
by exists a; [rewrite inE/= aeb lexx|rewrite aeb !subrr mulr0].
have [c cab D] := MVT altb fdrvbl fcont.
by exists c => //; rewrite in_itv /= ltW (
itvP cab).
Qed.
Lemma
ler0_derive1_nincr
(
R
: realType) (
f
: R -> R) (
a
b
: R)
:
(
forall
x,
x \in `]a, b[%R -> derivable f x 1)
->
(
forall
x,
x \in `]a, b[%R -> f^`()
x <= 0)
->
{within `[a,b], continuous f} ->
forall
x
y,
a <= x -> x <= y -> y <= b -> f y <= f x.
Proof.
Lemma
le0r_derive1_ndecr
(
R
: realType) (
f
: R -> R) (
a
b
: R)
:
(
forall
x,
x \in `]a, b[%R -> derivable f x 1)
->
(
forall
x,
x \in `]a, b[%R -> 0 <= f^`()
x)
->
{within `[a,b], continuous f} ->
forall
x
y,
a <= x -> x <= y -> y <= b -> f x <= f y.
Proof.
move=> fdrvbl dfge0 fcont x y; rewrite -[f _ <= _]ler_opp2.
apply (
@ler0_derive1_nincr _ (
- f))
=> t tab; first exact/derivableN/fdrvbl.
rewrite derive1E deriveN; last exact: fdrvbl.
by rewrite oppr_le0 -derive1E; apply: dfge0.
by apply: continuousN; exact: fcont.
Qed.
Lemma
derive1_comp
(
R
: realFieldType) (
f
g
: R -> R)
x
:
derivable f x 1 -> derivable g (
f x)
1 ->
(
g \o f)
^`()
x = g^`() (
f x)
* f^`()
x.
Proof.
move=> /derivable1_diffP df /derivable1_diffP dg.
rewrite derive1E'; last exact/differentiable_comp.
rewrite diff_comp // !derive1E' //= -[X in 'd _ _ X = _]mulr1.
by rewrite [LHS]linearZ mulrC.
Qed.
Section
is_derive_instances
.
Variables (
R
: numFieldType) (
V
: normedModType R).
Lemma
derivable_cst
(
x
: V)
: derivable (
fun=> x)
0 1.
Proof.
exact/diff_derivable. Qed.
Lemma
derivable_id
(
x
v
: V)
: derivable id x v.
Proof.
exact/diff_derivable. Qed.
Global Instance
is_derive_id
(
x
v
: V)
: is_derive x v id v.
Proof.
Global Instance
is_deriveNid
(
x
v
: V)
: is_derive x v -%R (
- v).
Proof.
End is_derive_instances.
Lemma
trigger_derive
(
R
: realType) (
f
: R -> R)
x
x1
y1
:
is_derive x 1 f x1 -> x1 = y1 -> is_derive x 1 f y1.
Proof.
by move=> Hi <-. Qed.