Module mathcomp.analysis.derive

From HB Require Import structures.
From mathcomp Require Import boot order ssralg ssrnum matrix interval.
From mathcomp Require Import poly sesquilinear.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import mathcomp_extra boolp contra classical_sets.
From mathcomp Require Import functions reals interval_inference topology.
From mathcomp Require Import prodnormedzmodule tvs normedtype landau.

# 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 is_derive x v f df == the derivative of a function f at point x along v is df and f is derivable at x along v is_diff x f df == the differential of a function f at point x is df and f is differentiable at point x ``` Naming convention in this file: - lemmas of the form `... -> derivable f x v` are named `derivable*` (e.g., `derivableV`, `derivableM`) or `*derivable` (e.g., `diff_derivable`) - lemmas of the form `D_v f x = ...` are named `derive*` (e.g., `deriveVP, `deriveM`) - lemmas of the form ``f^`() x = ...`` are named `derive1*` (e.g., `derive1_cst`, `derive1_comp`) - lemmas of the form `... -> is_derive x v f df` are named `is_derive*` (e.g., `is_derive_cst`) - lemmas of the form `... -> is_diff x f df` are named `is_diff*` (e.g., `is_diff_cst`) # Automatic derivation and differentiation with `is_diff` and `is_derive` Statements of the form `is_diff` and `is_derive` are typeclasses registered via `Instance` declarations with a proof `ex_derive`/`ex_diff` of derivability/differentiability of the expression and a proof `derive_val`/`diff_val` of the value of the derivative/differential of the function; so that typeclass resolution can automatically synthesize the differential/derivative of a compound expression from the differentials/derivatives of its parts, instead of requiring the user to prove and compute derivatives by hand. ## Lemmas of the form `is_derive` and `is_diff` For a compound expression, e.g., built from f and g, state the goal with the expected derivative/differential and let typeclass resolution fill the proof by `apply: is_derive_eq` or `apply: is_diff_eq`: ``` Lemma is_derive_example (W : normedModType R) (t : R^o) (f g : R^o -> W) (f' g' : W) v : is_derive t v f f' -> is_derive t v g g' -> is_derive t v (f + g) (f' + g'). Proof. move => is_der_f is_der_g. by apply: is_derive_eq. Qed. ``` The proof is inferred structurally by chaining declared `is_derive` or `is_diff` instances matching the pattern of the goal stated. To verify if a given expression is derivable or differentiable, you can use `apply: ex_derive` or `apply: ex_diff`, given the right `is_derive _` or `is_diff _` instances are defined such as: ``` Hypothesis derivable_f : forall t, derivable f t 1. Hypothesis derivable_h : forall t, derivable h t 1. Local Instance is_derive_f t : is_derive t 1 f ('D_1 f t). by apply: derivableP. Qed. Local Instance is_derive_h t : is_derive t 1 h ('D_1 h t). by apply: derivableP. Qed. Lemma is_derivable_example (t : R^o) : derivable (f + h) t 1. Proof. apply/ex_derive. Qed. ``` To verify the value of a given function you can apply `derive_val` or `diff_val`, given the right `is_derive/diff` instances are defined, e.g.: ``` Lemma is_derive_val_example t : 'D_1 (f + h) t = 'D_1 f t + 'D_1 h t. Proof. by apply/derive_val. Qed. ``` It is worth mentioning that every differentiable function is derivable via the lemma `diff_derivable` and that a function is differentiable iff it is derivable in the case of functions from $\mathbb{R}$ to a normed module, via the lemma `derivable1_diffP`.

Unset SsrOldRewriteGoalsOrder.
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 ^` ()" (format "f ^` ()").
Reserved Notation "f ^` ( n )" (format "f ^` ( n )").

Section Differential.
Context { : numDomainType} { : normedModType K}.

Definition ( : filter_on V) (_ : phantom (set_system V) F) ( : V -> W) :=
  (get (fun ( : {linear V -> W}) => continuous df /\ forall ,
      f x = f (lim F) + df (x - lim F) +o_( \near F) (x - lim F))).

Local Notation := (@diff _ (Phantom _ (nbhs x)) f).

Fact : forall , T -> unit

Proof.

by constructor. Qed.

Variant ( : V -> W) ( : filter_on V)
  ( : phantom (set_system V) x) : Prop := of
  (continuous ('d f x) /\
  f = cst (f (lim x)) + 'd f x \o center (lim x) +o_x (center (lim x))).

Local Notation f F :=
  (@differentiable_def f _ (Phantom _ (nbhs F))).

Class ( : filter_on V) ( : phantom (set_system V) x) ( : V -> W)
  ( : V -> W) := DiffDef {
     : differentiable f x ;
     : 'd f x = df :> (V -> W)
  }.
Hint Mode is_diff_def - - ! - : typeclass_instances.

Lemma ( : filter_on V) ( : V -> W) :
  differentiable f F <->
  continuous ('d f F) /\
  (forall , f x = f (lim F) + 'd f F (x - lim F) +o_( \near F) (x - lim F)).

Proof.

by split=> [[] |]; last constructor; rewrite funeqE. Qed.

Lemma ( : filter_on V) ( : V -> W) :
differentiable f x -> continuous ('d f x).

Proof.

by move=> /diffP []. Qed.

Hint Extern 0 (continuous _) => solve[apply: diff_continuous] : core.

Lemma ( : filter_on V) ( : V -> W) :
differentiable f F ->
forall , f x = f (lim F) + 'd f F (x - lim F) +o_( \near F) (x - lim F).

Proof.

by move=> /diffP []. Qed.

Lemma ( : V) ( : V -> W) ( : V -> V) :
[o_x e of f] = [o_ 0 (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 \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 \near _, _ <= _](near_shift 0) subr0; apply: fe.
Unshelve. all: by end_near. Qed.

End Differential.

Section Differential_numFieldType.
Context { : numFieldType } { : normedModType K}.

Local Notation f F :=
  (@differentiable_def _ _ _ f _ (Phantom _ (nbhs F))).
Local Notation := (@diff _ _ _ _ (Phantom _ (nbhs x)) f).
Hint Extern 0 (continuous _) => solve[now apply: diff_continuous] : core.

Lemma ( : V) ( : V -> W) :
  differentiable f x <-> continuous ('d f x) /\
  forall , f (h + x) = f x + 'd f x h +o_( \near 0) h.

Proof.

split=> [dxf|[dfc dxf]].
  split => //; apply: eqaddoEx => h; have /diffE -> := dxf.
  rewrite lim_id // addrK; congr (_ + _); rewrite littleo_center0 /= addrK.
  by congr ('o); rewrite funeqE => k /=; rewrite addrK.
apply/diffP; split=> //; apply: eqaddoEx; move=> y.
rewrite lim_id // -[in LHS](subrK x y) dxf; congr (_ + _).
rewrite -(comp_centerK x id) -[X in the_littleo _ _ _ X](comp_centerK x).
by rewrite -[_ (y - x)]/((_ \o (center x)) y) -littleo_center0.
Qed.

Lemma ( : V) ( : V -> W) : differentiable f x ->
forall , f (h + x) = f x + 'd f x h +o_( \near 0) h.

Proof.

by move=> /diff_locallyxP []. Qed.

Lemma ( : V) ( : V -> W) : differentiable f x ->
forall , f (x + h) = f x + 'd f x h +o_( \near 0) h.

Proof.

by move=> ?; apply/eqaddoEx => h; rewrite [x + h]addrC diff_locallyx. Qed.

Lemma ( : V) ( : V -> W) :
differentiable f x <->
continuous ('d f x) /\ (f \o shift x = cst (f x) + 'd f x +o_ 0 id).

Proof.

by apply: iff_trans (diff_locallyxP _ _) _; rewrite funeqE. Qed.

Lemma ( : V) ( : V -> W) : differentiable f x ->
(f \o shift x = cst (f x) + 'd f x +o_ 0 id).

Proof.

by move=> /diff_locallyP []. Qed.

End Differential_numFieldType.

Notation := (@diff _ _ _ _ (Phantom _ (nbhs F)) f).
Notation f F := (@differentiable_def _ _ _ f _ (Phantom _ (nbhs F))).

Notation := (is_diff_def (Phantom _ (nbhs F))).
#[global] Hint Extern 0 (differentiable _ _) => solve[apply: ex_diff] : core.
#[global] Hint Extern 0 ({for _, continuous _}) =>
solve[now apply: diff_continuous] : core.

Lemma ( : numDomainType) ( : normedModType R) ( : V -> W) :
differentiable f x -> is_diff x f ('d f x).

Proof.

by move=> ?; apply: DiffDef. Qed.

Section jacobian.

Definition ( : numFieldType) ( : 'rV[R]_n -> 'rV[R]_m) :=
lin1_mx ('d f p).

End jacobian.

Notation := (jacobian f p).

Section DifferentialR.

Context { : numFieldType} { : normedModType R}.

Lemma ( : V) ( : V -> W) :
differentiable f x -> {for x, continuous f}.

Proof.

move=> /diff_locallyP [dfc]; rewrite -addrA.
rewrite (littleo_bigO_eqo (cst (1 : R))).
by apply/eqOP; near=> k; rewrite /cst [`|1|]normr1 mulr1; near do by [].
rewrite addfo; last by move=> /eqolim; rewrite cvg_comp_shift add0r.
by apply/eqolim0P; apply: (cvg_trans (dfc 0)); rewrite linear0.
Unshelve. all: by end_near. Qed.

Section littleo_lemmas.
Variables ( : normedModType R).

Lemma ( : X -> Y) : `| [o_( \near x) (1 : R) of f x]| = 0.

Proof.

rewrite /cst /=; have [e /(_ (`|e x|/2) _)/nbhs_singleton /=] := littleo.
rewrite pmulr_lgt0 // [`|1|]normr1 mulr1 [leLHS]splitr gerDr pmulr_lle0 //.
by move=> /implyP; case : real_ltgtP; rewrite ?realE ?normrE //= lexx.
Qed.

Lemma ( : X -> Y) ( : _ -> Z) ( : X) :
f @ x --> 0 -> [o_x f of h] x = 0.

Proof.

move/eqolim0P => ->; have [k /(_ _ [gt0 of 1 : R])/=] := littleo.
by move=> /nbhs_singleton; rewrite mul1r normm_littleo normr_le0 => /eqP.
Qed.

End littleo_lemmas.

Section diff_locally_converse_tentative.
Lemma ( : R -> R) ( : R) :
f \o shift x = cst a + b *: idfun +o_ 0 id -> f x = a.

Proof.

rewrite funeqE => /(_ 0) /=; rewrite add0r => ->.
by rewrite -[LHS]/(_ 0 + _ 0 + _ 0) /cst [X in a + X]scaler0 littleo_lim0 ?addr0.
Qed.

End diff_locally_converse_tentative.

Definition ( : V -> W) :=
  lim ((fun => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ 0^').

Local Notation := (derive f ^~ v).
Local Notation := (derive f c v).

Definition ( : V -> W) :=
  cvg ((fun => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ 0^').

Class ( : V) ( : V -> W) ( : W) := DeriveDef {
   : derivable f a v;
   : 'D_v f a = df
}.

Lemma ( : V -> W) :
  derivable f a v ->
  (fun => (f \o shift a) (h *: v)) = (cst (f a)) +
    (fun => h *: ('D_v f a)) +o_ (nbhs 0) id.

Proof.

move=> df; apply/eqaddoP => _/posnumP[e].
rewrite -nbhs_nearE nbhs_simpl /= dnbhsE; split; last first.
  apply/principal_filterP.
  rewrite opprD -![(_ + _ : _ -> _) _]/(_ + _) scale0r add0r.
  by rewrite addrCA addKr normrN scale0r !normr0 mulr0.
have /eqolimP := df.
move=> /eqaddoP /(_ e%:num) /(_ [gt0 of e%:num]).
apply: filter_app; rewrite /= !near_simpl near_withinE; near=> h => hN0.
rewrite /= opprD -![(_ + _ : _ -> _) _]/(_ + _) -![(- _ : _ -> _) _]/(- _).
rewrite /cst /= [`|1|]normr1 mulr1 => dfv.
rewrite addrA -[X in X + _]scale1r -(@mulVf _ h) //.
rewrite mulrC -scalerA -scalerBr normrZ.
by rewrite -ler_pdivlMl ?normr_gt0// mulrC mulfK ?normr_eq0.
Unshelve. all: by end_near. Qed.

Lemma ( : V -> W) :
  derivable f a v <->
  (fun => (f \o shift a) (h *: v)) = (cst (f a)) +
    (fun => h *: ('D_v f a)) +o_ (nbhs 0) id.

Proof.

split; first exact: derivable_nbhs.
move=> df; apply/cvg_ex; exists ('D_v f a).
apply/(@eqolimP _ _ _ (dnbhs_filter_on _))/eqaddoP => _/posnumP[e].
have /eqaddoP /(_ e%:num) /(_ [gt0 of e%:num]) := df.
rewrite /= !(near_simpl, near_withinE); apply: filter_app; near=> h.
rewrite /= opprD -![(_ + _ : _ -> _) _]/(_ + _) -![(- _ : _ -> _) _]/(- _).
rewrite /cst /= [`|1|]normr1 mulr1 addrA => dfv hN0.
rewrite -[X in _ - X]scale1r -(@mulVf _ h) //.
rewrite -scalerA -scalerBr normrZ normfV ler_pdivrMl ?normr_gt0 //.
by rewrite mulrC.
Unshelve. all: by end_near. Qed.

Lemma ( : V -> W) :
derivable f a v -> forall , f (a + h *: v) = f a + h *: 'D_v f a
+o_( \near (nbhs 0)) h.

Proof.

move=> /derivable_nbhs; rewrite funeqE => df.
by apply: eqaddoEx => h; have /= := df h; rewrite addrC => ->.
Qed.

Lemma ( : V -> W) :
derivable f a v <-> forall , f (a + h *: v) = f a + h *: 'D_v f a
+o_( \near (nbhs 0)) h.

Proof.

split; first exact: derivable_nbhsx.
move=> df; apply/derivable_nbhsP; apply/eqaddoE; rewrite funeqE => h.
by rewrite /= addrC df.
Qed.

Lemma ( : V -> W) ( : V) : derivable f x 0.

Proof.

apply: (is_cvg_near_cst 0) => //=.
near=> h.
by rewrite scaler0 add0r subrr scaler0.
Unshelve. all: by end_near. Qed.

Lemma ( : V -> W) ( : V) : 'D_0 f x = 0.

Proof.

apply/lim_near_cst => //=.
near=> h.
by rewrite scaler0 add0r subrr scaler0.
Unshelve. all: by end_near. Qed.

Lemma ( : V -> W) ( : V) : is_derive x 0 f 0.

Proof.

by split; [exact/derivable0|rewrite derive0]. Qed.

End DifferentialR.

Notation := (derive f ^~ v).
Notation := (derive f c v).
#[global] Hint Extern 0 (derivable _ _ _) => solve[apply: ex_derive] : core.

Section DifferentialR_numFieldType.
Context { : numFieldType} { : normedModType R}.

Lemma ( : V -> W) ( : V) :
differentiable f a -> 'D_v f a = 'd f a v.

Proof.

rewrite /derive => /diff_locally -> /=; set k := 'o _.
evar (g : R -> W); rewrite [X in X @ _](_ : _ = g) /=.
  rewrite funeqE=> h.
  by rewrite -[_ - _]addrA addrC subrKA scalerDr addrC linearZ scalerA /g.
apply: cvg_lim => //.
pose g1 : R -> W := fun => (h^-1 * h) *: 'd f a v.
pose g2 : R -> W := fun : R => h^-1 *: k (h *: v ).
rewrite (_ : g = g1 + g2) ?funeqE // -(addr0 (_ _ v)); apply: cvgD.
  rewrite -(scale1r (_ _ v)); apply: cvgZr_tmp => /= X [e e0].
  rewrite /ball_ /= => eX.
  apply/nbhs_ballP.
  by exists e => //= x _ x0; apply eX; rewrite mulVf//= subrr normr0.
rewrite /g2.
have [->|v0] := eqVneq v 0.
  rewrite (_ : (fun _ => _) = cst 0)//.
  by rewrite funeqE => ?; rewrite scaler0 /k littleo_lim0 // scaler0.
apply/cvgrPdist_lt => e e0.
rewrite nearE /=; apply/nbhs_ballP.
have /(littleoP [littleo of k]) /nbhs_ballP[i i0 Hi] : 0 < e / (2 * `|v|).
  by rewrite divr_gt0 // pmulr_rgt0 // normr_gt0.
exists (i / `|v|); first by rewrite /= divr_gt0 // normr_gt0.
move=> /= j; rewrite /ball /= /ball_ add0r normrN.
rewrite ltr_pdivlMr ?normr_gt0 // => jvi j0.
rewrite add0r normrN normrZ -ltr_pdivlMl ?normr_gt0 ?invr_neq0 //.
have /Hi/le_lt_trans -> // : ball 0 i (j *: v).
  by rewrite -ball_normE/= add0r normrN (le_lt_trans _ jvi) // normrZ.
rewrite -(mulrC e) -mulrA -ltr_pdivlMl // mulKf ?gt_eqF// normfV invrK.
rewrite ltr_pdivrMl; first by rewrite pmulr_rgt0 // normr_gt0.
rewrite normrZ mulrC -mulrA.
by rewrite ltr_pMl ?ltr1n // pmulr_rgt0 ?normm_gt0 // normr_gt0.
Qed.

End DifferentialR_numFieldType.

Section DifferentialR2.
Variable : numFieldType.
Implicit Type (V : normedModType R).

Lemma ( : 'rV[R]_m -> 'rV[R]_n) ( : 'rV[R]_m) :
differentiable f a -> 'D_ v f a = v *m jacobian f a.

Proof.

by move=> /deriveE->; rewrite /jacobian mul_rV_lin1. Qed.

Definition ( : R -> V) ( : R) :=
lim ((fun => h^-1 *: (f (h + a) - f a)) @ 0^').

Local Notation := (derive1 f).

Lemma ( : R -> V) : 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 : differentiable (f : R -> V) a ->
f^`() a = 'd f a 1.

Proof.

by move=> ?; rewrite derive1E deriveE. Qed.

Definition ( : R -> V) := iter n (@derive1 V) f.

Local Notation := (derive1n n f).

Lemma ( : R -> V) : f^`(0) = f.

Proof.

by []. Qed.

Lemma ( : R -> V) : f^`(1) = f^`().

Proof.

by []. Qed.

Lemma ( : R -> V) : f^`(n.+1) = f^`(n)^`().

Proof.

by []. Qed.

Lemma ( : R -> V) : f^`(n.+1) = f^`()^`(n).

Proof.

exact: iterSr. Qed.

End DifferentialR2.
Notation := (derive1 f) : classical_set_scope.
Notation := (derive1n n f) : classical_set_scope.
#[deprecated(since="mathcomp-analysis 1.13.0", note="renamed to `deriveEjacobian`")]
Notation := deriveEjacobian (only parsing).

Section DifferentialR3.
Variable : numFieldType.

Fact ( : normedModType R) ( : W) ( : V) : continuous (0 : V -> W) /\
cst a \o shift x = cst (cst a x) + \0 +o_ 0 id.

Proof.

split; first exact: cst_continuous.
apply/eqaddoE; rewrite addr0 funeqE => ? /=; rewrite -[LHS]addr0; congr (_ + _).
by rewrite littleoE; first exact: littleo0_subproof.
Qed.

Variables ( : normedModType R).

Fact ( : V -> W) :
  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 id.

Proof.

move=> df dg; split => [?|]; do ?exact: continuousD.
apply/(@eqaddoE R); rewrite funeqE => y /=.
by rewrite !fctE ![_ (_ + x)]diff_locallyx// addrACA addox addrACA.
Qed.

Fact ( : V -> W) :
differentiable f x -> continuous (- ('d f x : V -> W)) /\
(- f) \o shift x = cst (- f x) \- 'd f x +o_ 0 id.

Proof.

move=> df; split; first by move=> ?; apply: continuousN.
apply/eqaddoE; rewrite funeqE => y /=.
by rewrite -[(- f) _]/(- (_ _)) diff_locallyx// !opprD oppox.
Qed.

Lemma ( : normedModType R) ( : V' -> W') ( : V') :
is_diff x f f' -> f' = g -> is_diff x f g.

Proof.

by move=> ? <-. Qed.

Fact ( : V -> W) :
differentiable f x -> continuous (k \*: 'd f x) /\
(k *: f) \o shift x = cst ((k *: f) x) + k \*: 'd f x +o_ 0 id.

Proof.

move=> df; split; first by move=> ?; apply: continuousZl_tmp.
apply/eqaddoE; rewrite funeqE => y /=.
by rewrite -[(k *: f) _]/(_ *: _) diff_locallyx // !scalerDr scaleox.
Qed.

Fact ( : V -> R) ( : W) :
  differentiable k x ->
  continuous (fun : V => 'd k x z *: f) /\
  (fun => k z *: f) \o shift x =
    cst (k x *: f) + (fun => 'd k x z *: f) +o_ 0 id.

Proof.

move=> df; split.
move=> ?; exact/continuousZr_tmp/diff_continuous.
apply/eqaddoE; rewrite funeqE => y /=.
by rewrite diff_locallyx //= !scalerDl scaleolx.
Qed.

Fact ( : normedModType R) ( : {linear V' -> W'}) :
continuous f -> f \o shift x = cst (f x) + f +o_ 0 id.

Proof.

move=> df; apply: eqaddoE; rewrite funeqE => y /=.
rewrite linearD addrC -[LHS]addr0; congr (_ + _).
by rewrite littleoE; first exact: littleo0_subproof. (*fixme*)
Qed.

Lemma ( : normedModType R) ( : U -> V')
( : V' -> W') :
[o_ 0 id of g] \o [O_ 0 id of f] =o_ 0 id.

Proof.

apply/eqoP => _ /posnumP[e].
have /bigO_exP [_ /posnumP[k]] := bigOP [bigO of [O_ 0 id of f]].
have := littleoP [littleo of [o_ 0 id of g]].
move=> /(_ (e%:num / k%:num)) /(_ _) /nbhs_ballP [//|_ /posnumP[d] hd].
apply: filter_app; near=> x => leOxkx; apply: le_trans (hd _ _) _; last first.
by rewrite -ler_pdivlMl // invf_div mulrA divfK.
by rewrite -ball_normE /= distrC subr0 (le_lt_trans leOxkx) // -ltr_pdivlMl.
Unshelve. all: by end_near. Qed.

Lemma ( : normedModType R) ( : U -> V')
( : V' -> W') :
forall : U, [o_ 0 id of g] ([O_ 0 id of f] x) =o_( \near 0) x.

Proof.

by move=> x; rewrite -[LHS]/((_ \o _) x) compoO_eqo. Qed.

Lemma ( : normedModType R) ( : U -> V') ( : V' -> W') :
[O_ 0 id of g] \o [o_ 0 id of f] =o_ 0 id.

Proof.

apply/eqoP => _ /posnumP[e].
have /bigO_exP [_ /posnumP[k]] := bigOP [bigO of [O_ 0 id of g]].
move=> /nbhs_ballP [_ /posnumP[d] hd].
have ekgt0 : e%:num / k%:num > 0 by [].
have /(_ _ ekgt0) := littleoP [littleo of [o_ 0 id of f]].
apply: filter_app; near=> x => leoxekx; apply: le_trans (hd _ _) _; last first.
by rewrite -ler_pdivlMl // mulrA [_^-1 * _]mulrC.
by rewrite -ball_normE /= distrC subr0 (le_lt_trans leoxekx)// -ltr_pdivlMl //.
Unshelve. all: by end_near. Qed.

End DifferentialR3.

Section DifferentialR3_numFieldType.
Variable : numFieldType.

Lemma ( : normedModType R) ( : {linear V -> W}) :
(f : V -> W) =o_ 0 id -> f = cst 0 :> (V -> W).

Proof.

move/eqoP => oid.
rewrite funeqE => x; apply/eqP; have [|xn0] := real_le0P (normr_real x).
by rewrite normr_le0 => /eqP ->; rewrite linear0.
rewrite -normr_le0 -(mul0r `|x|) -ler_pdivrMr //.
apply/ler_gtP => _ /posnumP[e]; rewrite ler_pdivrMr //.
have /oid /nbhs_ballP [_ /posnumP[d] dfe] := [elaborate gt0 e].
set k := ((d%:num / 2) / (PosNum xn0)%:num)^-1.
rewrite -{1}(@scalerKV _ _ k _ x) /k // linearZZ normrZ.
rewrite -ler_pdivlMl; first by rewrite gtr0_norm.
rewrite mulrCA (@le_trans _ _ (e%:num * `|k^-1 *: x|)) //; last first.
by rewrite ler_pM // normrZ normfV.
apply: dfe; rewrite -ball_normE /= sub0r normrN normrZ.
rewrite invrK -ltr_pdivlMr // ger0_norm // ltr_pdivrMr //.
by rewrite divfK ?lt0r_neq0// [ltRHS]splitr ltrDl.
Qed.

Lemma ( : normedModType R) ( : V -> W)
  ( : {linear V -> W}) :
  continuous df -> f \o shift x = cst (f x) + df +o_ 0 id ->
  'd f x = df :> (V -> W).

Proof.

move=> dfc dxf; apply/subr0_eq; rewrite -[LHS]/(_ \- _).
apply/littleo_linear0/eqoP/eq_some_oP => /=; rewrite funeqE => y /=.
have hdf h : (f \o shift x = cst (f x) + h +o_ 0 id) ->
    h = f \o shift x - cst (f x) +o_ 0 id.
  move=> hdf; apply: eqaddoE.
  rewrite hdf addrAC -!addrA addrC !addrA subrK.
  rewrite -[LHS]addr0 -addrA; congr (_ + _).
  by apply/eqP; rewrite eq_sym addrC addr_eq0 oppo.
rewrite (hdf _ dxf).
suff /diff_locally /hdf -> : differentiable f x.
  by rewrite [_ - _ + _]addrC addrKA oppox addox.
apply/diffP => /=.
apply: (@getPex _ (fun ( : {linear V -> W}) => continuous df /\
  forall , f y = f (lim (nbhs x)) + df (y - lim (nbhs x))
                  +o_( \near x) (y - lim (nbhs x)))).
exists df; split=> //; apply: eqaddoEx => z.
rewrite (hdf _ dxf) !addrA lim_id // /(_ \o _) /= subrK [f _ + _]addrC addrK.
rewrite -addrA -[LHS]addr0; congr (_ + _).
apply/eqP; rewrite eq_sym addrC addr_eq0 oppox; apply/eqP.
rewrite [in LHS]littleo_center0 (comp_centerK x id).
by rewrite -[- _ in RHS](comp_centerK x).
Qed.

Lemma ( : normedModType R) : ('d (cst a) x : V -> W) = 0.

Proof.

by apply/diff_unique; have [] := dcst a x. Qed.

Variables ( : normedModType R).

Lemma ( : normedModType R) ( : W') ( : V) :
differentiable (cst a) x.

Proof.

by apply/diff_locallyP; rewrite diff_cst; have := dcst a x. Qed.

Global Instance ( : W) ( : V) : is_diff x (cst a) 0.

Proof.

exact: DiffDef (differentiable_cst _ _) (diff_cst _ _). Qed.

Lemma ( : V -> W) :
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 ( : V -> W) :
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 ( : V -> W) :
is_diff x f df -> is_diff x g dg -> is_diff x (f + g) (df + dg).

Proof.

move=> dfx dgx; apply: DiffDef; first exact: differentiableD.
by rewrite diffD; last (congr (_ + _); apply: diff_val).
Qed.

Lemma ( : 'I_n -> V -> W) ( : V) :
(forall , differentiable (f i) x) -> differentiable (\sum_( < n) f i) x.

Proof.

by elim/big_ind : _ => // ? ? g h ?; apply: differentiableD; [exact:g|exact:h].
Qed.

Lemma ( : V -> W) :
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 ( : V -> W) :
differentiable f x -> differentiable (- f) x.

Proof.

by move=> df; apply/diff_locallyP; rewrite diffN //; have := dopp df.
Qed.

Global Instance ( : V -> W) :
is_diff x f df -> is_diff x (- f) (- df).

Proof.

move=> dfx; apply: DiffDef; first exact: differentiableN.
by rewrite diffN // diff_val.
Qed.

Global Instance ( : V -> W) :
is_diff x f df -> is_diff x g dg -> is_diff x (f - g) (df - dg).

Proof.

by move=> dfx dgx; apply: is_diff_eq. Qed.

Lemma ( : V -> W) :
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 [LHS]diff_val.
Qed.

Lemma ( : V -> W) :
differentiable f x -> differentiable g x -> differentiable (f \- g) x.

Proof.

by move=> /differentiableP df /differentiableP dg. Qed.

Lemma ( : V -> W) :
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 ( : V -> W) :
differentiable f x -> differentiable (k *: f) x.

Proof.

by move=> df; apply/diff_locallyP; rewrite diffZ //; have := dscale k df.
Qed.

Global Instance ( : V -> W) :
is_diff x f df -> is_diff x (k *: f) (k *: df).

Proof.

move=> dfx; apply: DiffDef; first exact: differentiableZ.
by rewrite diffZ // diff_val.
Qed.

Lemma ( : V -> R) ( : W) : differentiable k x ->
'd (fun => k z *: f) x = (fun => 'd k x z *: f) :> (_ -> _).

Proof.

move=> df; set g := RHS; have glin : linear g.
by move=> a u v; rewrite /g linearP /= scalerDl -scalerA.
pose glM := GRing.isLinear.Build _ _ _ _ _ glin.
pose gL : {linear _ -> _} := HB.pack g glM.
by apply: (@diff_unique _ _ _ gL); have [] := dscalel f df.
Qed.

Lemma ( : V -> R) ( : W) :
differentiable k x -> differentiable (fun => k z *: f) x.

Proof.

by move=> df; apply/diff_locallyP; rewrite diffZl //; have [] := dscalel f df.
Qed.

Lemma ( : normedModType R) ( : {linear V' -> W'}) :
continuous f -> 'd f x = f :> (V' -> W').

Proof.

by move=> fcont; apply/diff_unique => //; apply: dlin. Qed.

Lemma ( : normedModType R) ( : {linear V' -> W'})
: continuous f -> differentiable f x.

Proof.

by move=> fcont; apply/diff_locallyP; rewrite diff_lin //; have := dlin x fcont.
Qed.

Global Instance ( : V) : is_diff x id id.

Proof.

apply: DiffDef.
by apply: (@linear_differentiable _ _ idfun) => ? //.
by rewrite (@diff_lin _ _ idfun) // => ? //.
Qed.

Global Instance ( : R) ( : V) : is_diff x ( *:%R k) ( *:%R k).

Proof.

apply: DiffDef; first exact/linear_differentiable/scaler_continuous.
by rewrite diff_lin //; apply: scaler_continuous.
Qed.

Global Instance ( : R) ( : V) :
is_diff k ( *:%R ^~ x) ( *:%R ^~ x).

Proof.

have sx_lin : linear ( *:%R ^~ x : R -> _).
by move=> u y z; rewrite scalerDl scalerA.
pose sxlM := GRing.isLinear.Build _ _ _ _ _ sx_lin.
pose sxL : {linear _ -> _} := HB.pack ( *:%R ^~ x) sxlM.
have -> : *:%R ^~ x = sxL by rewrite funeqE.
apply: DiffDef; first exact/linear_differentiable/scalel_continuous.
by rewrite diff_lin //; apply: scalel_continuous.
Qed.

Lemma ( : 'M[R]_(m, n)) :
differentiable (fun : 'M[R]_(m, n) => N i j : R ) M.

Proof.

have @f : {linear 'M[R]_(m, n) -> R}.
by exists (fun : 'M[R]_(_, _) => N i j); do 2![eexists]; do ?[constructor];
rewrite ?mxE// => ? *; rewrite ?mxE//; move=> ?; rewrite !mxE.
rewrite (_ : (fun _ => _) = f) //; exact/linear_differentiable/coord_continuous.
Qed.

Lemma ( : normedModType R) ( : {linear V' -> W'}) :
continuous f -> exists2 , k > 0 & forall , `|f x| <= k * `|x|.

Proof.

move=> /(_ 0); rewrite /continuous_at linear0 => /(_ _ (nbhsx_ballx _ _ ltr01)).
move=> /nbhs_ballP [_ /posnumP[e] he]; exists (2 / e%:num) => // x.
have [|xn0] := real_le0P (normr_real x).
  by rewrite normr_le0 => /eqP->; rewrite linear0 !normr0 mulr0.
set k := 2 / e%:num * (PosNum xn0)%:num.
have kn0 : k != 0 by rewrite /k.
have abskgt0 : `|k| > 0 by rewrite normr_gt0.
rewrite -[x in leLHS](scalerKV kn0) linearZZ normrZ -ler_pdivlMl //.
suff /he : ball 0 e%:num (k^-1 *: x).
  rewrite -ball_normE /= distrC subr0 => /ltW /le_trans; apply.
  by rewrite ger0_norm /k // mulVf.
rewrite -ball_normE /= distrC subr0 normrZ.
rewrite normfV ger0_norm /k // invfM/= divfK ?gt_eqF//.
by rewrite invf_div gtr_pMr// invf_lt1// ltr1n.
Qed.

Lemma ( : normedModType R) ( : {linear V' -> W'}) :
continuous f -> (f : V' -> W') =O_ 0 id.

Proof.

move=> /linear_lipschitz [k kgt0 flip]; apply/eqO_exP; exists k => //.
exact: filterE.
Qed.

Lemma ( : normedModType R) ( : filter_on V') ( : V' -> W') :
differentiable f x -> ('d f x : V' -> W') =O_ 0 id.

Proof.

by move=> /diff_continuous /linear_eqO; apply. Qed.

Lemma ( : normedModType R) ( : U -> V') ( : V' -> W') :
[O_ 0 id of g] ([o_ 0 id of f] x) =o_( \near 0) x.

Proof.

by rewrite -[LHS]/((_ \o _) x) compOo_eqo. Qed.

Fact ( : normedModType R) ( : U -> V') ( : V' -> W') :
  differentiable f x -> differentiable g (f x) ->
  continuous ('d g (f x) \o 'd f x) /\ forall ,
  g (f (y + x)) = g (f x) + ('d g (f x) \o 'd f x) y +o_( \near 0) y.

Proof.

move=> df dg; split; first by move=> ?; apply: continuous_comp.
apply: eqaddoEx => y; rewrite diff_locallyx// -addrA diff_locallyxC// linearD.
rewrite addrA -[LHS]addrA; congr (_ + _ + _).
rewrite diff_eqO // ['d f x : _ -> _]diff_eqO //.
by rewrite {2}eqoO addOx compOo_eqox compoO_eqox addox.
Qed.

Lemma ( : normedModType R) ( : U -> V') ( : V' -> W') :
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 ( : normedModType R) ( : U -> V')
( : V' -> W') : 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 ( : normedModType R) ( : U -> V')
( : V' -> W') : is_diff x f df -> is_diff (f x) g dg ->
is_diff x (g \o f) (dg \o df) | 99.

Proof.

move=> dfx dgfx; apply: DiffDef; first exact: differentiable_comp.
by rewrite diff_comp // !diff_val.
Qed.

Lemma { } :
differentiable (rsubmx : 'M[R]_(m, n1 + n2) -> 'M[R]_(m, n2)) v.

Proof.

exact/linear_differentiable/continuous_rsubmx. Qed.

Lemma { } :
differentiable (lsubmx : 'M[R]_(m, n1 + n2) -> 'M[R]_(m, n1)) v.

Proof.

exact/linear_differentiable/continuous_lsubmx. Qed.

Lemma ( : normedModType R)
( : {bilinear U -> V' -> W'}) : continuous (fun => f p.1 p.2) ->
exists2 , k > 0 & forall , `|f u v| <= k * `|u| * `|v|.

Proof.

move=> /(_ 0); rewrite /continuous_at linear0r => /(_ _ (nbhsx_ballx _ _ ltr01)).
move=> /nbhs_ballP [_ /posnumP[e] he]; exists ((2 / e%:num) ^+2) => // u v.
have [|un0] := real_le0P (normr_real u).
  by rewrite normr_le0 => /eqP->; rewrite linear0l !normr0 mulr0 mul0r.
have [|vn0] := real_le0P (normr_real v).
  by rewrite normr_le0 => /eqP->; rewrite linear0r !normr0 mulr0.
rewrite -[`|u|]/((PosNum un0)%:num) -[`|v|]/((PosNum vn0)%:num).
set ku := 2 / e%:num * (PosNum un0)%:num.
set kv := 2 / e%:num * (PosNum vn0)%:num.
rewrite -[X in f X](@scalerKV _ _ ku) /ku // linearZl_LR normrZ.
rewrite gtr0_norm // -ler_pdivlMl //.
rewrite -[X in f _ X](@scalerKV _ _ kv) /kv // linearZr_LR normrZ.
rewrite gtr0_norm // -ler_pdivlMl //.
suff /he : ball 0 e%:num (ku^-1 *: u, kv^-1 *: v).
  rewrite -ball_normE /= distrC subr0 => /ltW /le_trans; apply.
  rewrite ler_pdivlMl 1?pmulr_lgt0// mulr1 ler_pdivlMl 1?pmulr_lgt0//.
  by rewrite mulrA [ku * _]mulrAC expr2.
rewrite -ball_normE /= distrC subr0.
have -> : (ku^-1 *: u, kv^-1 *: v) =
    (e%:num / 2) *: ((PosNum un0)%:num ^-1 *: u, (PosNum vn0)%:num ^-1 *: v).
  by rewrite invfM [kv ^-1]invfM invf_div -[_ *: u]scalerA -[_ *: v]scalerA.
rewrite normrZ ger0_norm // -mulrA gtr_pMr // ltr_pdivrMl // mulr1.
by rewrite prod_normE/= !normrZ !normfV !normr_id !mulVf ?gt_eqF// maxxx ltr1n.
Qed.

Lemma ( : normedModType R) ( : {bilinear U -> V' -> W'}) :
continuous (fun => f p.1 p.2) -> (fun => f p.1 p.2) =o_ (0 : U * V') id.

Proof.

move=> fc; have [_ /posnumP[k] fschwarz] := bilinear_schwarz fc.
apply/eqoP=> _ /posnumP[e]; near=> x; rewrite (le_trans (fschwarz _ _))//.
rewrite ler_pM ?pmulr_rge0 //; last by rewrite num_le_max /= lexx orbT.
rewrite -ler_pdivlMl //.
suff : `|x| <= k%:num ^-1 * e%:num.
by apply: le_trans; rewrite num_le_max /= lexx.
near: x; rewrite !near_simpl; apply/nbhs_le_nbhs_norm.
by exists (k%:num ^-1 * e%:num) => //= ? /=; rewrite /= distrC subr0 => /ltW.
Unshelve. all: by end_near. Qed.

Fact ( : normedModType R) ( : {bilinear U -> V' -> W'}) :
  continuous (fun => f p.1 p.2) ->
  continuous (fun => (f p.1 q.2 + f q.1 p.2)) /\
  (fun => f q.1 q.2) \o shift p = cst (f p.1 p.2) +
    (fun => f p.1 q.2 + f q.1 p.2) +o_ (0 : U * V') id.

Proof.

move=> fc; split=> [q|].
  by apply: (@continuousD _ _ _ (fun => f p.1 q.2) (fun => 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 linearDr !linearDl -addrA addrC addrA [_ + f p.1 p.2]addrC.
by congr (_ + _); rewrite -[LHS]/((fun => f p.1 p.2) q) bilinear_eqo.
Qed.

Lemma ( : normedModType R) ( : {bilinear U -> V' -> W'}) :
continuous (fun => f p.1 p.2) -> 'd (fun => f q.1 q.2) p =
(fun => f p.1 q.2 + f q.1 p.2) :> (U * V' -> W').

Proof.

pose d := f p.1 q.2 + f q.1 p.2.
move=> fc; have lind : linear d.
by move=> ? ? ?; rewrite /d linearPr linearPl scalerDr addrACA.
pose dlM := GRing.isLinear.Build _ _ _ _ _ lind.
pose dL : {linear _ -> _} := HB.pack d dlM.
rewrite -/d -[d]/(dL : _ -> _).
by apply/diff_unique; have [] := dbilin p fc.
Qed.

Lemma ( : normedModType R)
( : {bilinear U -> V' -> W'}) :
continuous (fun => f p.1 p.2) -> differentiable (fun => f p.1 p.2) p.

Proof.

by move=> fc; apply/diff_locallyP; rewrite diff_bilin //; apply: dbilin p fc.
Qed.

Lemma :
  bilinear_for
    (GRing.Scale.Law.clone _ _ *:%R _) (GRing.Scale.Law.clone _ _ *:%R _)
    (@GRing.mul R).

Proof.

split=> [u'|u] a x y /=.
- by rewrite mulrDl scalerAl.
- by rewrite mulrDr scalerAr.
Qed.

..Build R R R R _ _ (@GRing.mul R)
mulr_is_bilinear.

Global Instance ( : R * R) :
is_diff p (fun q => q.1 * q.2) (fun => p.1 * q.2 + q.1 * p.2).

Proof.

apply: DiffDef; last by rewrite diff_bilin // => ?; apply: mul_continuous.
by apply: differentiable_bilin =>?; apply: mul_continuous.
Qed.

Lemma ( : normedModType R) ( : filter_on U)
( : U -> V') ( : U -> W') :
(fun => ([o_F id of f] t, [o_F id of g] t)) =o_F id.

Proof.

apply/eqoP => _/posnumP[e]; near=> x; rewrite num_ge_max /=.
by apply/andP; split; near: x; apply: littleoP.
Unshelve. all: by end_near. Qed.

Fact ( : normedModType R) ( : U -> V') ( : U -> W') :
  differentiable f x -> differentiable g x ->
  continuous (fun => ('d f x y, 'd g x y)) /\
  (fun => (f y, g y)) \o shift x = cst (f x, g x) +
  (fun => ('d f x y, 'd g x y)) +o_ 0 id.

Proof.

move=> df dg; split=> [?|]; first by apply: cvg_pair; apply: diff_continuous.
apply/eqaddoE; rewrite funeqE => y /=.
rewrite ![_ (_ + x)]diff_locallyx//.
(* fixme *)
have -> : forall , (f x + 'd f x y + [o_ 0 id of h] y,
  g x + 'd g x y + [o_ 0 id of e] y) =
  (f x, g x) + ('d f x y, 'd g x y) +
  ([o_ 0 id of h] y, [o_ 0id of e] y) by [].
by congr (_ + _); rewrite -[LHS]/((fun => (_ y, _ y)) y) eqo_pair.
Qed.

Lemma ( : normedModType R) ( : U -> V') ( : U -> W') :
differentiable f x -> differentiable g x -> 'd (fun => (f y, g y)) x =
(fun => ('d f x y, 'd g x y)) :> (U -> V' * W').

Proof.

move=> df dg.
pose d := ('d f x y, 'd g x y).
have lin_pair : linear d by move=> ???; rewrite /d !linearPZ.
pose pairlM := GRing.isLinear.Build _ _ _ _ _ lin_pair.
pose pairL : {linear _ -> _} := HB.pack d pairlM.
rewrite -/d -[d]/(pairL : _ -> _).
by apply: diff_unique; have [] := dpair df dg.
Qed.

Lemma ( : normedModType R) ( : U -> V')
( : U -> W') : differentiable f x -> differentiable g x ->
differentiable (fun => (f y, g y)) x.

Proof.

by move=> df dg; apply/diff_locallyP; rewrite diff_pair //; apply: dpair.
Qed.

Global Instance ( : normedModType R) ( : U -> V')
( : U -> W') : is_diff x f df -> is_diff x g dg ->
is_diff x (fun y => (f y, g y)) (fun => (df y, dg y)).

Proof.

move=> dfx dgx; apply: DiffDef; first exact: differentiable_pair.
by rewrite diff_pair // !diff_val.
Qed.

Global Instance ( : V -> R) :
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.1 * p.2) \o (fun => (f y, g y)) by [].
apply: is_diff_eq.
by rewrite funeqE => ?; rewrite /= [_ * g _]mulrC.
Qed.

Lemma ( : V -> R) :
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 [LHS]diff_val.
Qed.

Lemma ( : V -> R) :
differentiable f x -> differentiable g x -> differentiable (f * g) x.

Proof.

by move=> /differentiableP df /differentiableP dg. Qed.

Fact ( : R) :
  x != 0 -> continuous (fun : R => - x ^- 2 *: h) /\
  (fun => x^-1)%R \o shift x = cst (x^-1)%R +
  (fun : R => - x ^- 2 *: h) +o_ 0 id.

Proof.

move=> xn0; split; first by move=> ?; exact: continuousZl_tmp.
apply/eqaddoP => _ /posnumP[e]; near=> h.
have hDx_neq0 : h + x != 0.
  near: h; rewrite !nbhs_simpl; apply/nbhs_normP.
  exists `|x|; first by rewrite /= normr_gt0.
  move=> h /=; rewrite /= distrC subr0 -subr_gt0 => lthx.
  rewrite -(normr_gt0 (h + x)) addrC -[h]opprK.
  apply: lt_le_trans (ler_dist_dist _ _).
  by rewrite ger0_norm normrN //; apply: ltW.
rewrite !fctE/= opprD scaleNr opprK.
suff: `|h * h| / `|h + x| / `|x * x| <= e%:num * `|h|.
  rewrite -2!normf_div -mulrA -invfM; congr (`|_| <= _).
  apply/(canLR (mulfK _)); rewrite ?mulf_neq0//.
  rewrite mulrDl mulKf// [(_ + _) * _]mulrC mulrDr mulrN.
  rewrite -mulrA mulfK// -mulrA mulVKf ?mulf_neq0//.
  by rewrite [- _ + _]addrC !mulrDl [x * h]mulrC addrKA subrKC.
rewrite ler_pdivrMr ?normr_gt0 ?mulf_neq0 // mulrAC ler_pdivrMr ?normr_gt0 //.
have : `|h * h| <= `|x / 2| * (e%:num * `|x * x| * `|h|).
  rewrite !mulrA; near: h; exists (`|x / 2| * e%:num * `|x * x|).
    by rewrite /= !pmulr_rgt0 // normr_gt0 mulf_neq0.
  by move=> h /ltW; rewrite distrC subr0 [`|h * _|]normrM => /ler_pM; apply.
move=> /le_trans -> //; rewrite [leLHS]mulrC ler_pM ?mulr_ge0 //.
near: h; exists (`|x| / 2); first by rewrite /= divr_gt0 ?normr_gt0.
move=> h; rewrite /= distrC subr0 => lthhx; rewrite addrC -[h]opprK.
apply: le_trans (@ler_dist_dist _ R _ _).
rewrite normrN [leRHS]ger0_norm.
  rewrite subr_ge0; apply: ltW; apply: lt_le_trans lthhx _.
  by rewrite ler_pdivrMr // -{1}(mulr1 `|x|) ler_pM // ler1n.
rewrite lerBrDr -lerBrDl (splitr `|x|).
rewrite normf_div (@ger0_norm _ 2) // addrK; apply/ltW.
Unshelve. all: by end_near. Qed.

Lemma ( : R) : x != 0 ->
'd GRing.inv x = (fun : R => - x ^- 2 *: h) :> (R -> R).

Proof.

move=> xn0; have -> : (fun : R => - x ^- 2 *: h) = ( *:%R (- x ^- 2)) by [].
by apply: diff_unique; have [] := dinv xn0.
Qed.

Lemma ( : R) : x != 0 ->
differentiable (GRing.inv : R -> R) x.

Proof.

by move=> xn0; apply/diff_locallyP; rewrite diff_Rinv //; apply: dinv.
Qed.

Lemma ( : V -> R) : differentiable f x -> f x != 0 ->
'd (fun => (f y)^-1) x = - (f x) ^- 2 \*: 'd f x :> (V -> R).

Proof.

move=> df fxn0.
by rewrite [LHS](diff_comp df (differentiable_Rinv fxn0)) diff_Rinv.
Qed.

Lemma ( : V -> R) :
differentiable f x -> f x != 0 -> differentiable (fun => (f y)^-1) x.

Proof.

by move=> df fxn0; apply: differentiable_comp _ (differentiable_Rinv fxn0).
Qed.

Global Instance ( : V -> R) :
is_diff x f df -> is_diff x (f ^+ n.+1) (n.+1%:R * f x ^+ n *: df).

Proof.

move=> dfx; elim: n => [|n ihn]; first by rewrite expr1 expr0 mulr1 scale1r.
rewrite exprS; apply: is_diff_eq.
rewrite scalerA mulrCA -exprS -scalerDl.
by rewrite [in LHS]mulr_natl exprfctE -mulrSr mulr_natl.
Qed.

Lemma ( : V -> R) :
differentiable f x -> differentiable (f ^+ n.+1) x.

Proof.

by move=> /differentiableP. Qed.

Lemma ( : V -> R) :
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 ( : numFieldType) ( : normedModType R).
Implicit Types f : R -> U.

Let : derivable f x 1 ->
f \o shift x = cst (f x) + ( *:%R^~ (f^`() x)) +o_ 0 id.

Proof.

move=> df; apply/eqaddoE; have /derivable_nbhsP := df.
have -> : (fun => (f \o shift x) h%:A) = f \o shift x.
by rewrite funeqE=> ?; rewrite [_%:A]mulr1.
by rewrite derive1E =>->.
Qed.

Lemma : derivable f x 1 -> 'd f x = ( *:%R^~ (f^`() x)) :> (R -> U).

Proof.

pose d ( : R) := h *: (f^`() x)%classic.
move=> df; have lin_scal : linear d by move=> ? ? ?; rewrite /d scalerDl scalerA.
pose scallM := GRing.isLinear.Build _ _ _ _ _ lin_scal.
pose scalL : {linear _ -> _} := HB.pack d scallM.
rewrite -/d -[d]/(scalL : _ -> _).
by apply: diff_unique; [apply: scalel_continuous|apply: der1].
Qed.

Lemma :
differentiable f x -> 'd f x = (fun => h *: f^`()%classic x) :> (R -> U).

Proof.

pose d ( : R) := h *: 'd f x 1.
move=> df; have lin_scal : linear d by move=> ? ? ?; rewrite /d scalerDl scalerA.
pose scallM := GRing.isLinear.Build _ _ _ _ _ lin_scal.
pose scalL : {linear _ -> _} := HB.pack d scallM.
have -> : (fun => h *: f^`()%classic x) = scalL by rewrite derive1E'.
apply: diff_unique; first exact: scalel_continuous.
apply/eqaddoE; have /diff_locally -> := df; congr (_ + _ + _).
by rewrite funeqE => h /=; rewrite -{1}[h]mulr1 linearZ.
Qed.

Lemma : derivable f x 1 <-> differentiable f x.

Proof.

split=> dfx.
  by apply/diff_locallyP; rewrite deriv1E //; split;
    [apply: scalel_continuous|apply: der1].
apply/derivable_nbhsP/eqaddoE.
have -> : (fun => (f \o shift x) h%:A) = f \o shift x.
  by rewrite funeqE=> ?; rewrite [_%:A]mulr1.
by have /diff_locally := dfx; rewrite diff1E // derive1E =>->.
Qed.

Lemma ( : interval R) :
{in i, forall , 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 ( : numFieldType) ( : normedModType R).
Implicit Types f : V -> W.

Lemma :
derivable f x v <-> derivable (fun : R => f (h *: v + x)) 0 1.

Proof.

rewrite /derivable; set g1 := fun => h^-1 *: _; set g2 := fun => h^-1 *: _.
suff -> : g1 = g2 by [].
by rewrite funeqE /g1 /g2 => h /=; rewrite addr0 scale0r add0r [_%:A]mulr1.
Qed.

Lemma : derivable f x v -> is_derive x v f ('D_v f x).

Proof.

by move=> df; apply: DeriveDef. Qed.

Lemma : differentiable f a -> derivable f a v.

Proof.

move=> dfa; apply/derivable1P/derivable1_diffP.
by apply: differentiable_comp; rewrite ?scale0r ?add0r.
Qed.

Global Instance ( : W) ( : V) : is_derive x v (cst a) 0.

Proof.

apply: DeriveDef; last by rewrite deriveE // diff_val.
exact/diff_derivable.
Qed.

Lemma ( : W) ( : V) : derivable (cst w) x v.

Proof.

exact/diff_derivable. Qed.

Lemma ( : V) ( : W) :
is_derive x v f f' -> f' = df -> is_derive x v f df.

Proof.

by move=> ? <-. Qed.

End DeriveVW.
Arguments derivable_cst {R V W}.

Section Derive_lemmasVW.
Variables ( : numFieldType) ( : normedModType R).
Implicit Types f g : V -> W.

Fact ( : V) : derivable f x v -> derivable g x v ->
(fun => h^-1 *: (((f + g) \o shift x) (h *: v) - (f + g) x)) @
0^' --> 'D_v f x + 'D_v g x.

Proof.

move=> df dg.
evar (fg : R -> W); rewrite [X in X @ _](_ : _ = fg) /=.
rewrite funeqE => h.
by rewrite !scalerDr scalerN scalerDr opprD addrACA -!scalerBr /fg.
exact: cvgD.
Qed.

Lemma ( : 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=> df dg; apply: cvg_lim (der_add df dg). Qed.

Lemma ( : V) :
derivable f x v -> derivable g x v -> derivable (f + g) x v.

Proof.

move=> df dg; apply/cvg_ex; exists (derive f x v + derive g x v).
exact: der_add.
Qed.

Global Instance ( : V) ( : W) :
is_derive x v f df -> is_derive x v g dg -> is_derive x v (f + g) (df + dg).

Proof.

move=> dfx dgx; apply: DeriveDef; first exact: derivableD.
by rewrite deriveD // !derive_val.
Qed.

Global Instance ( : 'I_n -> V -> W) ( : V)
( : 'I_n -> W) : (forall , is_derive x v (h i) (dh i)) ->
is_derive x v (\sum_( < n) h i) (\sum_( < n) dh i).

Proof.

by elim/big_ind2 : _ => // [|] *; [exact: is_derive_cst|exact: is_deriveD].
Qed.

Lemma ( : 'I_n -> V -> W) ( : V) :
(forall , derivable (h i) x v) -> derivable (\sum_( < n) h i) x v.

Proof.

move=> df; suff : forall , is_derive x v (h i) ('D_v (h i) x) by [].
by move=> ?; apply: derivableP.
Qed.

Lemma ( : 'I_n -> V -> W) ( : V) :
(forall , derivable (h i) x v) ->
'D_v (\sum_( < n) h i) x = \sum_( < n) 'D_v (h i) x.

Proof.

move=> df; suff dfx : forall , is_derive x v (h i) ('D_v (h i) x).
by rewrite derive_val.
by move=> ?; apply: derivableP.
Qed.

Fact ( : V) : derivable f x v ->
(fun => 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) /=.
by rewrite funeqE => h; rewrite !scalerDr !scalerN -opprD -scalerBr /g.
exact: cvgN.
Qed.

Lemma ( : V) : derivable f x v ->
'D_v (- f) x = - 'D_v f x.

Proof.

by move=> df; apply: cvg_lim (der_opp df). Qed.

Lemma ( : 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 ( : V) ( : W) :
is_derive x v f df -> is_derive x v (- f) (- df).

Proof.

move=> dfx; apply: DeriveDef; first exact: derivableN.
by rewrite deriveN // derive_val.
Qed.

Global Instance ( : V) ( : W) :
is_derive x v f df -> is_derive x v g dg -> is_derive x v (f - g) (df - dg).

Proof.

by move=> ??; apply: is_derive_eq. Qed.

Lemma ( : 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 ( : V) :
derivable f x v -> derivable g x v -> derivable (f - g) x v.

Proof.

by move=> /derivableP df /derivableP dg. Qed.

Fact ( : R) ( : V) : derivable f x v ->
(fun => h^-1 *: ((k \*: f \o shift x) (h *: v) - (k \*: f) x)) @
0^' --> k *: 'D_v f x.

Proof.

move=> df; evar (h : R -> W); rewrite [X in X @ _](_ : _ = h) /=.
rewrite funeqE => r.
by rewrite scalerBr !scalerA mulrC -!scalerA -!scalerBr /h.
exact: cvgZl_tmp.
Qed.

Lemma ( : R) ( : V) : derivable f x v ->
'D_v (k \*: f) x = k *: 'D_v f x.

Proof.

by move=> df; apply: cvg_lim (der_scal df). Qed.

Lemma ( : R) ( : 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 ( : R) ( : V) ( : W) :
is_derive x v f df -> is_derive x v (k \*: f) (k *: df).

Proof.

move=> dfx; apply: DeriveDef; first exact: derivableZ.
by rewrite deriveZ // derive_val.
Qed.

Lemma ( : W) ( : V) : 'D_v (cst k) x = 0.

Proof.

by rewrite derive_val. Qed.

End Derive_lemmasVW.

Section derive_id.
Variables ( : numFieldType) ( : normedModType R).

Lemma ( : V) : derivable id x v.

Proof.

exact/diff_derivable. Qed.

Global Instance ( : V) : is_derive x v id v.

Proof.

apply: (DeriveDef (@derivable_id _ _)).
rewrite deriveE// (@diff_lin _ _ _ idfun)//=.
by rewrite /continuous_at.
Qed.

Global Instance ( : V) : is_derive x v -%R (- v).

Proof.

exact: is_deriveN. Qed.

Lemma ( : V) : 'D_v id x = v.

Proof.

by have /derivableP := @derivable_id x v; rewrite derive_val. Qed.

End derive_id.

Lemma { : numFieldType} :
(fun => x.~ : R^o)^`()%classic = cst (-1).

Proof.

by apply/funext => x; rewrite derive1E deriveB// derive_id derive_cst sub0r.
Qed.

Section Derive_lemmasVR.
Context { : numFieldType} { : normedModType R}.
Implicit Types (f g : V -> R) (x v : V).

Fact :
  derivable f x v -> derivable g x v ->
  (fun => h^-1 *: (((f * g) \o shift x) (h *: v) - (f * g) x)) @
  0^' --> f x *: 'D_v g x + g x *: 'D_v f x.

Proof.

move=> df dg.
evar (fg : R -> R); rewrite [X in X @ _](_ : _ = fg) /=.
  rewrite funeqE => h.
  have -> : (f * g) (h *: v + x) - (f * g) x =
    f (h *: v + x) *: (g (h *: v + x) - g x) + g x *: (f (h *: v + x) - f x).
    by rewrite !scalerBr -addrA ![g x *: _]mulrC addKr.
  rewrite scalerDr scalerA mulrC -scalerA.
  by rewrite [_ *: (g x *: _)]scalerA mulrC -scalerA /fg.
apply: cvgD; last exact: cvgZl_tmp df.
apply: cvg_comp2 (@scale_continuous _ _ (_, _)) => /=; last exact: dg.
suff : {for 0, continuous (fun : R => f(h *: v + x))}.
  by move=> /continuous_withinNx; rewrite scale0r add0r.
exact/differentiable_continuous/derivable1_diffP/(derivable1P _ _ _).1.
Qed.

Lemma : 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.

by move=> df dg; apply: cvg_lim (der_mult df dg). Qed.

Lemma :
derivable f x v -> derivable g x v -> derivable (f * g) x v.

Proof.

move=> df dg; apply/cvg_ex; exists (f x *: 'D_v g x + g x *: 'D_v f x).
exact: der_mult.
Qed.

Lemma ( : R) :
derivable f x v -> 'D_v (r \o* f) x = r * 'D_v f x.

Proof.

move/deriveM => /(_ _ (derivable_cst _ _ _)) ->.
by rewrite derive_cst scaler0 add0r.
Qed.

Lemma ( : R) :
derivable f x v -> 'D_v (r \*o f) x = r * 'D_v f x.

Proof.

by move=> fxv; rewrite -deriveMr// mul_funC. Qed.

Global Instance ( : 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.

move=> dfx dgx; apply: DeriveDef; first exact: derivableM.
by rewrite deriveM // !derive_val.
Qed.

Global Instance ( : R) :
is_derive x v f df -> is_derive x v (f ^+ n) ((n%:R * f x ^+ n.-1) *: df).

Proof.

case: n => [fdf|n dfx].
by rewrite expr0 mul0r scale0r; exact: is_derive_cst.
elim: n => [|n ihn]; first by rewrite expr1 expr0 mulr1 scale1r.
rewrite exprS; apply: is_derive_eq.
rewrite scalerA -scalerDl mulrCA -[f x * _]exprS.
by rewrite [in LHS]mulr_natl exprfctE -mulrSr mulr_natl.
Qed.

Lemma : derivable f x v -> derivable (f ^+ n) x v.

Proof.

by case: n => [_|n /derivableP]; [rewrite expr0|]. Qed.

Lemma : derivable f x v ->
'D_v (f ^+ n) x = (n%:R * f x ^+ n.-1) *: 'D_v f x.

Proof.

by move=> /derivableP df; rewrite derive_val. Qed.

Fact : f x != 0 -> derivable f x v ->
(fun => h^-1 *: (((fun => (f y)^-1) \o shift x) (h *: v) - (f x)^-1)) @
0^' --> - (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^' [set | f (h *: v + x) != 0].
  apply: (fc [set | 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 => - ((f x)^-1 * (f (h *: v + x))^-1) *:
  (h^-1 *: (f (h *: v + x) - f x))) @ 0^' -->
  - (f x) ^- 2 *: 'D_v f x.
  by apply: cvgM => //; apply: cvgN; rewrite expr2 invfM; apply: cvgM => //;
     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 : f x != 0 -> derivable f x v ->
'D_v (fun => (f y)^-1) x = - (f x) ^- 2 *: 'D_v f x.

Proof.

by move=> fxn0 df; apply: cvg_lim (der_inv fxn0 df). Qed.

Lemma :
f x != 0 -> derivable f x v -> derivable (fun => (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 ( : R) :
f x != 0 -> is_derive x v f df ->
is_derive x v (fun => (f y)^-1) (- (f x) ^- 2 *: df).

Proof.

move=> fxNZ Df; apply: DeriveDef; first exact: derivableV.
by rewrite deriveV//; case: Df => _ ->.
Qed.

End Derive_lemmasVR.

#[global] Hint Extern 0 (is_derive _ _ (fun _ => (_ _)^-1) _) =>
(apply: is_deriveV; first by []) : typeclass_instances.

Lemma { : numFieldType} ( : R) :
'D_v (shift k : R -> R) = cst v.

Proof.

by apply/funext => x/=; rewrite deriveD// derive_id derive_cst addr0.
Qed.

Lemma { : numFieldType} ( : R) :
is_derive x v (shift k) v.

Proof.

by apply: DeriveDef => //; rewrite derive_val addr0. Qed.

Lemma { : numFieldType} ( : normedModType R) ( : V) :
(cst k)^`() t = 0.

Proof.

by rewrite derive1E derive_cst. Qed.

Lemma { : numFieldType} ( : R -> R) ( : R) :
derivable f x 1 ->
(fun => f x * r)^`()%classic x = f^`()%classic x * r.

Proof.

by move=> ?; rewrite derive1E deriveMr ?derive1E 1?mulrC. Qed.

Lemma { : numFieldType} ( : R -> R) ( : R) :
derivable f x 1 ->
(fun => r * f x)^`()%classic x = r * f^`()%classic x :> R.

Proof.

by move=> ?; rewrite derive1E deriveMl ?derive1E. Qed.

Lemma { : numFieldType} ( : R) :
derivable (@GRing.exp R ^~ n) x v.

Proof.

elim: n => [/=|n ih]; first by rewrite (_ : _ ^~ _ = 1).
rewrite (_ : _ ^~ _ = (fun => x * x ^+ n)).
by apply/funext => y; rewrite exprS.
by apply: derivableM; first exact: derivable_id.
Qed.

Lemma { : numFieldType} :
'D_v (@GRing.exp R ^~ n) x = n%:R *: x ^+ n.-1 *: v.

Proof.

have /= := @deriveX R R id n x v (@derivable_id _ _ _ _).
by rewrite fctE => ->; rewrite derive_id.
Qed.

Lemma { : numFieldType} :
(@GRing.exp R ^~ n)^`() x = n%:R *: x ^+ n.-1.

Proof.

by rewrite derive1E exp_derive [LHS]mulr1. Qed.

Lemma ( : topologicalType) ( : realType) ( : T -> R)
    ( : set T) :
  A !=set0 -> compact A -> {within A, continuous f} ->
  exists2 , c \in A & forall , t \in A -> f t <= f c.

Proof.

move=> A0 cA cf.
have sup_fA : has_sup (f @` A).
  by apply/compact_has_sup; [exact: image_nonempty A0|exact/continuous_compact].
have [|imf_ltsup] := pselect (exists2 , c \in A & f c = sup (f @` A)).
  move=> [c cinA fcsupfA]; exists c => // t tA; rewrite fcsupfA.
  by apply/sup_upper_bound => //; exact/imageP/set_mem.
have {}AfsupfA t : t \in A -> f t < sup (f @` A).
  move=> tA; have [//|supfAft] := ltrP (f t) (sup (f @` A)).
  rewrite falseE; apply: imf_ltsup; exists t => //.
  apply/eqP; rewrite eq_le supfAft andbT sup_upper_bound//.
  exact/imageP/set_mem.
pose g : R := (sup (f @` A) - f t)^-1.
have invf_continuous : {within A, continuous g}.
  rewrite continuous_subspace_in => t tA; apply: cvgV => //=.
    by rewrite subr_eq0 gt_eqF// AfsupfA//; rewrite inE in tA.
  by apply: cvgD; [exact: cst_continuous | apply: cvgN; exact: cf].
have /ex_strict_bound_gt0[k k_gt0 /= imVfltk] : bounded_set (g @` A).
  exact/compact_bounded/continuous_compact.
have [_ [t tA <-]] : exists2 , (f @` A) y & sup (f @` A) - k^-1 < y.
  by apply: sup_adherent => //; rewrite invr_gt0.
rewrite ltrBlDr -ltrBlDl.
suff : sup (f @` A) - f t > k^-1 by move=> /ltW; rewrite leNgt => /negbTE ->.
rewrite invf_plt ?posrE ?subr_gt0 ?AfsupfA//; first exact/mem_set.
by rewrite (le_lt_trans (ler_norm _))// imVfltk//; exact: imageP.
Qed.

Lemma ( : topologicalType) ( : realType) ( : T -> R)
    ( : set T) :
  A !=set0 -> compact A -> {within A, continuous f} ->
  exists2 , c \in A & forall , t \in A -> f c <= f t.

Proof.

move=> A0 cA cf.
have /(compact_EVT_max A0 cA)[c cinA fcmin] : {within A, continuous (- f)}.
by move=> ?; apply: continuousN => ?; exact: cf.
by exists c => // t tA; rewrite -lerN2 fcmin.
Qed.

Lemma ( : realType) ( : R -> R) ( : R) :
a <= b -> {within `[a, b], continuous f} ->
exists2 , c \in `[a, b]%R & forall , t \in `[a, b]%R -> f t <= f c.

Proof.

move=> ab cf.
have ab0 : `[a, b] !=set0 by exists a => /=; rewrite in_itv/= lexx.
have [/= c cab maxf] := compact_EVT_max ab0 (@segment_compact _ a b) cf.
by rewrite inE in cab; exists c => //= t tab; apply: maxf; rewrite inE.
Qed.

Lemma ( : realType) ( : R -> R) ( : R) :
a <= b -> {within `[a, b], continuous f} ->
exists2 , c \in `[a, b]%R & forall , t \in `[a, b]%R -> f c <= f t.

Proof.

move=> ab cf.
have ab0 : `[a, b] !=set0 by exists a => /=; rewrite in_itv/= lexx.
have [/= c cab minf] := compact_EVT_min ab0 (@segment_compact _ a b) cf.
by rewrite inE in cab; exists c => //= t tab; apply: minf; rewrite inE.
Qed.

Lemma ( : realType) ( : 'rV[R]_n -> R) ( : set 'rV[R]_n) :
A !=set0 -> compact A -> {within A, continuous f} ->
exists2 , c \in A & forall , t \in A -> f t <= f c.

Proof.

by move=> A0 cA cf; exact: compact_EVT_max. Qed.

Lemma ( : realType) ( : 'rV[R]_n -> R) ( : set 'rV[R]_n) :
A !=set0 -> compact A -> {within A, continuous f} ->
exists2 , c \in A & forall , t \in A -> f c <= f t.

Proof.

by move=> A0 cA cf; exact: compact_EVT_min. Qed.

Lemma ( : numFieldType) ( : normedModType R) ( : R -> V) :
cvg (f @ x^') -> lim (f @ x^') = lim (f @ at_right x).

Proof.

move=> cvfx; apply/esym/(@cvg_lim _ _ _ (at_right _)) => //.
move=> A /cvfx /nbhs_ballP [_ /posnumP[e] xe_A].
by exists e%:num => //= y xe_y /gt_eqF/negbT/xe_A; exact.
Qed.

Arguments cvg_at_rightE {R V} f x.

Lemma ( : numFieldType) ( : normedModType R) ( : R -> V) :
cvg (f @ x^') -> lim (f @ x^') = lim (f @ at_left x).

Proof.

move=> cvfx; apply/esym/(@cvg_lim _ _ _ (at_left _)) => //.
move=> A /cvfx /nbhs_ballP [_ /posnumP[e] xe_A].
by exists e%:num => //= y xe_y /lt_eqF/negbT/xe_A; exact.
Qed.

Arguments cvg_at_leftE {R V} f x.

Lemma ( : realFieldType) ( : R -> R) ( : R) :
a <= b -> (forall , t \in `]a, b[%R -> derivable f t 1) -> c \in `]a, b[%R ->
(forall , t \in `]a, b[%R -> f t <= f c) -> is_derive c 1 f 0.

Proof.

move=> leab fdrvbl cab cmax; apply: DeriveDef; first exact: fdrvbl.
apply/eqP; rewrite eq_le; apply/andP; split.
  rewrite ['D_1 f c]cvg_at_rightE; first exact: fdrvbl.
  apply: limr_le.
    have /fdrvbl dfc := cab.
    rewrite -(cvg_at_rightE (fun : R => h^-1 *: ((f \o shift c) _ - f c))) //.
    apply: cvg_trans dfc; apply: cvg_app.
    move=> A [e egt0 Ae]; exists e => // x xe xgt0; apply: Ae => //.
    exact/lt0r_neq0.
  near=> h; apply: mulr_ge0_le0.
    by rewrite invr_ge0; apply: ltW; near: h; exists 1 => /=.
  rewrite subr_le0 [_%:A]mulr1; apply: cmax; near: h.
  exists (b - c); first by rewrite /= subr_gt0 (itvP cab).
  move=> h; rewrite /= distrC subr0 /= in_itv /= -ltrBrDr.
  move=> /(le_lt_trans (ler_norm _)) -> /ltr_pDl -> //.
  by rewrite (itvP cab).
rewrite ['D_1 f c]cvg_at_leftE; first exact: fdrvbl.
apply: limr_ge.
  have /fdrvbl dfc := cab; rewrite -(cvg_at_leftE (fun => h^-1 *: ((f \o shift c) _ - f c))) //.
  apply: cvg_trans dfc; apply: cvg_app.
  move=> A [e egt0 Ae]; exists e => // x xe xgt0; apply: Ae => //.
  exact/ltr0_neq0.
near=> h; apply: mulr_le0.
  by rewrite invr_le0; apply: ltW; near: h; exists 1 => /=.
rewrite subr_le0 [_%:A]mulr1; apply: cmax; near: h.
exists (c - a); first by rewrite /= subr_gt0 (itvP cab).
move=> h; rewrite /= distrC subr0.
move=> /ltr_normlP []; rewrite ltrBrDl ltrBlDl in_itv /= => -> _.
by move=> /ltr_nDl -> //; rewrite (itvP cab).
Unshelve. all: by end_near. Qed.

Lemma ( : realFieldType) ( : R -> R) ( : R) :
a <= b -> (forall , t \in `]a, b[%R -> derivable f t 1) -> c \in `]a, b[%R ->
(forall , 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; first 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 lerN2; apply: cmin.
Qed.

Lemma ( : realType) ( : R -> R) ( : R) :
  a < b -> (forall , x \in `]a, b[%R -> derivable f x 1) ->
  {within `[a, b], continuous f} -> f a = f b ->
  exists2 , 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_setE => /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_setE => /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; first 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 ( : realType) ( : R -> R) ( : R) :
  a < b -> (forall , x \in `]a, b[%R -> is_derive x 1 f (df x)) ->
  {within `[a, b], continuous f} ->
  exists2 , c \in `]a, b[%R & f b - f a = df c * (b - a).

Proof.

move=> altb fdrvbl fcont.
set g := f + (- ( *:%R^~ ((f b - f a) / (b - a)) : R -> R)).
have gdrvbl x : x \in `]a, b[%R -> derivable g x 1.
  by move=> /fdrvbl dfx; apply/derivableB/derivable1_diffP.
have gcont : {within `[a, b], continuous g}.
  move=> x; apply: continuousD _ ; first exact: fcont.
  exact/continuousN/continuous_subspaceT/scalel_continuous.
have gaegb : g a = g b.
  rewrite /g -![(_ - _ : _ -> _) _]/(_ - _).
  apply/eqP; rewrite -subr_eq /= opprK addrAC -addrA -scalerBl.
  rewrite [_ *: _]mulrC divfK; last by rewrite addrC subrK.
  by apply: lt0r_neq0; rewrite subr_gt0.
have [c cab dgc0] := Rolle altb gdrvbl gcont gaegb.
exists c; first exact: cab.
have /fdrvbl dfc := cab; move/@derive_val: dgc0; rewrite deriveB //.
move/eqP; rewrite [X in _ - X]deriveE // derive_val diff_val scale1r subr_eq0.
by move/eqP->; rewrite divfK// subr_eq0 gt_eqF.
Qed.

Lemma ( : realType) ( : R -> R) ( : R) :
  a <= b -> (forall , x \in `]a, b[%R -> is_derive x 1 f (df x)) ->
  {within `[a, b], continuous f} ->
  exists2 , 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.

Section ger0_derive1_le.
Context { : realType}.
Variables ( : R -> R) ( : R).
Hypothesis : forall , x \in `]a, b[%R -> derivable f x 1.
Hypothesis : forall , x \in `]a, b[%R -> 0 <= f^`() x.

Lemma ( : bool) :
{within [set` (Interval (BSide sa a) (BSide sb b))], continuous f} ->
{in Interval (BSide sa a) (BSide sb b) &, {homo f : / x <= y}}.

Proof.

move=> cf x y + + xy.
move: (xy); rewrite le_eqVlt=> /predU1P[-> | xy']; first by rewrite lexx.
rewrite !itv_boundlr -subr_ge0 /= => /andP[ax _] /andP[_ yb].
have HMVT1 : {within `[x, y], continuous f}.
  exact/(continuous_subspaceW _ cf)/subset_itv.
have zab : `]x, y[ `<=` `]a, b[.
  clear -ax yb; apply/subset_itv.
    by move: sa ax => []; rewrite !bnd_simp// => /ltW.
  by move: sb yb => []; rewrite !bnd_simp// => /ltW.
have HMVT0 z : z \in `]x, y[%R -> is_derive z 1 f (f^`() z).
  by move=> zxy; rewrite derive1E; exact/derivableP/df/zab.
have[z zxy ->]:= MVT xy' HMVT0 HMVT1.
by rewrite mulr_ge0// ?subr_ge0// dfge0// zab.
Qed.

Lemma : {within `[a, b] , continuous f} ->
{in `[a, b]%R &, {homo f : / x <= y >-> x <= y}}.

Proof.

exact: ger0_derive1_le. Qed.

Lemma : {within `[a, b[ , continuous f} ->
{in `[a, b[%R &, {homo f : / x <= y >-> x <= y}}.

Proof.

exact: ger0_derive1_le. Qed.

Lemma : {within `]a, b], continuous f} ->
{in `]a, b]%R &, {homo f : / x <= y >-> x <= y}}.

Proof.

exact: ger0_derive1_le. Qed.

Lemma : {in `]a, b[, continuous f} ->
{in `]a, b[%R &, {homo f : / x <= y >-> x <= y}}.

Proof.

by rewrite -continuous_open_subspace//; exact: ger0_derive1_le. Qed.

End ger0_derive1_le.

Section ler0_derive1_le.
Context { : realType}.
Variables ( : R -> R) ( : R).
Hypothesis : forall , x \in `]a, b[%R -> derivable f x 1.
Hypothesis : forall , x \in `]a, b[%R -> f^`() x <= 0.

Lemma ( : bool) :
{within [set` (Interval (BSide sa a) (BSide sb b))], continuous f} ->
{in Interval (BSide sa a) (BSide sb b) &, {homo f : /~ x <= y}}.

Proof.

move=> cf.
suff : {in Interval (BSide sa a) (BSide sb b) &, {homo (- f) : / x <= y}}.
by move=> h y x iy ix xy; move: (h x y ix iy xy); rewrite opprfctE lerNl opprK.
apply: ger0_derive1_le.
- move => x xab; exact/derivableN/df.
- move => x xab; rewrite derive1E deriveN; first exact: df.
by rewrite -derive1E oppr_ge0 dfle0.
by move=> x; exact/continuousN/cf.
Qed.

Lemma :{within `[a, b], continuous f} ->
{in `[a, b]%R &, {homo f : /~ x <= y}}.

Proof.

exact: ler0_derive1_le. Qed.

Lemma : {within `[a, b[, continuous f} ->
{in `[a, b[%R &, {homo f : /~ x <= y}}.

Proof.

exact: ler0_derive1_le. Qed.

Lemma : {within `]a, b], continuous f} ->
{in `]a, b]%R &, {homo f : /~ x <= y}}.

Proof.

exact: ler0_derive1_le. Qed.

Lemma : {in `]a, b[, continuous f} ->
{in `]a, b[%R &, {homo f : /~ x <= y}}.

Proof.

by rewrite -continuous_open_subspace//; exact: ler0_derive1_le. Qed.

End ler0_derive1_le.

#[deprecated(since="mathcomp-analysis 1.10.0",
  note="use `ler0_derive1_le_cc` instead")]
Lemma ( : realType) ( : R -> R) ( : R) :
  (forall , x \in `]a, b[%R -> derivable f x 1) ->
  (forall , x \in `]a, b[%R -> f^`() x <= 0) ->
  {within `[a, b], continuous f} ->
  forall , a <= x -> x <= y -> y <= b -> f y <= f x.

Proof.

move=> df dfle0 cf x y ax xy yb.
by apply: ler0_derive1_le_cc; [ exact: df | exact: dfle0 | by [] | | | by [] ];
rewrite in_itv/= ?ax ?yb ?andbT/= ?(le_trans ax)// (le_trans _ yb).
Qed.

Section gtr0_derive1_lt.
Context { : realType}.
Variables ( : R -> R) ( : R).
Hypothesis : forall , x \in `]a, b[%R -> derivable f x 1.
Hypothesis : forall , x \in `]a, b[%R -> 0 < f^`() x.

Lemma ( : bool) :
{within [set` (Interval (BSide sa a) (BSide sb b))], continuous f} ->
{in Interval (BSide sa a) (BSide sb b) &, {homo f : / x < y}}.

Proof.

move=> cf x y + + xy.
rewrite !itv_boundlr /= -subr_gt0 => /andP [] ax ? /andP [] ? yb.
have HMVT1: {within `[x, y], continuous f}.
  exact/(continuous_subspaceW _ cf)/subset_itv.
have zab : `]x, y[ `<=` `]a, b[.
  clear -ax yb; apply/subset_itv.
    by move: sa ax => []; rewrite !bnd_simp// => /ltW.
  by move: sb yb => []; rewrite !bnd_simp// => /ltW.
have HMVT0 ( : R^o) : z \in `]x, y[%R -> is_derive z 1 f (f^`() z).
  by move=> zxy; rewrite derive1E; exact/derivableP/df/zab.
have[z zxy ->]:= MVT xy HMVT0 HMVT1.
by rewrite mulr_gt0// ?subr_gt0// dfgt0// zab.
Qed.

Lemma : {within `[a, b], continuous f} ->
{in `[a, b]%R &, {homo f : / x < y}}.

Proof.

exact: gtr0_derive1_lt. Qed.

Lemma : {within `[a, b[, continuous f} ->
{in `[a, b[%R &, {homo f : / x < y}}.

Proof.

exact: gtr0_derive1_lt. Qed.

Lemma : {within `]a, b], continuous f} ->
{in `]a, b]%R &, {homo f : / x < y}}.

Proof.

exact: gtr0_derive1_lt. Qed.

Lemma : {in `]a, b[, continuous f} ->
{in `]a, b[%R &, {homo f : / x < y}}.

Proof.

by rewrite -continuous_open_subspace//; exact: gtr0_derive1_lt. Qed.

End gtr0_derive1_lt.

#[deprecated(since="mathcomp-analysis 1.10.0",
  note="use `gtr0_le_derive1` instead")]
Lemma ( : realType) ( : R -> R) ( : R) :
  (forall , x \in `]a, b[%R -> derivable f x 1) ->
  (forall , x \in `]a, b[%R -> 0 < f^`() x) ->
  {within `[a, b], continuous f}%classic ->
  forall , a <= x -> x < y -> y <= b -> f x < f y.

Proof.

move=> abf abf' cf x y ax xy yb; apply: (@gtr0_derive1_lt_cc _ _ a b) => //;
rewrite in_itv/= ?ax ?yb ?andbT/=.
- by rewrite (le_trans (ltW xy)).
- by rewrite (le_trans _ (ltW xy)).
Qed.

Section ltr0_derive1_lt.
Context { : realType}.
Variables ( : R -> R) ( : R).
Hypothesis : forall , x \in `]a, b[%R -> derivable f x 1.
Hypothesis : forall , x \in `]a, b[%R -> f^`() x < 0.

Lemma ( : bool) :
{within [set` (Interval (BSide sa a) (BSide sb b))], continuous f} ->
{in Interval (BSide sa a) (BSide sb b) &, {homo f : /~ x < y}}.

Proof.

move=> cf.
suff : {in Interval (BSide sa a) (BSide sb b) &, {homo (- f) : / x < y}}.
by move=> h x y ix iy xy; move: (h y x iy ix xy); rewrite opprfctE ltrNl opprK.
apply: gtr0_derive1_lt.
- move => x xab; exact/derivableN/df.
- move => x xab; rewrite derive1E deriveN; first exact: df.
by rewrite -derive1E oppr_gt0 dflt0.
by move=> x; exact/continuousN/cf.
Qed.

Lemma : {within `[a, b], continuous f} ->
{in `[a, b]%R &, {homo f : /~ x < y}}.

Proof.

exact: ltr0_derive1_lt. Qed.

Lemma : {within `[a, b[, continuous f} ->
{in `[a, b[%R &, {homo f : /~ x < y}}.

Proof.

exact: ltr0_derive1_lt. Qed.

Lemma : {within `]a, b], continuous f} ->
{in `]a, b]%R &, {homo f : /~ x < y}}.

Proof.

exact: ltr0_derive1_lt. Qed.

Lemma : {in `]a, b[, continuous f} ->
{in `]a, b[%R &, {homo f : /~ x < y}}.

Proof.

by rewrite -continuous_open_subspace//; exact: ltr0_derive1_lt. Qed.

End ltr0_derive1_lt.

#[deprecated(since="mathcomp-analysis 1.10.0",
  note="use `ler0_derive1_lt_cc` instead")]
Lemma ( : realType) ( : R -> R) ( : R) :
  (forall , x \in `]a, b[%R -> derivable f x 1) ->
  (forall , x \in `]a, b[%R -> f^`() x < 0) ->
  {within `[a, b], continuous f}%classic ->
  forall , a <= x -> x < y -> y <= b -> f y < f x.

Proof.

move=> df f'0 cf x y ax xy yb.
apply: ltr0_derive1_lt_cc; [ exact: df | exact: f'0 | by [] | | | by [] ];
rewrite !in_itv/= ?ax ?yb ?andbT/=.
by rewrite (le_trans _ (ltW xy)).
by rewrite (le_trans (ltW xy)).
Qed.

#[global] Hint Extern 0 (is_true (_ <= ?x)) => match goal with
    H : x \is_near _ |- _ =>
      solve[near: x; apply: nbhs_pinfty_ge; apply: num_real]
  end : core.
#[global] Hint Extern 0 (is_true (?x <= _)) => match goal with
    H : x \is_near _ |- _ =>
      solve[near: x; apply: nbhs_ninfty_le; apply: num_real]
  end : core.

Lemma { : realType} ( : R -> R) ( : R) :
  (forall , x \in `]a, +oo[%R -> derivable f x 1) ->
  (forall , x \in `]a, +oo[%R -> f^`() x <= 0) ->
  {within `[a, +oo[, continuous f} ->
  forall , a <= x -> x <= y -> f y <= f x.

Proof.

move=> df dfle0 cf x y ax xy.
near (pinfty_nbhs R)%R => N.
apply: (@ler0_derive1_le_cc _ _ a N) => [r|r| | | | // ]; rewrite ?in_itv/=.
- by move=> /andP[ar rN]; apply: df; rewrite !in_itv/= andbT ar.
- by move=> /andP[ar rN]; apply: dfle0; rewrite !in_itv/= andbT ar.
- exact/continuous_subspaceW/cf/subset_itvl.
- by rewrite (le_trans ax)/=.
- by rewrite ax/=.
Unshelve. all: end_near. Qed.

Lemma { : realType} ( : R -> R) ( : R) :
  (forall , x \in `]-oo, b[%R -> derivable f x 1) ->
  (forall , x \in `]-oo, b[%R -> f^`() x <= 0) ->
  {within `]-oo, b], continuous f} ->
  forall , x <= y -> y <= b -> f y <= f x.

Proof.

move=> df dfle0 cf x y xy yb.
near (ninfty_nbhs R)%R => N.
apply: (@ler0_derive1_le_cc _ _ N b) => [r|r| | | | // ]; rewrite ?in_itv/=.
- by move=> /andP[Nr rb]; apply: df; rewrite !in_itv/= rb.
- by move=> /andP[Nr rb]; apply: dfle0; rewrite !in_itv/= rb.
- exact/continuous_subspaceW/cf/subset_itvr.
- by rewrite yb andbT.
by rewrite (le_trans xy)//= andbT.
Unshelve. all: end_near. Qed.

Lemma ( : realType) ( : R -> R) ( : R) :
  (forall , x \in `]a, b[%R -> derivable f x 1) ->
  (forall , x \in `]a, b[%R -> 0 <= f^`() x) ->
  {within `[a,b], continuous f} ->
  forall , a <= x -> x <= y -> y <= b -> f x <= f y.

Proof.

move=> df dfge0 cf x y ax xy yb.
by apply: (@ger0_derive1_le_cc _ _ a b) => //;
rewrite in_itv/= ?(le_trans _ xy)//= ?(le_trans xy) ?andbT.
Qed.

#[deprecated(since="mathcomp-analysis 1.9.0",
  note="renamed to `ger0_derive1_ndecr`")]
Notation := ger0_derive1_ndecr (only parsing).

Lemma { : realType} ( : R -> R) ( : R) :
  (forall , x \in `]a, +oo[%R -> derivable f x 1) ->
  (forall , x \in `]a, +oo[%R -> 0 <= f^`() x) ->
  {within `[a, +oo[, continuous f} ->
  forall , a <= x -> x <= y -> f x <= f y.

Proof.

move=> df dfge0 cf x y ax xy.
near (pinfty_nbhs R)%R => N.
apply: (@ger0_derive1_le_cc _ _ a N) => [r|r| | | | // ]; rewrite ?in_itv/=.
- by move=> /andP[ar rN]; apply: df; rewrite !in_itv/= andbT ar.
- by move=> /andP[ar rN]; apply: dfge0; rewrite !in_itv/= andbT ar.
- exact/continuous_subspaceW/cf/subset_itvl.
- by rewrite (le_trans ax)/=.
- by rewrite (le_trans ax)/=.
Unshelve. all: end_near. Qed.

Lemma { : realType} ( : R -> R) ( : R) :
  (forall , x \in `]-oo, b[%R -> derivable f x 1) ->
  (forall , x \in `]-oo, b[%R -> 0 <= f^`() x) ->
  {within `]-oo, b], continuous f} ->
  forall , x <= y -> y <= b -> f x <= f y.

Proof.

move=> df dfge0 cf x y xy yb.
near (ninfty_nbhs R)%R => N.
apply: (@ger0_derive1_le_cc _ _ N b) => [r|r| | | | // ]; rewrite ?in_itv/=.
- by move=> /andP[Nr rb]; apply: df; rewrite !in_itv/=.
- by move=> /andP[Nr rb]; apply: dfge0; rewrite !in_itv/=.
- exact/continuous_subspaceW/cf/subset_itvr.
- by rewrite (le_trans xy)//= andbT.
- by rewrite yb andbT.
Unshelve. all: end_near. Qed.

Lemma { : realFieldType} ( : R -> R) ( : set R) ( : R) :
  {in D° : set R, forall , derivable f x 1%R} ->
  {in D &, {homo f : /~ x < y}} ->
  D° x -> f^`() x <= 0.

Proof.

move=> df decrf Dx.
apply: limr_le.
  under eq_fun; first (move=> h; rewrite -{2}(scaler1 h); over).
  by apply: df; rewrite inE.
have [e /= e0 Hball] := open_subball (open_interior D) Dx.
near=> h.
have h0 : h != 0%R by near: h; exact: nbhs_dnbhs_neq.
have Dhx : D° (h + x).
  apply: (Hball (`|2 * h|%R)) => //.
  - rewrite /= sub0r normrN normr_id normrM ger0_norm// -ltr_pdivlMl//.
      by near: h; apply: dnbhs0_lt; exact: mulr_gt0.
    by rewrite normrM ger0_norm// mulr_gt0// normr_gt0.
  apply: ball_sym; rewrite /ball/= addrK.
  by rewrite normrM (@ger0_norm _ 2)// ltr_pMl ?normr_gt0// ltr1n.
move: h0; rewrite neq_lt => /orP[h0|h0].
- rewrite nmulr_rle0 ?invr_lt0// subr_ge0 ltW//.
  by apply: decrf; rewrite ?in_itv ?andbT ?gtrDr// inE; exact: interior_subset.
- rewrite pmulr_rle0 ?invr_gt0// subr_le0 ltW//.
  by apply: decrf; rewrite ?in_itv ?andbT ?ltrDr// inE; exact: interior_subset.
Unshelve. end_near. Qed.

Lemma { : realType} ( : R -> R)
    ( : bool) ( : R) ( : R) :
  {in `]a, b[, forall : R, derivable f x 1%R} ->
  {in Interval (BSide b0 a) (BSide b1 b) &, {homo f : /~ (x < y)%R}} ->
  z \in `]a, b[%R -> f^`() z <= 0.

Proof.

have [?|ab] := leP b a; first by move=> _ _ /lt_in_itv; rewrite bnd_simp le_gtF.
move=> df decrf zab.
have {}zab : [set` (Interval (BSide b0 a) (BSide b1 b))]° z.
by rewrite interior_itv// inE/=.
apply: decr_derive1_le0 zab; first by rewrite interior_itv.
by move=> x y /[!inE]/=; apply/decrf.
Qed.

Lemma { : realType} ( : R -> R)
    ( : bool) ( : R) ( : R) :
  {in `]a, +oo[, forall : R, derivable f x 1%R} ->
  {in Interval (BSide b0 a) (BInfty _ false) &, {homo f : /~ (x < y)%R}} ->
  z \in `]a, +oo[%R -> f^`() z <= 0.

Proof.

move=> df decrf zay.
have {}zay : [set` (Interval (BSide b0 a) (BInfty _ false))]° z.
by rewrite interior_itv// inE/=.
apply: decr_derive1_le0 zay; first by rewrite interior_itv.
by move=> x y /[!inE]/=; apply/decrf.
Qed.

Lemma { : realType} ( : R -> R)
    ( : bool) ( : R) ( : R) :
  {in `]-oo, b[, forall : R, derivable f x 1%R} ->
  {in Interval (BInfty _ true) (BSide b1 b) &, {homo f : /~ (x < y)%R}} ->
  z \in `]-oo, b[%R -> f^`() z <= 0.

Proof.

move=> df decrf zNyb.
have {}zNyb : [set` (Interval (BInfty _ true) (BSide b1 b))]° z.
by rewrite interior_itv// inE/=.
apply: decr_derive1_le0 zNyb; first by rewrite interior_itv.
by move=> x y /[!inE]/=; apply/decrf.
Qed.

Lemma { : realFieldType} ( : R -> R)
   ( : set R) ( : R):
  {in D° : set R, forall : R, derivable f x 1%R} ->
  {in D &, {homo f : / (x < y)%R}} ->
  D° x -> 0 <= f^`() x.

Proof.

move=> df incrf Dx; rewrite -[leRHS]opprK oppr_ge0.
have dfx : derivable f x 1 by apply: df; rewrite inE.
rewrite derive1E -deriveN// -derive1E; apply: decr_derive1_le0 Dx.
- by move=> y Dy; apply: derivableN; apply: df.
- by move=> y z Dy Dz yz; rewrite ltrN2; apply: incrf.
Qed.

Lemma { : realType} ( : R -> R)
  ( : bool) ( : R) ( : R) :
  {in `]a, b[ : set R, forall : R, derivable f x 1%R} ->
  {in Interval (BSide b0 a) (BSide b1 b) &, {homo f : / (x < y)%R}} ->
  z \in `]a, b[%R -> 0 <= f^`() z.

Proof.

move=> df incrf zab; rewrite -[leRHS]opprK oppr_ge0.
have dfz : derivable f z 1 by apply: df; rewrite inE.
rewrite derive1E -deriveN// -derive1E.
apply: (@decr_derive1_le0_itv _ _ b0 b1 a b); last exact: zab.
- by move=> y Dy; apply: derivableN; apply: df.
- move=> x y Dx Dy yx; rewrite ltrN2; apply: incrf => //; rewrite in_itv/=.
Qed.

Lemma { : realType} ( : R -> R)
    ( : bool) ( : R) ( : R) :
  {in `]a, +oo[, forall : R, derivable f x 1%R} ->
  {in Interval (BSide b0 a) +oo%O &, {homo f : / (x < y)%R}} ->
  z \in `]a, +oo[%R -> 0 <= f^`() z.

Proof.

move=> df incrf zay; rewrite -[leRHS]opprK oppr_ge0.
have dfz : derivable f z 1 by apply: df; rewrite inE.
rewrite derive1E -deriveN// -derive1E.
apply: (@decr_derive1_le0_itvy _ _ b0 _ _ _ _ zay).
- by move=> y Dy; apply: derivableN; apply: df.
- by move=> x y Dx Dy yx; rewrite ltrN2; apply: incrf.
Qed.

Lemma { : realType} ( : R -> R)
    ( : bool) ( : R) ( : R) :
  {in `]-oo, b[, forall : R, derivable f x 1%R} ->
  {in Interval (BInfty _ true) (BSide b1 b) &, {homo f : / (x < y)%R}} ->
  z \in `]-oo, b[%R -> 0 <= f^`() z.

Proof.

move=> df incrf zNyb; rewrite -[leRHS]opprK oppr_ge0.
have dfz : derivable f z 1 by apply: df; rewrite inE.
rewrite derive1E -deriveN// -derive1E.
apply: (@decr_derive1_le0_itvNy _ _ b1 _ _ _ _ zNyb).
- by move=> y Dy; apply: derivableN; apply: df.
- by move=> x y Dx Dy yx; rewrite ltrN2; apply: incrf.
Qed.

Lemma ( : realFieldType) ( : R -> R) :
derivable f x 1 -> derivable g (f x) 1 ->
(g \o f)^`() x = g^`()%classic (f x) * f^`()%classic x.

Proof.

move=> /derivable1_diffP df /derivable1_diffP dg.
rewrite derive1E'; first exact/differentiable_comp.
rewrite diff_comp // !derive1E' //= -[X in 'd _ _ X = _]mulr1.
by rewrite [LHS]linearZ mulrC.
Qed.

Global Instance ( : realFieldType) ( : R -> R) ( : R) :
is_derive (g x) 1 f a -> is_derive x 1 g b -> is_derive x 1 (f \o g) (a * b).

Proof.

move=> [fgxv <-{a}] [gv <-{b}]; apply: (@DeriveDef _ _ _ _ _ (f \o g)).
apply/derivable1_diffP/differentiable_comp; first exact/derivable1_diffP.
by move/derivable1_diffP in fgxv.
by rewrite -derive1E (derive1_comp gv fgxv) 2!derive1E.
Qed.

Lemma ( : numFieldType) ( : normedModType R)
    ( : V -> W) ( : V) : {near a, f =1 g} ->
   \forall \near 0,
     h^-1 *: (f (h *: v + a) - f a) = h^-1 *: (g (h *: v + a) - g a).

Proof.

move=> fg; near do rewrite (nbhs_singleton fg) (near fg)// addrC.
apply/(@near0Z _ _ _ [set | (a + v) \is_near (nbhs a)])=> /=.
by rewrite (near_shift a)/=; near do rewrite /= sub0r addrC addrNK//.
Unshelve. all: by end_near. Qed.

Lemma ( : numFieldType) ( : normedModType R)
( : V -> W) ( : V) :
{near a, f =1 g} -> derivable f a v -> derivable g a v.

Proof.

have [-> _ _|] := eqVneq v 0; first exact/derivable0.
move=> vn0 nfg /cvg_ex[/= l fl]; apply/cvg_ex; exists l => /=.
exact/(cvg_trans _ fl)/near_eq_cvg/cvg_within/near_eq_growth_rate.
Qed.

Lemma ( : numFieldType) ( : normedModType R)
( : V -> W) ( : V) :
(\near , f a = g a) -> 'D_v f a = 'D_v g a.

Proof.

have [-> _|] := eqVneq v 0; first by rewrite !derive0.
move=> v0 fg; rewrite /derive; congr (lim _).
rewrite eqEsubset; split; apply/near_eq_cvg/cvg_within/near_eq_growth_rate =>//.
by near do apply/esym.
Unshelve. all: by end_near. Qed.

Lemma ( : numFieldType) ( : normedModType R)
( : V -> W) ( : V) ( : W) :
(\near , f a = g a) -> is_derive a v f df -> is_derive a v g df.

Proof.

move=> fg [fav <-]; rewrite (near_eq_derive _ fg).
by apply: DeriveDef => //; exact: near_eq_derivable fav.
Qed.

Section Derive_max.
Context { : realType} { : normedModType K}.
Implicit Types f g : V -> K^o.
Implicit Type x : V.

Fact : f x != g x ->
  derivable f x v -> derivable g x v ->
  {for x, continuous f} -> {for x, continuous g} ->
  (fun => h^-1 *: (((f \max g) \o shift x) (h *: v) - (f \max g) x))
    @ 0^' --> if f x < g x then 'D_v g x else 'D_v f x.

Proof.

wlog: f g x / f x < g x.
  move=> wlg; rewrite neq_lt => /orP[fg|gf df dg fxv gxv].
  - by apply: wlg => //; rewrite lt_eqF.
  - rewrite fun_maxC ltNge if_neg le_eqVlt eq_sym gt_eqF//=.
    by apply: wlg => //; rewrite lt_eqF.
move=> fx_lt_gx fg_neq df dg cf cg; case: ifPn => fg /=.
- rewrite /Num.max fg => A DgxA.
  apply: (@near_eq_cvg _ _ _ _ (fun => h^-1 *: (g (h *: v + x) - g x))).
  + near do rewrite ifT// -subr_lt0 -[ltLHS]/(((f - g) \o shift x) (_ *: v)).
    have Hf ( : V -> K^o) : continuous_at x h ->
        h (shift x (k *: v)) @[ --> nbhs 0^'] --> h x.
      move=> ch.
      apply: cvg_comp; last exact: ch.
      rewrite -[in nbhs x](add0r x); apply: cvgD => //.
      rewrite -(scale0r v); apply: cvgZ => //.
      exact: nbhs_dnbhs.
    apply/(cvgr_lt (f x - g x)); last by rewrite subr_lt0.
    by apply: cvgB; exact: Hf.
  + exact: dg.
- absurd.
  by rewrite fx_lt_gx in fg.
Unshelve. all: by end_near. Qed.

Lemma :
  f x != g x -> derivable f x v -> derivable g x v ->
  {for x, continuous f} -> {for x, continuous g} ->
  derivable (f \max g) x v.

Proof.

move=> fx_gx df dg cf cg; apply/cvg_ex => /=.
exists (if f x < g x then 'D_v g x else 'D_v f x).
exact: der_max_subproof.
Qed.

Lemma : f x > g x ->
{for x, continuous f} -> {for x, continuous g} ->
'D_v (f \max g) x = 'D_v f x.

Proof.

have [-> gx_fx cf cg|v0 fg cf cg]:= eqVneq v 0.
by rewrite !derive0.
apply: near_eq_derive => //.
near do rewrite /Order.max_fun /Num.max ifN// -leNgt -subr_le0.
by move: fg; rewrite -subr_lt0; apply: cvgr_le; exact: cvgB.
Unshelve. all: by end_near. Qed.

Lemma : f x < g x ->
{for x, continuous f} -> {for x, continuous g} ->
'D_v (f \max g) x = 'D_v g x.

Proof.

by move=> fg cf cg; rewrite fun_maxC derive_maxl. Qed.

Lemma :
  f x != g x -> derivable f x v -> derivable g x v ->
  {for x, continuous f} -> {for x, continuous g} ->
  derivable (f \min g) x v.

Proof.

have [-> *|x0] := eqVneq v 0; first exact/derivable0.
rewrite min_fun_to_max => fx_gx df dg cf cg.
by apply/derivableB; [apply/(derivableD df dg) |apply/derivable_max].
Qed.

Lemma : f x > g x ->
{for x, continuous f} -> {for x, continuous g} ->
'D_v (f \min g) x = 'D_v g x.

Proof.

have [-> *|v0 fg cf cg] := eqVneq v 0; first by rewrite !derive0.
apply: near_eq_derive => //.
near do rewrite /Order.min_fun /Num.min ifN// -leNgt -subr_le0.
by move: fg; rewrite -subr_lt0; apply: cvgr_le; exact: cvgB.
Unshelve. all: by end_near. Qed.

Lemma : f x < g x ->
{for x, continuous f} -> {for x, continuous g} ->
'D_v (f \min g) x = 'D_v f x.

Proof.

by move=> fg cf cg; rewrite fun_minC derive_minr. Qed.

End Derive_max.

Lemma { : realFieldType} ( : R -> R) ( : R) :
derivable f x 1 -> (- f)^`() x = (- f^`()%classic x).

Proof.

by move=> fx; rewrite !derive1E deriveN. Qed.

Lemma { : realFieldType} ( : R) : derivable -%R x v.

Proof.

by apply: derivableN; exact: derivable_id. Qed.

Lemma { : realFieldType} ( : R) : id^`() x = 1.

Proof.

by rewrite derive1E derive_id. Qed.

Lemma ( : realType) ( : R -> R) :
is_derive x (1 : R) f x1 -> x1 = y1 -> is_derive x 1 f y1.

Proof.

by move=> Hi <-. Qed.

Section derive_horner.
Variable ( : realFieldType).
Local Open Scope ring_scope.

Lemma : horner (0 : {poly R}) = 0.

Proof.

by apply/funext => y /=; rewrite horner0. Qed.

Lemma ( : {poly R}) :
horner (p * 'X + r%:P) = horner (p * 'X) + horner (r%:P).

Proof.

by apply/funext => y /=; rewrite !(hornerE,fctE). Qed.

Lemma ( : {poly R}) :
horner (p * 'X) = (fun => p.[x] * x)%R.

Proof.

by apply/funext => y; rewrite !hornerE. Qed.

Lemma ( : R) : horner r%:P = cst r.

Proof.

by apply/funext => y /=; rewrite !hornerE. Qed.

Lemma ( : {poly R}) : derivable (horner p) x 1.

Proof.

elim/poly_ind: p => [|p r ih]; first by rewrite horner0_ext.
rewrite hornerD_ext; apply: derivableD.
- rewrite horner_scale_ext/=.
by apply: derivableM; [exact:ih|exact:derivable_id].
- by rewrite hornerC_ext; exact: derivable_cst.
Qed.

Lemma ( : {poly R}) : horner (p^`()) = (horner p)^`()%classic.

Proof.

apply/funext => x; elim/poly_ind: p => [|p r ih].
by rewrite deriv0 hornerC horner0_ext derive1_cst.
rewrite derivD hornerD hornerD_ext.
rewrite derive1E deriveD//; [exact: derivable_horner..|].
rewrite -!derive1E hornerC_ext derive1_cst addr0.
rewrite horner_scale_ext derive1E deriveM//; first exact: derivable_horner.
rewrite derive_id -derive1E -ih derivC horner0 addr0 derivM hornerD !hornerE.
by rewrite derivX hornerE mulr1 addrC mulrC scaler1.
Qed.

Global Instance ( : {poly R}) ( : R) :
is_derive x (1:R) (horner p) p^`().[x].

Proof.

by apply: DeriveDef; [exact: derivable_horner|rewrite derivE derive1E].
Qed.

Lemma ( : {poly R}) : continuous (horner p).

Proof.

move=> /= x; apply/differentiable_continuous.
exact/derivable1_diffP/derivable_horner.
Qed.

End derive_horner.

Section pointwise_derivable.
Context { : realFieldType} { : normedModType R} { : nat}.
Implicit Types M : V -> 'M[R]_(m, n).

Lemma :
derivable M t v <-> forall , derivable (fun => M x i j) t v.

Proof.

split=> [|Mvt].
- move=> /cvg_ex[/= l Mvtl] i j; apply/cvg_ex; exists (l i j).
  apply/cvgrPdist_le => /= e e0.
  move/cvgrPdist_le : Mvtl => /(_ _ e0)[/= r r0] rMvte.
  near=> x.
  apply: le_trans (rMvte x _ _).
  + rewrite [leRHS]/Num.Def.normr/= mx_normrE.
    apply: le_trans; last exact: le_bigmax.
    by rewrite !mxE.
  + rewrite /ball_/= sub0r normrN.
    by near: x; exact: dnbhs0_lt.
  + near: x; exact: nbhs_dnbhs_neq.
- apply/cvg_ex => /=.
  exists (\matrix_( < m, < n) sval (cid ((cvg_ex _).1 (Mvt i j)))).
  apply/cvgrPdist_le => /= e e0.
  near=> x.
  rewrite /Num.Def.normr/= mx_normrE (bigmax_le _ (ltW e0))//= => i _.
  rewrite !mxE/=.
  move: i; near: x; apply: filter_forall => /= i.
  exact: ((cvgrPdist_le _ _).1 (svalP (cid ((cvg_ex _).1 (Mvt i.1 i.2))))).
Unshelve. all: by end_near. Qed.

End pointwise_derivable.

Section pointwise_derive.
Local Open Scope classical_set_scope.
Context { : realFieldType} { : normedModType R}.

Lemma { : nat} ( : V -> 'M[R]_(m, n)) :
derivable M t v ->
'D_v M t = \matrix_( < m, < n) 'D_v (fun => M t i j) t.

Proof.

move=> /cvg_ex[/= l Mvtl]; apply/cvg_lim => //=; apply/cvgrPdist_le => /= e e0.
move/cvgrPdist_le : (Mvtl) => /(_ (e / 2)) /[!divr_gt0]// /(_ isT)[d /= d0 dle].
near=> x.
rewrite [leLHS]/Num.Def.normr/= mx_normrE (bigmax_le _ (ltW e0))//= => -[i j] _.
rewrite [in leLHS]mxE/= [X in _ + X]mxE -(subrKA (l i j)).
rewrite (le_trans (ler_normD _ _))// (splitr e) lerD//.
- rewrite mxE.
  suff : (h^-1 *: (M (h *: v + t) i j - M t i j)) @[ --> 0^'] --> l i j.
    move/cvg_lim => /=; rewrite /derive /= => ->//.
    by rewrite subrr normr0 divr_ge0// ltW.
  apply/cvgrPdist_le => /= r r0.
  move/cvgrPdist_le : Mvtl => /(_ r r0)[/= s s0] sr.
  near=> y.
  apply: (@le_trans _ _ (`|l - y^-1 *: (M (y *: v + t) - M t)|)).
    rewrite [in leRHS]/Num.Def.normr/= mx_normrE.
    by under eq_bigr do rewrite !mxE; exact: (le_bigmax _ _ (i, j)).
  rewrite sr//=; last by near: y; exact: nbhs_dnbhs_neq.
  by rewrite sub0r normrN; near: y; exact: dnbhs0_lt.
- rewrite mxE.
  apply: (@le_trans _ _ `|l - x^-1 *: (M (x *: v + t) - M t)|).
    rewrite [in leRHS]/Num.Def.normr/= mx_normrE/=.
    under eq_bigr do rewrite !mxE.
    apply: le_trans; last exact: le_bigmax.
    by rewrite !mxE.
  apply: dle => //=; last by near: x; exact: nbhs_dnbhs_neq.
  by rewrite sub0r normrN; near: x; exact: dnbhs0_lt.
Unshelve. all: by end_near. Qed.

Global Instance { : nat} ( : V -> 'M[R]_(m, n))
    ( : 'M[R]_(m, n)) ( : V) :
  (forall , is_derive x v (fun => M t i j) (dM i j)) ->
  is_derive x v M dM.

Proof.

move=> MdM; apply: DeriveDef; first exact/derivable_mxP.
apply/matrixP => i j.
have [_ <-] := MdM i j.
rewrite derive_mx ?mxE//.
apply/derivable_mxP => i0 j0.
by have [] := MdM i0 j0.
Qed.

Fact { : nat} ( : V -> 'M[R]_(m, n)) ( : V) :
  let := fun : V => (\matrix_( < m, < n) 'd M x t i j) in
  differentiable M x ->
  continuous g /\
  M \o shift x = cst (M x) + g +o_ 0 id.

Proof.

move=> dM Mx; split => [|].
- apply/continuous_mx => i j v; apply/cvgrPdist_le => /= e e0.
  case: Mx => -[+ _] => /(_ v)/cvgrPdist_le/(_ _ e0).
  apply: filterS => /= t; apply: le_trans.
  by rewrite {2}/Num.norm/= mx_normrE (le_trans _ (le_bigmax _ _ (i, j))) ?mxE.
- apply/eqaddoE; rewrite funeqE => y /=.
  rewrite (diff_locallyx Mx) /dM !fctE; congr (_ + _ + _).
  by apply/matrixP => i j/=; rewrite mxE.
Qed.

Lemma { : nat} ( : V -> 'M[R]_(m, n)) :
  differentiable M x ->
  'd M (nbhs_filter_on x) =
  (fun : V => \matrix_( < m, < n) 'd M x t i j) :> (_ -> _).

Proof.

move=> dM.
set g := fun : V => \matrix_(, ) 'd M x t i j.
have glin : linear (g : V -> _).
move=> a u w.
by rewrite /g linearD linearZ/=; apply/matrixP => i j; rewrite !mxE.
pose glM := GRing.isLinear.Build _ _ _ _ _ glin.
pose gL : {linear _ -> _} := HB.pack g glM.
by apply: (@diff_unique _ _ _ _ gL); have [? ?] := dmx dM.
Qed.

Global Instance
    ( : V -> 'M[R]_(n, m)) ( : 'M[R]_(n,m)) ( : V) :
  is_derive t w f f' ->
  forall , is_derive t w (fun => f x i j) (f' i j).

Proof.

move=> fD i j /=.
have fDer : derivable f t w by case: fD.
apply/DeriveDef; last by have [_ <-] := fD; rewrite derive_mx// mxE.
by move/derivable_mxP : fDer => /(_ i j).
Qed.

Global Instance
    ( : V -> 'M[R]_(n, m))
    ( : V -> 'M[R]_(m, p)) ( : V) :
  is_derive t w M M' -> is_derive t w N N' ->
  is_derive t w (fun => M t *m N t) (M' *m N t + M t *m N').

Proof.

move=> is_der_M' is_der_N'.
apply is_derive_mx => i j /=.
rewrite !mxE/=.
under eq_fun do rewrite mxE/=.
rewrite -!big_split /= -fct_sumE.
apply/is_derive_sum => k.
by rewrite mulrC addrC; exact/is_deriveM.
Qed.

End pointwise_derive.

Section Ris_diff_mx.
Local Open Scope classical_set_scope.
Context { : realFieldType}.

Global Instance { : nat} ( : R -> 'M[R]_(m, n)) ( : R) :
(forall , is_diff x (fun t => M t i j) (fun => dM t i j)) ->
is_diff x M dM.

Proof.

move=> /= MdM.
have diffMx : differentiable M (nbhs_filter_on x).
apply/derivable1_diffP; apply/derivable_mxP => i j.
by have [/(@derivable1_diffP _ _ (fun => M t i j) x)] := MdM i j.
apply: DiffDef; first exact: diffMx.
rewrite diffmx//=; apply/funext => /= v; apply/matrixP => i j.
rewrite !mxE.
have [diffMij dMdM] := MdM i j.
rewrite -deriveE//.
move/(congr1 (fun => f v)) : dMdM.
rewrite -(deriveE _ diffMij) => <-.
rewrite derive_mx; last by rewrite /= mxE.
apply/derivable_mxP => i0 j0/=.
by have [/diff_derivable-/(_ v)] := MdM i0 j0.
Qed.

End Ris_diff_mx.

Section derivable_derive_row_mx.
Context { : realFieldType} { : normedModType R} { : nat}.
Implicit Types (f : V -> 'rV[R]_n1) (g : V -> 'rV[R]_n2).

Lemma : derivable f t v -> derivable g t v ->
derivable (fun => row_mx (f x) (g x)) t v.

Proof.

move=> /= fv gv; apply/derivable_mxP => i j; rewrite (ord1 i)/=.
have /cvg_ex[/= l Hl] := fv.
have /cvg_ex[/= k Hk] := gv.
apply/cvg_ex => /=; exists (row_mx l k ord0 j).
apply/cvgrPdist_le => /= e e0.
move/cvgrPdist_le : Hl => /(_ _ e0) Hl.
move/cvgrPdist_le : Hk => /(_ _ e0) Hk.
move: Hl Hk; apply: filterS2 => x Hl Hk.
rewrite !mxE; case: fintype.splitP => j1 jj1.
- rewrite (le_trans _ Hl)// [in leRHS]/Num.Def.normr/= mx_normrE.
by rewrite (le_trans _ (le_bigmax _ _ (ord0, j1)))// !mxE.
- rewrite (le_trans _ Hk)// [in leRHS]/Num.Def.normr/= mx_normrE.
by rewrite (le_trans _ (le_bigmax _ _ (ord0, j1)))// !mxE.
Qed.

Lemma : derivable f t v -> derivable g t v ->
'D_v (fun => row_mx (f x) (g x)) t = row_mx ('D_v f t) ('D_v g t).

Proof.

move=> fv gv; rewrite derive_mx.
  by apply: derivable_row_mx; [exact: fv|exact: gv].
apply/matrixP => i j.
rewrite !mxE !derive_mx//; case: splitP => k jE; rewrite !mxE; congr ('D_v _ t);
  apply/funext => w; rewrite !mxE; case: splitP => l lE//.
- by congr (f w i _); apply/val_inj => /=; rewrite -jE -lE.
- by absurd: lE; rewrite ltn_eqF//= jE (leq_trans (ltn_ord k))// leq_addr.
- by absurd: lE; rewrite gtn_eqF//= jE (leq_trans (ltn_ord l))// leq_addr.
- congr (g w i _); apply/val_inj => /=.
  by apply/eqP; rewrite -(eqn_add2l n1) -lE -jE.
Qed.

Global Instance :
is_derive x v f A -> is_derive x v g B ->
is_derive x v (fun => row_mx (f t) (g t)) (row_mx A B).

Proof.

move=> [dfx fA] [dgx gB]; apply: DeriveDef; first exact: derivable_row_mx.
by rewrite derive_row_mx// fA gB.
Qed.

End derivable_derive_row_mx.

Lemma ( : realFieldType) { : nat} ( : filter_on K)
( : K -> 'M[K]_(m, n1)) ( : K -> 'M[K]_(m, n2)) ( : K -> K) :
(fun => row_mx ([o_F f of A1] t) ([o_F f of A2] t)) =o_F f.

Proof.

apply/eqoP => _/posnumP[e]; near=> x; rewrite norm_row_mx ge_max.
by apply/andP; split; near: x; apply: littleoP.
Unshelve. all: by end_near. Qed.

Section is_diff_row_mx.
Local Open Scope classical_set_scope.
Context { : realFieldType} { : nat}.
Implicit Types (M dM : R -> 'rV[R]_n1) (N dN : R -> 'rV[R]_n2) (x t : R).

Fact ( : R -> R) : differentiable M x -> differentiable N x ->
  continuous (fun => row_mx ('d M x y) ('d N x y)) /\
  (fun => row_mx (M y) (N y)) \o shift x = cst (row_mx (M x) (N x)) +
  (fun => row_mx ('d M x y) ('d N x y)) +o_ 0 id.

Proof.

move=> df dg; split=> [/= ?|].
  by apply: cvg_row_mx => //=; exact: diff_continuous.
apply/eqaddoE; rewrite funeqE => y /=.
rewrite ![_ (_ + x)]diff_locallyx//.
have ->/= : forall , row_mx (M x + 'd M x y + [o_ 0 id of h] y)
  (N x + 'd N x y + [o_ 0 id of e] y) =
  row_mx (M x) (N x) + row_mx ('d M x y) ('d N x y) +
  row_mx ([o_ 0 id of h] y) ([o_ 0 id of e] y).
  by move=> /= h e; rewrite !add_row_mx.
congr (_ + _).
by rewrite -[LHS]/((fun => row_mx (_ y) (_ y)) y) eqo_row_mx.
Qed.

Lemma : differentiable M x -> differentiable N x ->
'd (fun => row_mx (M y) (N y)) x =
(fun => row_mx ('d M x y) ('d N x y)) :> (R -> 'rV[R]_(n1 + n2)).

Proof.

move=> df dg.
pose d := row_mx ('d M x y) ('d N x y).
have lin_row_mx : linear d.
by move=> /= a b c; rewrite /d 2!linearPZ scale_row_mx add_row_mx.
pose row_mxlM := GRing.isLinear.Build _ _ _ _ _ lin_row_mx.
pose row_mxL : {linear _ -> _} := HB.pack d row_mxlM.
rewrite -/d -[d]/(row_mxL : _ -> _).
by apply: diff_unique; have [] := drow_mx id df dg.
Qed.

Lemma : differentiable M x -> differentiable N x ->
differentiable (fun => row_mx (M t) (N t)) x.

Proof.

by move=> df dg; apply/diff_locallyP; rewrite diff_row_mx //; apply: drow_mx.
Qed.

Global Instance :
is_diff x M dM -> is_diff x N dN ->
is_diff x (fun t => row_mx (M t) (N t)) (fun => row_mx (dM t) (dN t)).

Proof.

move=> dfx dgx; apply: DiffDef; first exact: differentiable_row_mx.
by rewrite diff_row_mx// !diff_val.
Qed.

End is_diff_row_mx.

Files

Module mathcomp.analysis.derive