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.