Added differentiability of the max function

CHANGELOG_UNRELEASED.md

@@ -10,6 +10,12 @@
 - in set_interval.v
   + `itv_is_open_unbounded`, `itv_is_oo`, `itv_open_ends` (Prop to bool)
 
+- in `functions.v`:
+  + lemmas `fun_maxC`, `fun_minC`, `min_fun_to_max`, `max_fun_to_min`
+
+- in `derive.v`:
+  + lemmas `derivable_max`, `derive_maxl`, `derive_maxr` `derivable_min`, `derive_minl`, `derive_minr`
+
 ### Renamed
 - in set_interval.v
   + `itv_is_ray` -> `itv_is_open_unbounded`

classical/functions.v

@@ -2677,6 +2677,24 @@ Lemma mul_funC (T : Type) {R : comPzSemiRingType} (f : T -> R) (r : R) :
   r \*o f = r \o* f.
 Proof. by apply/funext => x/=; rewrite mulrC. Qed.
 
+Lemma min_fun_to_max (T : Type) (T' : numDomainType) (f g : T -> T') :
+  (f \min g) = (f + g) - (f \max g).
+Proof.
+apply/funext=> x /=; by rewrite Num.Theory.minr_to_max. Qed.
+
+Lemma max_fun_to_min (T : Type) (T' : numDomainType) (f g : T -> T') :
+  (f \max g) = (f + g) - (f \min g).
+Proof.
+apply/funext => x /=; by rewrite Num.Theory.maxr_to_min. Qed.
+
+Lemma fun_maxC d (T : Type) (T' : orderType d) (f g : T -> T') :
+  f \max g = g \max f.
+Proof. by apply/funext => z/=; rewrite Order.TotalTheory.maxC. Qed.
+
+Lemma fun_minC d (T : Type) (T' : orderType d) (f g : T -> T') :
+  f \min g = g \min f.
+Proof. by apply/funext => z/=; rewrite Order.TotalTheory.minC. Qed.
+
 End function_space.
 
 Section function_space_lemmas.

theories/derive.v

@@ -304,6 +304,27 @@ move=> df; apply/derivable_nbhsP; apply/eqaddoE; rewrite funeqE => h.
 by rewrite /= addrC df.
 Qed.
 
+Lemma derivable0 (f : V -> W) (x : V) : derivable f x 0.
+Proof.
+apply:is_cvg_near_cst => //=.
+near=>h.
+by rewrite scaler0 add0r subrr scaler0.
+Unshelve.
+end_near.
+Qed.
+
+Lemma derive0 (f : V -> W) (x : V) : 'D_0 f x = 0.
+Proof.
+apply/lim_near_cst => //=.
+near=> h.
+by rewrite scaler0 add0r subrr scaler0.
+Unshelve.
+end_near.
+Qed.
+
+Lemma is_derive0 (f : V -> W) (x : V) : is_derive x 0 f 0.
+Proof. split; [by apply/derivable0 | by rewrite derive0]. Qed.
+
 End DifferentialR.
 
 Notation "''D_' v f" := (derive f ^~ v).
@@ -2024,40 +2045,146 @@ by rewrite [LHS]linearZ mulrC.
 Qed.
 
 Lemma near_eq_growth_rate (R : numFieldType) (V W : normedModType R)
-    (f g : V -> W) (a v : V) : v != 0 -> {near a, f =1 g} ->
+    (f g : V -> W) (a v : V) : {near a, f =1 g} ->
    \forall h \near 0,
      h^-1 *: (f (h *: v + a) - f a) = h^-1 *: (g (h *: v + a) - g a).
 Proof.
-move=> v0 fg; near do rewrite (nbhs_singleton fg) (near fg)// addrC.
+move=> fg; near do rewrite (nbhs_singleton fg) (near fg)// addrC.
 apply/(@near0Z _ _ _ [set v | (a + v) \is_near (nbhs a)])=> /=.
 by rewrite (near_shift a)/=; near do rewrite /= sub0r addrC addrNK//.
 Unshelve. all: by end_near. Qed.
 
 Lemma near_eq_derivable (R : numFieldType) (V W : normedModType R)
-    (f g : V -> W) (a v : V) : v != 0 ->
+    (f g : V -> W) (a v : V) :
   {near a, f =1 g} -> derivable f a v -> derivable g a v.
 Proof.
+case: (eqVneq v 0)=> [-> _ _| ].
+by apply/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 near_eq_derive (R : numFieldType) (V W : normedModType R)
   (f g : V -> W) (a v : V) :
-  v != 0 -> (\near a, f a = g a) -> 'D_v f a = 'D_v g a.
+  (\near a, f a = g a) -> 'D_v f a = 'D_v g a.
 Proof.
+case: (eqVneq v 0)=> [-> _ | ].
+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 near_eq_is_derive (R : numFieldType) (V W : normedModType R)
-    (f g : V -> W) (a v : V) (df : W) : v != 0 ->
+    (f g : V -> W) (a v : V) (df : W) :
   (\near a, f a = g a) -> is_derive a v f df -> is_derive a v g df.
 Proof.
-move=> v0 fg [fav <-]; rewrite (near_eq_derive v0 fg).
+move=> fg [fav <-]; rewrite (near_eq_derive _ fg).
 by apply: DeriveDef => //; exact: near_eq_derivable fav.
 Qed.
 
+Section Derive_max.
+Context {K : realType} {V W : normedModType K}.
+Implicit Types f g : V -> K^o.
+Implicit Type x : V.
+
+Fact der_max f g x v :
+  f x <> g x -> derivable f x v -> derivable g x v ->
+  {for x, continuous f} -> {for x, continuous g} ->
+  (fun h => 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 fx_neq_gx.
+  move: (fx_neq_gx) => /eqP.
+  rewrite neq_lt => /orP[fg|gf].
+    move: fg fx_neq_gx.
+    by apply:wlg.
+  move=> df dg cf cg.
+  move: dg df cg cf.
+  rewrite fun_maxC ltNge if_neg le_eqVlt.
+  move: fx_neq_gx => /nesym/[dup] fx_neq_gx /eqP/negPf -> /=.
+  by apply:(wlg g f).
+move=> fx_lt_gx fg_neq df dg cf cg.
+case: ifPn => fg /=.
+  rewrite /Num.max fg => t Ht.
+  apply:(@near_eq_cvg _ _ _ _ (fun h => h^-1 *: (g (h *: v + x) - g x))).
+    near=> h.
+    rewrite ifT // -subr_lt0 (_ : f _ - _ = ((f - g) \o shift x) (h *: v)) //.
+    near: h.
+    have Hf : forall f : V -> K^o,
+    continuous_at x f -> f (shift x (x0 *: v)) @[x0 --> nbhs 0^'] --> f x.
+      move=> f' cf'.
+      apply:cvg_comp; last by apply:cf'.
+      rewrite -[in nbhs x](add0r x).
+      apply:cvgD; last by apply:cvg_cst.
+      rewrite -(scale0r v).
+      apply:cvgZ; last by apply:cvg_cst.
+      by apply:nbhs_dnbhs.
+    apply/cvgr_lt; last by move: fg; rewrite -subr_lt0; apply.
+    by apply:cvgB; apply:Hf.
+  by apply:dg.
+exfalso.
+by apply: (negP fg).
+Unshelve.
+end_near.
+Qed.
+
+Lemma derivable_max f g x v :
+  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.
+Qed.
+
+Lemma derive_maxl f g x v : f x > g x ->
+  {for x, continuous f} -> {for x, continuous g} ->
+  'D_v (f \max g) x = 'D_v f x.
+Proof.
+case: (boolP (v == 0)) => [/eqP -> //= gx_fx cf cg | v0].
+  by rewrite !derive0.
+move=> fg cf cg; 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 derive_maxr f g x v : 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 derivable_min f g x v :
+  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.
+case: (boolP (v == 0)) => [/eqP -> /= _ _ _ _ _| v0].
+  by apply/derivable0.
+rewrite min_fun_to_max=> fx_gx df dg cf cg.
+apply/derivableB; [by apply/(derivableD df dg) | by apply/derivable_max].
+Qed.
+
+Lemma derive_minr f g x v : f x > g x ->
+  {for x, continuous f} -> {for x, continuous g} ->
+  'D_v (f \min g) x = 'D_v g x.
+Proof.
+case: (boolP (v == 0)) => [/eqP -> //= gx_fx cf cg | v0].
+  by rewrite !derive0.
+move=> fg cf cg; 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 derive_minl f g x v : 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 derive1N {R : realFieldType} (f : R -> R) (x : R) :
   derivable f x 1 -> (- f)^`() x = (- f^`()%classic x).
 Proof. by move=> fx; rewrite !derive1E deriveN. Qed.

theories/exp.v

@@ -1088,9 +1088,11 @@ apply: (@cvg_comp _ _ _ _ _ _ (@ninfty_nbhs R)).
 exact/cvgNy_compNP/cvgr_expR.
 Unshelve. end_near. Qed.
 
-Lemma derivable_powR v x : v != 0 ->
+Lemma derivable_powR v x :
   {in `]0, +oo[, forall a, derivable (powR ^~ x) a v}.
 Proof.
+case: (eqVneq v 0)=> [-> y _| ].
+by apply/derivable0.
 move=> v0 a; rewrite in_itv/= andbT => a0.
 apply: (@near_eq_derivable _ _ _ (fun a' => expR (x * ln a'))) => //.
   by near=> b; rewrite /powR gt_eqF//; near: b; exact: lt_nbhsr.