Library mathcomp.analysis.derive

(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval.
Require Import boolp reals mathcomp_extra classical_sets signed functions.
Require Import topology prodnormedzmodule 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])).
#[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).

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.
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 *)
#[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.

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.

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.

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.

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)%R \o shift x = cst (x^-1)%R +
  (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 derive1_cst (R : numFieldType) (V : normedModType R) (k : V) t :
  (cst k)^`() t = 0.

Lemma EVT_max (R : realType) (f : R → R) (a b : R) : (* TODO : Filter not infered *)
  a ≤ b → {within `[a, b], 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 → {within `[a, b], 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).
Arguments cvg_at_rightE {R V} f 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).
Arguments cvg_at_leftE {R V} f 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) →
  {within `[a, b], 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)) →
  {within `[a, b], continuous f} →
  exists2 c, c \in `]a, b[%R & f b - f a = df c × (b - a).

Weakens MVT to work when the interval is a single point.
Lemma MVT_segment (R : realType) (f df : R → R) (a b : R) :
  a ≤ b → (∀ 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).

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) →
  {within `[a,b], continuous f} →
  ∀ 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) →
  {within `[a,b], continuous f} →
  ∀ 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
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.