derive row_mx (#1866)

* derive row_mx

- with is_derive, is_diff instances

---------

Co-authored-by: Holger Thies <thies.holger.5c@kyoto-u.ac.jp>

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -174,6 +174,20 @@
 - in `ftc.v`:
   + lemma `ge0_integration_by_substitution_shift_itvy`,
     `ge0_integration_by_substitution_shift_itvNy`
+- in `derive.v`:
+  + lemmas `derivable_row_mx`, `derive_row_mx`
+  + instance `is_derive_row_mx`
+
+- in `matrix_normedtype.v`
+  + lemmas `norm_row_mx`, `norm_row_mx0r`, `norm_row_mx0l`, `cvg_row_mx`
+
+- in `unstable.v`:
+  + lemma `sub_row_mx`
+
+- in `derive.v`:
+  + lemmas `eqo_row_mx`, `drow_mx`, `diff_row_mx`,
+    `differentiable_row_mx`
+  + instance `is_diff_row_mx`
 
 - in `functions.v`:
   + lemmas `zerofctE`, `onefctE`

classical/unstable.v

@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint.
-From mathcomp Require Import vector archimedean interval.
+From mathcomp Require Import vector archimedean interval matrix.
 
 (**md**************************************************************************)
 (* # MathComp extra                                                           *)
@@ -53,6 +53,11 @@ Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Theory.
 Local Open Scope ring_scope.
 
+Lemma sub_row_mx {V : zmodType} m n1 n2 (A1 : 'M[V]_(m, n1)) (A2 : 'M[V]_(m, n2))
+    (B1 : 'M[V]_(m, n1)) (B2 : 'M[V]_(m, n2)) :
+  row_mx A1 A2 - row_mx B1 B2 = row_mx (A1 - B1) (A2 - B2).
+Proof. by rewrite opp_row_mx add_row_mx. Qed.
+
 Section IntervalNumDomain.
 Variable R : numDomainType.
 Implicit Types x : R.

theories/derive.v

@@ -377,7 +377,7 @@ Lemma deriveEjacobian m n (f : 'rV[R]_m -> 'rV[R]_n) (a v : 'rV[R]_m) :
 Proof. by move=> /deriveE->; rewrite /jacobian mul_rV_lin1. Qed.
 
 Definition derive1 V (f : R -> V) (a : R) :=
-   lim ((fun h => h^-1 *: (f (h + a) - f a)) @ 0^').
+  lim ((fun h => h^-1 *: (f (h + a) - f a)) @ 0^').
 
 Local Notation "f ^` ()" := (derive1 f).
 
@@ -2330,7 +2330,7 @@ Unshelve. all: by end_near. Qed.
 
 Global Instance is_derive_mx {m n : nat} (M : V -> 'M[R]_(m, n))
     (dM : 'M[R]_(m, n)) (x v : V) :
-  (forall i j, is_derive x v (fun x => M x i j) (dM i j)) ->
+  (forall i j, is_derive x v (fun t => M t i j) (dM i j)) ->
   is_derive x v M dM.
 Proof.
 move=> MdM; apply: DeriveDef; first exact/derivable_mxP.
@@ -2342,7 +2342,7 @@ by have [] := MdM i0 j0.
 Qed.
 
 Fact dmx {m n : nat} (M : V -> 'M[R]_(m, n)) (x : V) :
-  let g := fun x0 : V => (\matrix_(i < m, j < n) 'd M x x0 i j) in
+  let g := fun t : V => (\matrix_(i < m, j < n) 'd M x t i j) in
   differentiable M x ->
   continuous g /\
   M \o shift x = cst (M x) + g +o_ 0 id.
@@ -2357,13 +2357,13 @@ move=> dM Mx; split => [|].
   by apply/matrixP => i j/=; rewrite mxE.
 Qed.
 
-Lemma diffmx {m n : nat} (M : V -> 'M[R]_(m, n)) t :
-  differentiable M t ->
-  'd M (nbhs_filter_on t) =
-  (fun x0 : V => \matrix_(i < m, j < n) 'd M t x0 i j) :> (_ -> _).
+Lemma diffmx {m n : nat} (M : V -> 'M[R]_(m, n)) x :
+  differentiable M x ->
+  'd M (nbhs_filter_on x) =
+  (fun t : V => \matrix_(i < m, j < n) 'd M x t i j) :> (_ -> _).
 Proof.
 move=> dM.
-set g := fun x0 : V => \matrix_(i, j) 'd M t x0 i j.
+set g := fun t : V => \matrix_(i, j) '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.
@@ -2379,16 +2379,14 @@ Local Open Scope classical_set_scope.
 Context {R : realFieldType}.
 
 Global Instance is_diff_mx {m n : nat} (M dM : R -> 'M[R]_(m, n)) (x : R) :
-  (forall i j, is_diff x (fun x => M x i j) (fun x => dM x i j)) ->
+  (forall i j, is_diff x (fun t => M t i j) (fun t => dM t i j)) ->
   is_diff x M dM.
 Proof.
 move=> /= MdM.
-have diffM : differentiable M (nbhs_filter_on x).
+have diffMx : differentiable M (nbhs_filter_on x).
   apply/derivable1_diffP; apply/derivable_mxP => i j.
-  by have [/(@derivable1_diffP _ _ (fun x0 => M x0 i j) x)] := MdM i j.
-have diffMx i j : differentiable (fun x0 : R => M x0 i j) x.
-  by have [/=] := MdM i j.
-apply: DiffDef; first exact: diffM.
+  by have [/(@derivable1_diffP _ _ (fun t => 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.
@@ -2401,3 +2399,111 @@ by have [/diff_derivable-/(_ v)] := MdM i0 j0.
 Qed.
 
 End Ris_diff_mx.
+
+Section derivable_derive_row_mx.
+Context {R : realFieldType} {V : normedModType R} {n1 n2 : nat}.
+Implicit Types (f : V -> 'rV[R]_n1) (g : V -> 'rV[R]_n2).
+
+Lemma derivable_row_mx f g t v : derivable f t v -> derivable g t v ->
+  derivable (fun x => 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 derive_row_mx f g t v : derivable f t v -> derivable g t v ->
+  'D_v (fun x => 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_row_mx f A g B x v :
+  is_derive x v f A -> is_derive x v g B ->
+  is_derive x v (fun t => 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 eqo_row_mx (K : realFieldType) {m n1 n2 : nat} (F : filter_on K)
+  (A1 : K -> 'M[K]_(m, n1)) (A2 : K -> 'M[K]_(m, n2)) (f : K -> K) :
+  (fun t => 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 {R : realFieldType} {n1 n2 : nat}.
+Implicit Types (M dM : R -> 'rV[R]_n1) (N dN : R -> 'rV[R]_n2) (x t : R).
+
+Fact drow_mx M N x (f : R -> R) : differentiable M x -> differentiable N x ->
+  continuous (fun y => row_mx ('d M x y) ('d N x y)) /\
+  (fun y => row_mx (M y) (N y)) \o shift x = cst (row_mx (M x) (N x)) +
+  (fun y => 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 h e, 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 y => row_mx (_ y) (_ y)) y) eqo_row_mx.
+Qed.
+
+Lemma diff_row_mx M N x : differentiable M x -> differentiable N x ->
+  'd (fun y => row_mx (M y) (N y)) x =
+  (fun y => row_mx ('d M x y) ('d N x y)) :> (R -> 'rV[R]_(n1 + n2)).
+Proof.
+move=> df dg.
+pose d y := 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_row_mx M N x : differentiable M x -> differentiable N x ->
+  differentiable (fun t => 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_row_mx M dM N dN x :
+  is_diff x M dM -> is_diff x N dN ->
+  is_diff x (fun t => row_mx (M t) (N t)) (fun t => 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.

theories/normedtype_theory/matrix_normedtype.v

@@ -2,7 +2,9 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum matrix.
 From mathcomp Require Import interval interval_inference.
-From mathcomp Require Import boolp classical_sets reals topology.
+#[warning="-warn-library-file-internal-analysis"]
+From mathcomp Require Import unstable.
+From mathcomp Require Import boolp contra classical_sets reals topology.
 From mathcomp Require Import prodnormedzmodule tvs pseudometric_normed_Zmodule.
 From mathcomp Require Import normed_module.
 
@@ -274,3 +276,37 @@ split => [cf x|cf i j v].
   apply: le_trans (le_bigmax _ _ (i, j)).
   by rewrite !mxE.
 Unshelve. all: by end_near. Qed.
+
+Section norm_row_mx.
+Context {K : realDomainType} {m n1 n2 : nat}.
+Implicit Types (M : 'M[K]_(m, n1)) (N : 'M[K]_(m, n2)).
+
+Lemma norm_row_mx M N : `|row_mx M N| = Num.max `|M| `|N|.
+Proof.
+rewrite /Num.norm/= !mx_normrE.
+rewrite -!(pair_bigA_idem _ (fun i j => `|_ i j|))/= ?maxxx//.
+rewrite -big_split_idem/= ?maxxx//; apply: eq_bigr => i _.
+rewrite big_split_ord_idem/= ?maxxx//.
+   by move=> a; rewrite maxC.
+by congr maxr; apply: eq_bigr => j _; [rewrite row_mxEl|rewrite row_mxEr].
+Qed.
+
+Lemma norm_row_mx0r M : `|row_mx M (0 : 'M_(m, n2))| = `|M|.
+Proof. by rewrite norm_row_mx normr0; exact/max_idPl. Qed.
+
+Lemma norm_row_mx0l N : `|row_mx (0 : 'M_(m, n1)) N| = `|N|.
+Proof. by rewrite norm_row_mx normr0; exact/max_idPr. Qed.
+
+End norm_row_mx.
+
+Lemma cvg_row_mx {T : realFieldType} {F : set_system T} {n1 n2 : nat}
+    (G : 'rV[T]_n1) (H : 'rV[T]_n2) : Filter F ->
+  forall (f : T -> 'rV[T]_n1) (g : T -> 'rV[T]_n2),
+  f x @[x --> F] --> G -> g x @[x --> F] --> H ->
+  row_mx (f x) (g x) @[x --> F] --> row_mx G H.
+Proof.
+move=> FF M N cvgM cvgN; apply/cvgrPdist_le => /= e e0; near=> t.
+rewrite sub_row_mx norm_row_mx ge_max; apply/andP; split.
+- by near: t; move/cvgrPdist_le : cvgM => /(_ _ e0).
+- by near: t; move/cvgrPdist_le : cvgN => /(_ _ e0).
+Unshelve. all: by end_near. Qed.