differentiable rsubmx/lsubmx lemmas + derive_sqrt

theories/derive.v

@@ -693,6 +693,45 @@ have @f : {linear 'M[R]_(m, n) -> R}.
 rewrite (_ : (fun _ => _) = f) //; exact/linear_differentiable/coord_continuous.
 Qed.
 
+Lemma differentiable_rsubmx0 {n1 n2} t :
+  differentiable (@rsubmx R 1 n1 n2) t.
+Proof.
+have lin_rsubmx : linear (@rsubmx R 1 n1 n2).
+  move=> a b c.
+  by rewrite linearD//= linearZ.
+pose build_lin_rsubmx := GRing.isLinear.Build _ _ _ _ _ lin_rsubmx.
+pose Rsubmx : {linear 'rV[R^o]_(n1 + n2) -> 'rV[R^o]_n2} := HB.pack (@rsubmx R _ _ _) build_lin_rsubmx.
+apply: (@linear_differentiable _ _ _ _).
+move=> /= u A /=.
+move/nbhs_ballP=> [e /= e0 eA].
+apply/nbhs_ballP; exists e => //= v [? uv].
+apply: eA; split => //.
+(* TODO: lemma *)
+move: uv; rewrite /ball/= /mx_ball/ball /= => uv i j.
+apply: (le_lt_trans _ (uv i (rshift n1 j))).
+by rewrite !mxE.
+Qed.
+
+Lemma differentiable_lsubmx0{n1 n2} t :
+  differentiable (@lsubmx R 1 n1 n2) t.
+Proof.
+have lin_lsubmx : linear (@lsubmx R 1 n1 n2).
+  move=> a b c.
+  by rewrite linearD//= linearZ.
+pose build_lin_lsubmx := GRing.isLinear.Build _ _ _ _ _ lin_lsubmx.
+pose Lsubmx : {linear 'rV[R^o]_(n1 + n2) -> 'rV[R^o]_n1} :=
+  HB.pack (@lsubmx R _ _ _) build_lin_lsubmx.
+apply: (@linear_differentiable _ _ _ _).
+move=> /= u A /=.
+move/nbhs_ballP=> [e /= e0 eA].
+apply/nbhs_ballP; exists e => //= v [? uv].
+apply: eA; split => //.
+(* TODO: lemma *)
+move: uv; rewrite /ball/= /mx_ball/ball /= => uv i j.
+apply: (le_lt_trans _ (uv i (lshift n2 j))).
+by rewrite !mxE.
+Qed.
+
 Lemma linear_lipschitz (V' W' : normedModType R) (f : {linear V' -> W'}) :
   continuous f -> exists2 k, k > 0 & forall x, `|f x| <= k * `|x|.
 Proof.
@@ -760,6 +799,26 @@ move=> dfx dgfx; apply: DiffDef; first exact: differentiable_comp.
 by rewrite diff_comp // !diff_val.
 Qed.
 
+Lemma differentiable_rsubmx {n1 n2}
+    (f : V -> 'rV[R]_(n1 + n2)) t :
+  (forall x, differentiable f x) ->
+  differentiable (fun x => rsubmx (f x)) t.
+Proof.
+move=> /= => df1.
+apply: differentiable_comp => //.
+exact: differentiable_rsubmx0.
+Qed.
+
+Lemma differentiable_lsubmx {n1 n2}
+    (f : V -> 'rV[R]_(n1 + n2)) t :
+  (forall x, differentiable f x) ->
+  differentiable (fun x => lsubmx (f x)) t.
+Proof.
+move=> /= => df1.
+apply: differentiable_comp => //.
+exact: differentiable_lsubmx0.
+Qed.
+
 Lemma bilinear_schwarz (U V' W' : normedModType R)
   (f : {bilinear U -> V' -> W'}) : continuous (fun p => f p.1 p.2) ->
   exists2 k, k > 0 & forall u v, `|f u v| <= k * `|u| * `|v|.

theories/realfun.v

@@ -1914,7 +1914,16 @@ rewrite -[x]sqrtK//; apply: (@is_derive_inverse _ (fun x => x ^+ 2)).
 - rewrite !sqrtK//; split; first exact: exprn_derivable.
   by rewrite exp_derive expr1 scaler1.
 - by rewrite mulf_neq0// gt_eqF// sqrtr_gt0 exprn_gt0// sqrtr_gt0.
-Unshelve. all: by end_near. Qed.
+  Unshelve. all: by end_near. Qed.
+
+Lemma derive_sqrt {K : realType} (r : K) : 0 < r ->
+   (Num.sqrt^`())%classic r = (2 * Num.sqrt r)^-1 :> K.
+Proof.
+move=> r0.
+rewrite derive1E.
+apply: derive_val.
+exact: is_derive1_sqrt.
+Qed.
 
 #[global] Hint Extern 0 (is_derive _ _ (fun _ => (_ _)^-1) _) =>
   (eapply is_deriveV; first by []) : typeclass_instances.