adapt to MC master

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -174,19 +174,16 @@
   + instance `is_derive_row_mx`
 
 - in `matrix_normedtype.v`
-  + lemmas `norm_row_mx`, `norm_row_mx0r`, `norm_row_mx0l`
+  + 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`, `cvg_row_mx`, `drow_mx`, `diff_row_mx`,
+  + lemmas `eqo_row_mx`, `drow_mx`, `diff_row_mx`,
     `differentiable_row_mx`
   + instance `is_diff_row_mx`
 
-- in `unstable.v`:
-  + lemma `big_split_ord_idem`
-
 ### Changed
 
 - moved from `measurable_structure.v` to `classical_sets.v`:

classical/unstable.v

@@ -671,21 +671,3 @@ End Theory.
 Module Import Exports. HB.reexport. End Exports.
 End Norm.
 Export Norm.Exports.
-
-(* NB: big_split_org in bigop.v requires Monoid.law idx,
-   big_split_ord_idem will be made available from MathComp
-   via PR https://github.com/math-comp/math-comp/pull/1608
-   (MathComp 2.7.0) *)
-Lemma big_split_ord_idem [R : Type] [idx : R] (op : SemiGroup.com_law R) m n
-    (P : pred 'I_(m + n)) F :
-  op idx idx = idx ->
-  \big[op/idx]_(i | P i) F i =
-        op (\big[op/idx]_(i | P (lshift n i)) F (lshift n i))
-        (\big[op/idx]_(i | P (rshift m i)) F (rshift m i)).
-Proof.
-move=> opxx.
-rewrite -(big_map (lshift n) P F) -(big_map (@rshift m _) P F).
-rewrite -big_cat_idem//; congr bigop; apply: (inj_map val_inj).
-rewrite map_cat -!map_comp (map_comp (addn m)) /=.
-by rewrite ![index_enum _]unlock unlock !val_ord_enum -iotaDl addn0 iotaD.
-Qed.

theories/derive.v

@@ -2455,19 +2455,6 @@ 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.
 
-(* NB: this could be moved earlier in the file hierarchy *)
-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.
-
 Section is_diff_row_mx.
 Local Open Scope classical_set_scope.
 Context {R : realFieldType} {n1 n2 : nat}.

theories/normedtype_theory/matrix_normedtype.v

@@ -286,7 +286,8 @@ 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//=.
+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.
 
@@ -297,3 +298,15 @@ 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.