derive row_mx

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -4,6 +4,9 @@
 
 ### Added
 
+- in `derive.v`:
+  + lemmas `derivable_row_mx`, `derive_row_mx`
+
 ### Changed
 
 ### Renamed

theories/derive.v

@@ -2292,6 +2292,30 @@ Unshelve. all: by end_near. Qed.
 
 End pointwise_derivable.
 
+Section derivable_mx.
+
+Lemma derivable_row_mx {R : realFieldType} {V : normedModType R} {n1 n2 : nat}
+    (f : V -> 'rV[R]_n1) (g : V -> 'rV[R]_n2) t v :
+  (forall x, derivable f x v) -> (forall x, derivable g x v) ->
+  derivable (fun x : V => 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 t.
+have /cvg_ex[/= k Hk] := gv t.
+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.
+
+End derivable_mx.
+
 Section pointwise_derive.
 Local Open Scope classical_set_scope.
 Context {R : realFieldType} {V : normedModType R}.
@@ -2329,3 +2353,32 @@ rewrite (le_trans (ler_normD _ _))// (splitr e) lerD//.
 Unshelve. all: by end_near. Qed.
 
 End pointwise_derive.
+
+Section derive_mx.
+
+Lemma derive_row_mx {R : realFieldType} {V : normedModType R} {n1 n2 : nat}
+     (f : V -> 'rV[R]_n1) (g : V -> 'rV[R]_n2) t v :
+  (forall x, derivable f x v) -> (forall x, derivable g x 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; apply/matrixP => i j.
+rewrite [in LHS]derive_mx ?mxE//=; last first.
+  by apply: derivable_row_mx; [exact: fv|exact: gv].
+do 2 rewrite derive_mx ?mxE//=.
+case: split_ordP => /= j' jj'; rewrite !mxE; congr ('D_v _ t).
+- apply/funext => x; rewrite !mxE; case: split_ordP => [k jE|k].
+  + congr (f x i _).
+    by move: jE; rewrite jj' => /(congr1 val) => /= /val_inj.
+  + rewrite jj' => /(congr1 val)/=.
+    have /[swap] -> := ltn_ord j'.
+    by rewrite ltnNge/= leq_addr.
+- apply/funext => x; rewrite !mxE;  case: split_ordP => [k|k jE].
+  + rewrite jj' => /(congr1 val)/=.
+    have /[swap] <- := ltn_ord k.
+    by rewrite ltnNge/= leq_addr.
+  + congr (g x i _).
+    move: jE; rewrite jj' => /(congr1 val) => /= /eqP.
+    by rewrite eqn_add2l => /eqP /val_inj.
+Qed.
+
+End derive_mx.