From 914a1b78c3701d75e8827196c2d8abaa142d54d6 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 22 Jan 2026 00:14:47 +0900
Subject: [PATCH] derive_mx

---
 theories/derive.v | 89 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 89 insertions(+)

diff --git a/theories/derive.v b/theories/derive.v
index 440a1497e..0f8c60a1d 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -2125,3 +2125,92 @@ exact/derivable1_diffP/derivable_horner.
 Qed.
 
 End derive_horner.
+
+Section pointwise_derivable.
+Context {R : realFieldType} {V W : normedModType R} {m n : nat}.
+Implicit Types M : V -> 'M[R]_(m, n).
+
+Definition derivable_mx M t v :=
+  forall i j, derivable (fun x => M x i j) t v.
+
+(* NB: from robot-rocq *)
+Lemma derivable_mxP M t v : derivable_mx M t v <-> derivable M t v.
+Proof.
+split; rewrite /derivable_mx /derivable.
+- move=> H.
+  apply/cvg_ex => /=.
+  pose l := \matrix_(i < m, j < n) sval (cid ((cvg_ex _).1 (H i j))).
+  exists l.
+  apply/cvgrPdist_le => /= e e0.
+  near=> x.
+  rewrite /Num.Def.normr/= mx_normrE.
+    apply: (bigmax_le _ (ltW e0)) => /= i _.
+  rewrite !mxE/=.
+  move: i.
+  near: x.
+  apply: filter_forall => /= i.
+  exact: ((@cvgrPdist_le _ _ _ _ (dnbhs_filter 0) _ _).1
+    (svalP (cid ((cvg_ex _).1 (H i.1 i.2)))) _ e0).
+- move=> /cvg_ex[/= l Hl] i j.
+  apply/cvg_ex; exists (l i j).
+  apply/cvgrPdist_le => /= e e0.
+  move/cvgrPdist_le : Hl => /(_ _ e0)[/= r r0] H.
+  near=> x.
+  apply: le_trans; last first.
+    apply: (H x).
+    rewrite /ball_/=.
+    rewrite sub0r normrN.
+    near: x.
+    exact: dnbhs0_lt.
+    near: x.
+    exact: nbhs_dnbhs_neq.
+  rewrite [leRHS]/Num.Def.normr/= mx_normrE.
+  apply: le_trans; last exact: le_bigmax.
+  by rewrite /= !mxE.
+Unshelve. all: by end_near. Qed.
+
+End pointwise_derivable.
+
+Section pointwise_derive.
+Local Open Scope classical_set_scope.
+Context {R : realFieldType} {V W : normedModType R} .
+
+(* NB: from robot-rocq *)
+Lemma derive_mx {m n : nat} (M : V -> 'M[R]_(m, n)) t v :
+  derivable M t v ->
+  'D_v M t = \matrix_(i < m, j < n) 'D_v (fun t => M t i j) t.
+Proof.
+move=> /cvg_ex[/= l Hl]; apply/cvg_lim => //=.
+apply/cvgrPdist_le => /= e e0.
+move/cvgrPdist_le : (Hl) => /(_ (e / 2)).
+rewrite divr_gt0// => /(_ isT)[d /= d0 dle].
+near=> x.
+rewrite [in leLHS]/Num.Def.normr/= mx_normrE.
+apply/(bigmax_le _ (ltW e0)) => -[/= i j] _.
+rewrite [in leLHS]mxE/= [X in _ + X]mxE -[X in X - _](subrK (l i j)).
+rewrite -(addrA (_ - _)) (le_trans (ler_normD _ _))// (splitr e) lerD//.
+- rewrite mxE.
+  suff : (h^-1 *: (M (h *: v + t) i j - M t i j)) @[h --> 0^'] --> l i j.
+    move/cvg_lim => /=; rewrite /derive /= => ->//.
+    by rewrite subrr normr0 divr_ge0// ltW.
+  apply/cvgrPdist_le => /= r r0.
+  move/cvgrPdist_le : Hl => /(_ r r0)[/= s s0] sr.
+  near=> y.
+  have : `|l - y^-1 *: (M (y *: v + t) - M t)| <= r.
+    rewrite sr//=; last by near: y; exact: nbhs_dnbhs_neq.
+    by rewrite sub0r normrN; near: y; exact: dnbhs0_lt.
+  apply: le_trans.
+  rewrite [in leRHS]/Num.Def.normr/= mx_normrE.
+  by under eq_bigr do rewrite !mxE; exact: (le_bigmax _ _ (i, j)).
+- rewrite mxE.
+  have : `|l - x^-1 *: (M (x *: v + t) - M t)| <= e / 2.
+    apply: dle => //=; last by near: x; exact: nbhs_dnbhs_neq.
+    by rewrite sub0r normrN; near: x; exact: dnbhs0_lt.
+  apply: le_trans.
+  rewrite [in leRHS]/Num.Def.normr/= mx_normrE/=.
+  under eq_bigr do rewrite !mxE.
+  apply: le_trans; last exact: le_bigmax.
+  by rewrite !mxE.
+Unshelve. all: by end_near. Qed.
+
+End pointwise_derive.