Library mathcomp.analysis.derive
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice.
From mathcomp Require Import ssralg ssrnum fintype bigop order matrix interval.
Require Import boolp reals.
Require Import classical_sets posnum nngnum topology prodnormedzmodule.
Require Import normedtype landau forms.
From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice.
From mathcomp Require Import ssralg ssrnum fintype bigop order matrix interval.
Require Import boolp reals.
Require Import classical_sets posnum nngnum topology prodnormedzmodule.
Require Import normedtype landau forms.
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
f^`() == the derivative of f of domain R
f^`(n) == the nth derivative of f of domain R
Set Implicit Arguments.
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"). (* printing *)
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 ∧ ∀ x,
f x = f (lim F) + df (x - lim F) +o_(x \near F) (x - lim F))).
Fact diff_key : ∀ T, T → unit.
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))).
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)
}.
Lemma diffP (F : filter_on V) (f : V → W) :
differentiable f F ↔
continuous ('d f F) ∧
(∀ x, f x = f (lim F) + 'd f F (x - lim F) +o_(x \near F) (x - lim F)).
Lemma diff_continuous (x : filter_on V) (f : V → W) :
differentiable f x → continuous ('d f x).
We should have a continuous class or structure
Hint Extern 0 (continuous _) ⇒ exact: diff_continuous : core.
Lemma diffE (F : filter_on V) (f : V → W) :
differentiable f F →
∀ x, f x = f (lim F) + 'd f F (x - lim F) +o_(x \near F) (x - lim F).
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.
End Differential.
Section Differential_numFieldType.
Context {K : numFieldType } {V W : normedModType K}.
Hint Extern 0 (continuous _) ⇒ exact: diff_continuous : core.
Lemma diff_locallyxP (x : V) (f : V → W) :
differentiable f x ↔ continuous ('d f x) ∧
∀ h, f (h + x) = f x + 'd f x h +o_(h \near 0 : V) h.
Lemma diff_locallyx (x : V) (f : V → W) : differentiable f x →
∀ h, f (h + x) = f x + 'd f x h +o_(h \near 0 : V) h.
Lemma diff_locallyxC (x : V) (f : V → W) : differentiable f x →
∀ h, f (x + h) = f x + 'd f x h +o_(h \near 0 : V) h.
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).
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).
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])).
Hint Extern 0 (differentiable _ _) ⇒ solve[apply: ex_diff] : core.
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).
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 diffE (F : filter_on V) (f : V → W) :
differentiable f F →
∀ x, f x = f (lim F) + 'd f F (x - lim F) +o_(x \near F) (x - lim F).
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.
End Differential.
Section Differential_numFieldType.
Context {K : numFieldType } {V W : normedModType K}.
Hint Extern 0 (continuous _) ⇒ exact: diff_continuous : core.
Lemma diff_locallyxP (x : V) (f : V → W) :
differentiable f x ↔ continuous ('d f x) ∧
∀ h, f (h + x) = f x + 'd f x h +o_(h \near 0 : V) h.
Lemma diff_locallyx (x : V) (f : V → W) : differentiable f x →
∀ h, f (h + x) = f x + 'd f x h +o_(h \near 0 : V) h.
Lemma diff_locallyxC (x : V) (f : V → W) : differentiable f x →
∀ h, f (x + h) = f x + 'd f x h +o_(h \near 0 : V) h.
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).
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).
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])).
Hint Extern 0 (differentiable _ _) ⇒ solve[apply: ex_diff] : core.
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).
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}.
split in multiple bits:
- a linear map which is locally bounded is a little o of 1
- the identity is a littleo of 1
Lemma differentiable_continuous (x : V) (f : V → W) :
differentiable f x → {for x, continuous f}.
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.
Lemma littleo_lim0 (f : X → Y) (h : _ → Z) (x : X) :
f @ x --> (0 : Y) → [o_x f of h] x = 0.
End littleo_lemmas.
Section diff_locally_converse_tentative.
differentiable f x → {for x, continuous f}.
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.
Lemma littleo_lim0 (f : X → Y) (h : _ → Z) (x : X) :
f @ x --> (0 : Y) → [o_x f of h] x = 0.
End littleo_lemmas.
Section diff_locally_converse_tentative.
if there exist A and B s.t. f(a + h) = A + B h + o(h) then
f is differentiable at a, A = f(a) and B = f'(a)
this is a consequence of diff_continuous and eqolim0
indeed the differential being b *: idfun is locally bounded
and thus a littleo of 1, and so is id
This can be generalized to any dimension
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.
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^').
(* printing *)
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.
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.
Lemma derivable_nbhsx (f : V → W) a v :
derivable f a v → ∀ h, f (a + h *: v) = f a + h *: 'D_v f a
+o_(h \near (nbhs (0 : R))) h.
Lemma derivable_nbhsxP (f : V → W) a v :
derivable f a v ↔ ∀ h, f (a + h *: v) = f a + h *: 'D_v f a
+o_(h \near (nbhs (0 :R))) h.
End DifferentialR.
Notation "''D_' v f" := (derive f ^~ v).
Notation "''D_' v f c" := (derive f c v). (* printing *)
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.
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.
Definition derive1 V (f : R → V) (a : R) :=
lim ((fun h ⇒ h^-1 *: (f (h + a) - f a)) @ 0^').
Lemma derive1E V (f : R → V) a : f^`() a = 'D_1 f a.
f \o shift x = cst a + b *: idfun +o_ (0 : R) id → f x = a.
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^').
(* printing *)
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.
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.
Lemma derivable_nbhsx (f : V → W) a v :
derivable f a v → ∀ h, f (a + h *: v) = f a + h *: 'D_v f a
+o_(h \near (nbhs (0 : R))) h.
Lemma derivable_nbhsxP (f : V → W) a v :
derivable f a v ↔ ∀ h, f (a + h *: v) = f a + h *: 'D_v f a
+o_(h \near (nbhs (0 :R))) h.
End DifferentialR.
Notation "''D_' v f" := (derive f ^~ v).
Notation "''D_' v f c" := (derive f c v). (* printing *)
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.
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.
Definition derive1 V (f : R → V) (a : R) :=
lim ((fun h ⇒ h^-1 *: (f (h + a) - f a)) @ 0^').
Lemma derive1E V (f : R → V) a : f^`() a = 'D_1 f a.
Is it necessary?
Lemma derive1E' V f a : differentiable (f : R → V) a →
f^`() a = 'd f a 1.
Definition derive1n V n (f : R → V) := iter n (@derive1 V) f.
Lemma derive1n0 V (f : R → V) : f^`(0) = f.
Lemma derive1n1 V (f : R → V) : f^`(1) = f^`().
Lemma derive1nS V (f : R → V) n : f^`(n.+1) = f^`(n)^`().
Lemma derive1Sn V (f : R → V) n : f^`(n.+1) = f^`()^`(n).
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.
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.
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.
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.
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.
f^`() a = 'd f a 1.
Definition derive1n V n (f : R → V) := iter n (@derive1 V) f.
Lemma derive1n0 V (f : R → V) : f^`(0) = f.
Lemma derive1n1 V (f : R → V) : f^`(1) = f^`().
Lemma derive1nS V (f : R → V) n : f^`(n.+1) = f^`(n)^`().
Lemma derive1Sn V (f : R → V) n : f^`(n.+1) = f^`()^`(n).
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.
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.
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.
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.
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.
NB: could be generalized with K : absRingType instead of R; DONE?
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.
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.
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.
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.
TODO: generalize
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.
Lemma compoO_eqox (U V' W' : normedModType R) (f : U → V')
(g : V' → W') :
∀ x : U, [o_ (0 : V') id of g] ([O_ (0 : U) id of f] x) =o_(x \near 0 : U) x.
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.
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).
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).
Lemma diff_cst (V W : normedModType R) a x : ('d (cst a) x : V → W) = 0.
Variables (V W : normedModType R).
Lemma differentiable_cst (W' : normedModType R) (a : W') (x : V) :
differentiable (cst a) x.
Global Instance is_diff_cst (a : W) (x : V) : is_diff x (cst a) 0.
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).
Lemma differentiableD (f g : V → W) x :
differentiable f x → differentiable g x → differentiable (f + g) x.
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).
Lemma differentiable_sum n (f : 'I_n → V → W) (x : V) :
(∀ i, differentiable (f i) x) → differentiable (\sum_(i < n) f i) x.
Lemma diffN (f : V → W) x :
differentiable f x → 'd (- f) x = - ('d f x : V → W) :> (V → W).
Lemma differentiableN (f : V → W) x :
differentiable f x → differentiable (- f) x.
Global Instance is_diffN (f df : V → W) x :
is_diff x f df → is_diff x (- f) (- df).
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).
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).
Lemma differentiableB (f g : V → W) x :
differentiable f x → differentiable g x → differentiable (f \- g) x.
Lemma diffZ (f : V → W) k x :
differentiable f x → 'd (k *: f) x = k \*: 'd f x :> (V → W).
Lemma differentiableZ (f : V → W) k x :
differentiable f x → differentiable (k *: f) x.
Global Instance is_diffZ (f df : V → W) k x :
is_diff x f df → is_diff x (k *: f) (k *: df).
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) :> (_ → _).
Lemma differentiableZl (k : V → R) (f : W) x :
differentiable k x → differentiable (fun z ⇒ k z *: f) x.
Lemma diff_lin (V' W' : normedModType R) (f : {linear V' → W'}) x :
continuous f → 'd f x = f :> (V' → W').
Lemma linear_differentiable (V' W' : normedModType R) (f : {linear V' → W'})
x : continuous f → differentiable f x.
Global Instance is_diff_id (x : V) : is_diff x id id.
Global Instance is_diff_scaler (k : R) (x : V) : is_diff x ( *:%R k) ( *:%R k).
Global Instance is_diff_scalel (x k : R) :
is_diff k ( *:%R ^~ x) ( *:%R ^~ x).
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.
Lemma linear_lipschitz (V' W' : normedModType R) (f : {linear V' → W'}) :
continuous f → exists2 k, k > 0 & ∀ x, `|f x| ≤ k × `|x|.
Lemma linear_eqO (V' W' : normedModType R) (f : {linear V' → W'}) :
continuous f → (f : V' → W') =O_ (0 : V') id.
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.
Lemma compOo_eqox (U V' W' : normedModType R) (f : U → V')
(g : V' → W') : ∀ x,
[O_ (0 : V') id of g] ([o_ (0 : U) id of f] x) =o_(x \near 0 : U) x.
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) ∧ ∀ y,
g (f (y + x)) = g (f x) + ('d g (f x) \o 'd f x) y +o_(y \near 0 : U) y.
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').
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.
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.
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 & ∀ u v, `|f u v| ≤ k × `|u| × `|v|.
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.
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.
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').
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.
Definition Rmult_rev (y x : R) := x × y.
Canonical rev_Rmult := @RevOp _ _ _ Rmult_rev (@GRing.mul [ringType of R])
(fun _ _ ⇒ erefl).
Lemma Rmult_is_linear x : linear (@GRing.mul [ringType of R] x : R → R).
Canonical Rmult_linear x := Linear (Rmult_is_linear x).
Lemma Rmult_rev_is_linear y : linear (Rmult_rev y : R → R).
Canonical Rmult_rev_linear y := Linear (Rmult_rev_is_linear y).
Canonical Rmult_bilinear :=
[bilinear of (@GRing.mul [ringType of [lmodType R of R]])].
Global Instance is_diff_Rmult (p : R×R ) :
is_diff p (fun q ⇒ q.1 × q.2) (fun q ⇒ p.1 × q.2 + q.1 × p.2).
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.
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.
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').
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.
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)).
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).
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).
Lemma differentiableM (f g : V → R) x :
differentiable f x → differentiable g x → differentiable (f × g) x.
(g : V' → W') :
[o_ (0 : V') id of g] \o [O_ (0 : U) id of f] =o_ (0 : U) id.
Lemma compoO_eqox (U V' W' : normedModType R) (f : U → V')
(g : V' → W') :
∀ x : U, [o_ (0 : V') id of g] ([O_ (0 : U) id of f] x) =o_(x \near 0 : U) x.
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.
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).
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).
Lemma diff_cst (V W : normedModType R) a x : ('d (cst a) x : V → W) = 0.
Variables (V W : normedModType R).
Lemma differentiable_cst (W' : normedModType R) (a : W') (x : V) :
differentiable (cst a) x.
Global Instance is_diff_cst (a : W) (x : V) : is_diff x (cst a) 0.
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).
Lemma differentiableD (f g : V → W) x :
differentiable f x → differentiable g x → differentiable (f + g) x.
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).
Lemma differentiable_sum n (f : 'I_n → V → W) (x : V) :
(∀ i, differentiable (f i) x) → differentiable (\sum_(i < n) f i) x.
Lemma diffN (f : V → W) x :
differentiable f x → 'd (- f) x = - ('d f x : V → W) :> (V → W).
Lemma differentiableN (f : V → W) x :
differentiable f x → differentiable (- f) x.
Global Instance is_diffN (f df : V → W) x :
is_diff x f df → is_diff x (- f) (- df).
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).
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).
Lemma differentiableB (f g : V → W) x :
differentiable f x → differentiable g x → differentiable (f \- g) x.
Lemma diffZ (f : V → W) k x :
differentiable f x → 'd (k *: f) x = k \*: 'd f x :> (V → W).
Lemma differentiableZ (f : V → W) k x :
differentiable f x → differentiable (k *: f) x.
Global Instance is_diffZ (f df : V → W) k x :
is_diff x f df → is_diff x (k *: f) (k *: df).
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) :> (_ → _).
Lemma differentiableZl (k : V → R) (f : W) x :
differentiable k x → differentiable (fun z ⇒ k z *: f) x.
Lemma diff_lin (V' W' : normedModType R) (f : {linear V' → W'}) x :
continuous f → 'd f x = f :> (V' → W').
Lemma linear_differentiable (V' W' : normedModType R) (f : {linear V' → W'})
x : continuous f → differentiable f x.
Global Instance is_diff_id (x : V) : is_diff x id id.
Global Instance is_diff_scaler (k : R) (x : V) : is_diff x ( *:%R k) ( *:%R k).
Global Instance is_diff_scalel (x k : R) :
is_diff k ( *:%R ^~ x) ( *:%R ^~ x).
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.
Lemma linear_lipschitz (V' W' : normedModType R) (f : {linear V' → W'}) :
continuous f → exists2 k, k > 0 & ∀ x, `|f x| ≤ k × `|x|.
Lemma linear_eqO (V' W' : normedModType R) (f : {linear V' → W'}) :
continuous f → (f : V' → W') =O_ (0 : V') id.
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.
Lemma compOo_eqox (U V' W' : normedModType R) (f : U → V')
(g : V' → W') : ∀ x,
[O_ (0 : V') id of g] ([o_ (0 : U) id of f] x) =o_(x \near 0 : U) x.
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) ∧ ∀ y,
g (f (y + x)) = g (f x) + ('d g (f x) \o 'd f x) y +o_(y \near 0 : U) y.
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').
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.
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.
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 & ∀ u v, `|f u v| ≤ k × `|u| × `|v|.
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.
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.
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').
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.
Definition Rmult_rev (y x : R) := x × y.
Canonical rev_Rmult := @RevOp _ _ _ Rmult_rev (@GRing.mul [ringType of R])
(fun _ _ ⇒ erefl).
Lemma Rmult_is_linear x : linear (@GRing.mul [ringType of R] x : R → R).
Canonical Rmult_linear x := Linear (Rmult_is_linear x).
Lemma Rmult_rev_is_linear y : linear (Rmult_rev y : R → R).
Canonical Rmult_rev_linear y := Linear (Rmult_rev_is_linear y).
Canonical Rmult_bilinear :=
[bilinear of (@GRing.mul [ringType of [lmodType R of R]])].
Global Instance is_diff_Rmult (p : R×R ) :
is_diff p (fun q ⇒ q.1 × q.2) (fun q ⇒ p.1 × q.2 + q.1 × p.2).
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.
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.
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').
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.
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)).
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).
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).
Lemma differentiableM (f g : V → R) x :
differentiable f x → differentiable g x → differentiable (f × g) x.
fixme using
(1 / (h + x) - 1 / x) / h = - 1 / (h + x) x = -1/x^2 + o(1)
Fact dinv (x : R) :
x != 0 → continuous (fun h : R ⇒ - x ^- 2 *: h) ∧
(fun x ⇒ x^-1) \o shift x = cst (x^-1) +
(fun h : R ⇒ - x ^- 2 *: h) +o_ (0 : R) id.
Lemma diff_Rinv (x : R) : x != 0 →
'd GRing.inv x = (fun h : R ⇒ - x ^- 2 *: h) :> (R → R).
Lemma differentiable_Rinv (x : R) : x != 0 →
differentiable (GRing.inv : R → R) x.
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).
Lemma differentiableV (f : V → R) x :
differentiable f x → f x != 0 → differentiable (fun y ⇒ (f y)^-1) x.
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).
Lemma differentiableX (f : V → R) n x :
differentiable f x → differentiable (f ^+ n.+1) x.
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).
End DifferentialR3_numFieldType.
Section Derive.
Variables (R : numFieldType) (V W : normedModType R).
Let der1 (U : normedModType R) (f : R → U) x : derivable f x 1 →
f \o shift x = cst (f x) + ( *:%R^~ (f^`() x)) +o_ (0 : R) id.
Lemma deriv1E (U : normedModType R) (f : R → U) x :
derivable f x 1 → 'd f x = ( *:%R^~ (f^`() x)) :> (R → U).
Lemma diff1E (U : normedModType R) (f : R → U) x :
differentiable f x → 'd f x = (fun h ⇒ h *: f^`() x) :> (R → U).
Lemma derivable1_diffP (U : normedModType R) (f : R → U) x :
derivable f x 1 ↔ differentiable f x.
Lemma derivable1P (U : normedModType R) (f : V → U) x v :
derivable f x v ↔ derivable (fun h : R ⇒ f (h *: v + x)) 0 1.
Lemma derivableP (U : normedModType R) (f : V → U) x v :
derivable f x v → is_derive x v f ('D_v f x).
Global Instance is_derive_cst (U : normedModType R) (a : U) (x v : V) :
is_derive x v (cst a) 0.
Fact der_add (f g : V → W) (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.
Lemma deriveD (f g : V → W) (x v : V) : derivable f x v → derivable g x v →
'D_v (f + g) x = 'D_v f x + 'D_v g x.
Lemma derivableD (f g : V → W) (x v : V) :
derivable f x v → derivable g x v → derivable (f + g) x v.
Global Instance is_deriveD (f g : V → W) (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).
Global Instance is_derive_sum n (f : 'I_n → V → W) (x v : V)
(df : 'I_n → W) : (∀ i, is_derive x v (f i) (df i)) →
is_derive x v (\sum_(i < n) f i) (\sum_(i < n) df i).
Lemma derivable_sum n (f : 'I_n → V → W) (x v : V) :
(∀ i, derivable (f i) x v) → derivable (\sum_(i < n) f i) x v.
Lemma derive_sum n (f : 'I_n → V → W) (x v : V) :
(∀ i, derivable (f i) x v) →
'D_v (\sum_(i < n) f i) x = \sum_(i < n) 'D_v (f i) x.
Fact der_opp (f : V → W) (x v : V) : derivable f x v →
(fun h ⇒ h^-1 *: (((- f) \o shift x) (h *: v) - (- f) x)) @
0^' --> - 'D_v f x.
Lemma deriveN (f : V → W) (x v : V) : derivable f x v →
'D_v (- f) x = - 'D_v f x.
Lemma derivableN (f : V → W) (x v : V) :
derivable f x v → derivable (- f) x v.
Global Instance is_deriveN (f : V → W) (x v : V) (df : W) :
is_derive x v f df → is_derive x v (- f) (- df).
Lemma is_derive_eq (V' W' : normedModType R) (f : V' → W') (x v : V')
(df f' : W') : is_derive x v f f' → f' = df → is_derive x v f df.
Global Instance is_deriveB (f g : V → W) (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).
Lemma deriveB (f g : V → W) (x v : V) : derivable f x v → derivable g x v →
'D_v (f - g) x = 'D_v f x - 'D_v g x.
Lemma derivableB (f g : V → W) (x v : V) :
derivable f x v → derivable g x v → derivable (f - g) x v.
Fact der_scal (f : V → W) (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.
Lemma deriveZ (f : V → W) (k : R) (x v : V) : derivable f x v →
'D_v (k \*: f) x = k *: 'D_v f x.
Lemma derivableZ (f : V → W) (k : R) (x v : V) :
derivable f x v → derivable (k \*: f) x v.
Global Instance is_deriveZ (f : V → W) (k : R) (x v : V) (df : W) :
is_derive x v f df → is_derive x v (k \*: f) (k *: df).
Fact der_mult (f g : V → R) (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.
Lemma deriveM (f g : V → R) (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.
Lemma derivableM (f g : V → R) (x v : V) :
derivable f x v → derivable g x v → derivable (f × g) x v.
Global Instance is_deriveM (f g : V → R) (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).
Global Instance is_deriveX (f : V → R) 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).
Lemma derivableX (f : V → R) n (x v : V) :
derivable f x v → derivable (f ^+ n.+1) x v.
Lemma deriveX (f : V → R) n (x v : V) :
derivable f x v →
'D_v (f ^+ n.+1) x = (n.+1%:R × f x ^+ n) *: 'D_v f x.
Fact der_inv (f : V → R) (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.
Lemma deriveV (f : V → R) x v : f x != 0 → derivable f x v →
'D_v[fun y ⇒ (f y)^-1] x = - (f x) ^- 2 *: 'D_v f x.
Lemma derivableV (f : V → R) (x v : V) :
f x != 0 → derivable f x v → derivable (fun y ⇒ (f y)^-1) x v.
End Derive.
Lemma EVT_max (R : realType) (f : R → R) (a b : R) : (* TODO : Filter not infered *)
a ≤ b → {in `[a, b]%R, continuous f} → exists2 c, c \in `[a, b]%R &
∀ t, t \in `[a, b]%R → f t ≤ f c.
Lemma EVT_min (R : realType) (f : R → R) (a b : R) :
a ≤ b → {in `[a, b]%R, continuous f} → exists2 c, c \in `[a, b]%R &
∀ t, t \in `[a, b]%R → f c ≤ f t.
Lemma cvg_at_rightE (R : numFieldType) (V : normedModType R) (f : R → V) x :
cvg (f @ x^') → lim (f @ x^') = lim (f @ at_right x).
Lemma cvg_at_leftE (R : numFieldType) (V : normedModType R) (f : R → V) x :
cvg (f @ x^') → lim (f @ x^') = lim (f @ at_left x).
Lemma le0r_cvg_map (R : realFieldType) (T : topologicalType) (F : set (set T))
(FF : ProperFilter F) (f : T → R) :
(\∀ x \near F, 0 ≤ f x) → cvg (f @ F) → 0 ≤ lim (f @ F).
Lemma ler0_cvg_map (R : realFieldType) (T : topologicalType) (F : set (set T))
(FF : ProperFilter F) (f : T → R) :
(\∀ x \near F, f x ≤ 0) → cvg (f @ F) → lim (f @ F) ≤ 0.
Lemma ler_cvg_map (R : realFieldType) (T : topologicalType) (F : set (set T)) (FF : ProperFilter F)
(f g : T → R) :
(\∀ x \near F, f x ≤ g x) → cvg (f @ F) → cvg (g @ F) →
lim (f @ F) ≤ lim (g @ F).
Lemma derive1_at_max (R : realFieldType) (f : R → R) (a b c : R) :
a ≤ b → (∀ t, t \in `]a, b[%R → derivable f t 1) → c \in `]a, b[%R →
(∀ t, t \in `]a, b[%R → f t ≤ f c) → is_derive c 1 f 0.
Lemma derive1_at_min (R : realFieldType) (f : R → R) (a b c : R) :
a ≤ b → (∀ t, t \in `]a, b[%R → derivable f t 1) → c \in `]a, b[%R →
(∀ t, t \in `]a, b[%R → f c ≤ f t) → is_derive c 1 f 0.
Lemma Rolle (R : realType) (f : R → R) (a b : R) :
a < b → (∀ x, x \in `]a, b[%R → derivable f x 1) →
{in `[a, b]%R, continuous f} → f a = f b →
exists2 c, c \in `]a, b[%R & is_derive c 1 f 0.
Lemma MVT (R : realType) (f df : R → R) (a b : R) :
a ≤ b → (∀ x, x \in `]a, b[%R → is_derive x 1 f (df x)) →
{in `[a, b]%R, continuous f} →
exists2 c, c \in `[a, b]%R & f b - f a = df c × (b - a).
Lemma ler0_derive1_nincr (R : realType) (f : R → R) (a b : R) :
(∀ x, x \in `[a, b]%R → derivable f x 1) →
(∀ x, x \in `[a, b]%R → f^`() x ≤ 0) →
∀ x y, a ≤ x → x ≤ y → y ≤ b → f y ≤ f x.
Lemma le0r_derive1_ndecr (R : realType) (f : R → R) (a b : R) :
(∀ x, x \in `[a, b]%R → derivable f x 1) →
(∀ x, x \in `[a, b]%R → 0 ≤ f^`() x) →
∀ x y, a ≤ x → x ≤ y → y ≤ b → f x ≤ f y.
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.
Section is_derive_instances.
Variables (R : numFieldType) (V : normedModType R).
Lemma derivable_cst (x : V) : derivable (fun⇒ x) 0 1.
Lemma derivable_id (x v : V) : derivable id x v.
Global Instance is_derive_id (x v : V) : is_derive x v id v.
Global Instance is_deriveNid (x v : V) : is_derive x v -%R (- v).
End is_derive_instances.
x != 0 → continuous (fun h : R ⇒ - x ^- 2 *: h) ∧
(fun x ⇒ x^-1) \o shift x = cst (x^-1) +
(fun h : R ⇒ - x ^- 2 *: h) +o_ (0 : R) id.
Lemma diff_Rinv (x : R) : x != 0 →
'd GRing.inv x = (fun h : R ⇒ - x ^- 2 *: h) :> (R → R).
Lemma differentiable_Rinv (x : R) : x != 0 →
differentiable (GRing.inv : R → R) x.
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).
Lemma differentiableV (f : V → R) x :
differentiable f x → f x != 0 → differentiable (fun y ⇒ (f y)^-1) x.
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).
Lemma differentiableX (f : V → R) n x :
differentiable f x → differentiable (f ^+ n.+1) x.
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).
End DifferentialR3_numFieldType.
Section Derive.
Variables (R : numFieldType) (V W : normedModType R).
Let der1 (U : normedModType R) (f : R → U) x : derivable f x 1 →
f \o shift x = cst (f x) + ( *:%R^~ (f^`() x)) +o_ (0 : R) id.
Lemma deriv1E (U : normedModType R) (f : R → U) x :
derivable f x 1 → 'd f x = ( *:%R^~ (f^`() x)) :> (R → U).
Lemma diff1E (U : normedModType R) (f : R → U) x :
differentiable f x → 'd f x = (fun h ⇒ h *: f^`() x) :> (R → U).
Lemma derivable1_diffP (U : normedModType R) (f : R → U) x :
derivable f x 1 ↔ differentiable f x.
Lemma derivable1P (U : normedModType R) (f : V → U) x v :
derivable f x v ↔ derivable (fun h : R ⇒ f (h *: v + x)) 0 1.
Lemma derivableP (U : normedModType R) (f : V → U) x v :
derivable f x v → is_derive x v f ('D_v f x).
Global Instance is_derive_cst (U : normedModType R) (a : U) (x v : V) :
is_derive x v (cst a) 0.
Fact der_add (f g : V → W) (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.
Lemma deriveD (f g : V → W) (x v : V) : derivable f x v → derivable g x v →
'D_v (f + g) x = 'D_v f x + 'D_v g x.
Lemma derivableD (f g : V → W) (x v : V) :
derivable f x v → derivable g x v → derivable (f + g) x v.
Global Instance is_deriveD (f g : V → W) (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).
Global Instance is_derive_sum n (f : 'I_n → V → W) (x v : V)
(df : 'I_n → W) : (∀ i, is_derive x v (f i) (df i)) →
is_derive x v (\sum_(i < n) f i) (\sum_(i < n) df i).
Lemma derivable_sum n (f : 'I_n → V → W) (x v : V) :
(∀ i, derivable (f i) x v) → derivable (\sum_(i < n) f i) x v.
Lemma derive_sum n (f : 'I_n → V → W) (x v : V) :
(∀ i, derivable (f i) x v) →
'D_v (\sum_(i < n) f i) x = \sum_(i < n) 'D_v (f i) x.
Fact der_opp (f : V → W) (x v : V) : derivable f x v →
(fun h ⇒ h^-1 *: (((- f) \o shift x) (h *: v) - (- f) x)) @
0^' --> - 'D_v f x.
Lemma deriveN (f : V → W) (x v : V) : derivable f x v →
'D_v (- f) x = - 'D_v f x.
Lemma derivableN (f : V → W) (x v : V) :
derivable f x v → derivable (- f) x v.
Global Instance is_deriveN (f : V → W) (x v : V) (df : W) :
is_derive x v f df → is_derive x v (- f) (- df).
Lemma is_derive_eq (V' W' : normedModType R) (f : V' → W') (x v : V')
(df f' : W') : is_derive x v f f' → f' = df → is_derive x v f df.
Global Instance is_deriveB (f g : V → W) (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).
Lemma deriveB (f g : V → W) (x v : V) : derivable f x v → derivable g x v →
'D_v (f - g) x = 'D_v f x - 'D_v g x.
Lemma derivableB (f g : V → W) (x v : V) :
derivable f x v → derivable g x v → derivable (f - g) x v.
Fact der_scal (f : V → W) (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.
Lemma deriveZ (f : V → W) (k : R) (x v : V) : derivable f x v →
'D_v (k \*: f) x = k *: 'D_v f x.
Lemma derivableZ (f : V → W) (k : R) (x v : V) :
derivable f x v → derivable (k \*: f) x v.
Global Instance is_deriveZ (f : V → W) (k : R) (x v : V) (df : W) :
is_derive x v f df → is_derive x v (k \*: f) (k *: df).
Fact der_mult (f g : V → R) (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.
Lemma deriveM (f g : V → R) (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.
Lemma derivableM (f g : V → R) (x v : V) :
derivable f x v → derivable g x v → derivable (f × g) x v.
Global Instance is_deriveM (f g : V → R) (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).
Global Instance is_deriveX (f : V → R) 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).
Lemma derivableX (f : V → R) n (x v : V) :
derivable f x v → derivable (f ^+ n.+1) x v.
Lemma deriveX (f : V → R) n (x v : V) :
derivable f x v →
'D_v (f ^+ n.+1) x = (n.+1%:R × f x ^+ n) *: 'D_v f x.
Fact der_inv (f : V → R) (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.
Lemma deriveV (f : V → R) x v : f x != 0 → derivable f x v →
'D_v[fun y ⇒ (f y)^-1] x = - (f x) ^- 2 *: 'D_v f x.
Lemma derivableV (f : V → R) (x v : V) :
f x != 0 → derivable f x v → derivable (fun y ⇒ (f y)^-1) x v.
End Derive.
Lemma EVT_max (R : realType) (f : R → R) (a b : R) : (* TODO : Filter not infered *)
a ≤ b → {in `[a, b]%R, continuous f} → exists2 c, c \in `[a, b]%R &
∀ t, t \in `[a, b]%R → f t ≤ f c.
Lemma EVT_min (R : realType) (f : R → R) (a b : R) :
a ≤ b → {in `[a, b]%R, continuous f} → exists2 c, c \in `[a, b]%R &
∀ t, t \in `[a, b]%R → f c ≤ f t.
Lemma cvg_at_rightE (R : numFieldType) (V : normedModType R) (f : R → V) x :
cvg (f @ x^') → lim (f @ x^') = lim (f @ at_right x).
Lemma cvg_at_leftE (R : numFieldType) (V : normedModType R) (f : R → V) x :
cvg (f @ x^') → lim (f @ x^') = lim (f @ at_left x).
Lemma le0r_cvg_map (R : realFieldType) (T : topologicalType) (F : set (set T))
(FF : ProperFilter F) (f : T → R) :
(\∀ x \near F, 0 ≤ f x) → cvg (f @ F) → 0 ≤ lim (f @ F).
Lemma ler0_cvg_map (R : realFieldType) (T : topologicalType) (F : set (set T))
(FF : ProperFilter F) (f : T → R) :
(\∀ x \near F, f x ≤ 0) → cvg (f @ F) → lim (f @ F) ≤ 0.
Lemma ler_cvg_map (R : realFieldType) (T : topologicalType) (F : set (set T)) (FF : ProperFilter F)
(f g : T → R) :
(\∀ x \near F, f x ≤ g x) → cvg (f @ F) → cvg (g @ F) →
lim (f @ F) ≤ lim (g @ F).
Lemma derive1_at_max (R : realFieldType) (f : R → R) (a b c : R) :
a ≤ b → (∀ t, t \in `]a, b[%R → derivable f t 1) → c \in `]a, b[%R →
(∀ t, t \in `]a, b[%R → f t ≤ f c) → is_derive c 1 f 0.
Lemma derive1_at_min (R : realFieldType) (f : R → R) (a b c : R) :
a ≤ b → (∀ t, t \in `]a, b[%R → derivable f t 1) → c \in `]a, b[%R →
(∀ t, t \in `]a, b[%R → f c ≤ f t) → is_derive c 1 f 0.
Lemma Rolle (R : realType) (f : R → R) (a b : R) :
a < b → (∀ x, x \in `]a, b[%R → derivable f x 1) →
{in `[a, b]%R, continuous f} → f a = f b →
exists2 c, c \in `]a, b[%R & is_derive c 1 f 0.
Lemma MVT (R : realType) (f df : R → R) (a b : R) :
a ≤ b → (∀ x, x \in `]a, b[%R → is_derive x 1 f (df x)) →
{in `[a, b]%R, continuous f} →
exists2 c, c \in `[a, b]%R & f b - f a = df c × (b - a).
Lemma ler0_derive1_nincr (R : realType) (f : R → R) (a b : R) :
(∀ x, x \in `[a, b]%R → derivable f x 1) →
(∀ x, x \in `[a, b]%R → f^`() x ≤ 0) →
∀ x y, a ≤ x → x ≤ y → y ≤ b → f y ≤ f x.
Lemma le0r_derive1_ndecr (R : realType) (f : R → R) (a b : R) :
(∀ x, x \in `[a, b]%R → derivable f x 1) →
(∀ x, x \in `[a, b]%R → 0 ≤ f^`() x) →
∀ x y, a ≤ x → x ≤ y → y ≤ b → f x ≤ f y.
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.
Section is_derive_instances.
Variables (R : numFieldType) (V : normedModType R).
Lemma derivable_cst (x : V) : derivable (fun⇒ x) 0 1.
Lemma derivable_id (x v : V) : derivable id x v.
Global Instance is_derive_id (x v : V) : is_derive x v id v.
Global Instance is_deriveNid (x v : V) : is_derive x v -%R (- v).
End is_derive_instances.
Trick to trigger type class resolution