differentiable rsubmx/lsubmx lemmas + derive_sqrt (#1801)

* derive_sqrt

* rsubmx and lsubmx diff lemmas

---------

Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>

Author: yosakaon

CHANGELOG_UNRELEASED.md

@@ -109,6 +109,11 @@
 - in `order_topology.v`:
   + structures `POrderedNbhs`, `POrderedTopological`, `POrderedUniform`, `POrderedPseudoMetric`,
     `POrderedPointedTopological`
+- in `num_topology.v`:
+  + lemmas `continuous_rsubmx`, `continuous_lsubmx`
+
+- in `derive.v`:
+  + lemmas `differentiable_rsubmx`, `differentiable_lsubmx`
 
 ### Changed
 

theories/derive.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval poly.
 From mathcomp Require Import sesquilinear.
@@ -760,6 +760,14 @@ move=> dfx dgfx; apply: DiffDef; first exact: differentiable_comp.
 by rewrite diff_comp // !diff_val.
 Qed.
 
+Lemma differentiable_rsubmx m {n1 n2} v :
+  differentiable (rsubmx : 'M[R]_(m, n1 + n2) -> 'M[R]_(m, n2)) v.
+Proof. exact/linear_differentiable/continuous_rsubmx. Qed.
+
+Lemma differentiable_lsubmx m {n1 n2} v :
+  differentiable (lsubmx : 'M[R]_(m, n1 + n2) -> 'M[R]_(m, n1)) v.
+Proof. exact/linear_differentiable/continuous_lsubmx. 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/normedtype_theory/matrix_normedtype.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum matrix interval.
 From mathcomp Require Import boolp classical_sets interval_inference reals.

theories/realfun.v

@@ -1880,6 +1880,10 @@ rewrite -[x]sqrtK//; apply: (@is_derive_inverse _ (fun x => x ^+ 2)).
 - by rewrite mulf_neq0// gt_eqF// sqrtr_gt0 exprn_gt0// sqrtr_gt0.
 Unshelve. all: by end_near. Qed.
 
+Lemma derive_sqrt {K : realType} (r : K) : 0 < r ->
+  'D_1 Num.sqrt r = (2 * Num.sqrt r)^-1.
+Proof. by move=> r0; apply: derive_val; exact: is_derive1_sqrt. Qed.
+
 #[global] Hint Extern 0 (is_derive _ _ (fun _ => (_ _)^-1) _) =>
   (eapply is_deriveV; first by []) : typeclass_instances.
 

theories/topology_theory/matrix_topology.v

@@ -1,8 +1,9 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra finmap all_classical.
 From mathcomp Require Import interval_inference topology_structure.
 From mathcomp Require Import uniform_structure pseudometric_structure.
+
 (**md**************************************************************************)
 (* # Matrix topology                                                          *)
 (* ```                                                                        *)

theories/topology_theory/num_topology.v

@@ -3,13 +3,13 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra all_classical.
 From mathcomp Require Import interval_inference reals topology_structure.
 From mathcomp Require Import uniform_structure pseudometric_structure.
-From mathcomp Require Import order_topology.
+From mathcomp Require Import order_topology matrix_topology.
 
 (**md**************************************************************************)
 (* # Topological notions for numerical types                                  *)
 (*                                                                            *)
 (* We endow `numFieldType` with the types of topological notions (accessible  *)
-(* with `Import numFieldTopology.Exports).                                    *)
+(* with `Import numFieldTopology.Exports`).                                   *)
 (*                                                                            *)
 (******************************************************************************)
 
@@ -378,3 +378,19 @@ have inj_nat_of_rat : injective nat_of_rat.
   exact/bij_inj.
 by exists (nat_of_rat \o f) => i j Di Dj /inj_nat_of_rat/inj_f; exact.
 Qed.
+
+Lemma continuous_rsubmx {R : numFieldType} m {n1 n2} :
+  continuous (rsubmx : 'M[R]_(m, n1 + n2) -> 'M[R]_(m, n2)).
+Proof.
+move=> u A /nbhs_ballP[e /= e0 eA].
+apply/nbhs_ballP; exists e => //= v [_ uv]; apply: eA; split => // i j.
+by apply: (le_lt_trans _ (uv i (rshift n1 j))); rewrite !mxE.
+Qed.
+
+Lemma continuous_lsubmx {R : numFieldType} m {n1 n2} :
+  continuous (lsubmx : 'M[R]_(m, n1 + n2) -> 'M[R]_(m, n1)).
+Proof.
+move=> u A /nbhs_ballP[e /= e0 eA].
+apply/nbhs_ballP; exists e => //= v [_ uv]; apply: eA; split => // i j.
+by apply: (le_lt_trans _ (uv i (lshift n2 j))); rewrite !mxE.
+Qed.