matrix topology for all dimensions (#1742)

* redefine mx_ball, NormedModule for matrices for all dimensions

* fix convention; generalize lemma mx_normZ

Author: zhou31416

CHANGELOG_UNRELEASED.md

@@ -324,6 +324,9 @@
   + definition `poisson_pmf`, lemmas `poisson_pmf_ge0`, `measurable_poisson_pmf`,
   + definition `poisson_prob`
 
+- in `matrix_topology.v`:
+  + definition `mx_ball`
+
 ### Renamed
 
 - in `reals.v`:
@@ -367,6 +370,11 @@
   + generalized from `numDomainType` to `pzRingType`:
     + definition `onem`, lemmas `onme0`, `onem1`, `add_onemK`, `onemD`, `onemMr`, `onemM`
 
+- in `matrix_normedtype.v`:
+  + lemmas `rV_compact`, `mx_norm_ball`, `bounded_closed_compact`,
+    `mx_normZ`
+  + example `matrix_triangle`
+
 ### Deprecated
 
 ### Removed

theories/normedtype_theory/matrix_normedtype.v

@@ -37,10 +37,11 @@ Lemma coord_continuous {K : numFieldType} m n i j :
   continuous (fun M : 'M[K]_(m, n) => M i j).
 Proof.
 move=> /= M s /= /(nbhs_ballP (M i j)) [e e0 es].
-apply/nbhs_ballP; exists e => //= N MN; exact/es/MN.
+by apply/nbhs_ballP; exists e => //= N [_ MN]; exact/es/MN.
 Qed.
 
-Lemma rV_compact (T : ptopologicalType) n (A : 'I_n.+1 -> set T) :
+#[local]Lemma rV_compact_nondegenerate (T : ptopologicalType) n
+    (A : 'I_n.+1 -> set T) :
   (forall i, compact (A i)) ->
   compact [ set v : 'rV[T]_n.+1 | forall i, A i (v ord0 i)].
 Proof.
@@ -97,6 +98,17 @@ have GC : G [set g | C (\row_j g j)] by exists C.
 by have [g []] := clGf _ _ GC f_D; exists (\row_j (g j : T)).
 Qed.
 
+Lemma rV_compact (T : ptopologicalType) n (A : 'I_n -> set T) :
+  (forall i, compact (A i)) ->
+  compact [ set v : 'rV[T]_n | forall i, A i (v ord0 i)].
+Proof.
+case: n A => [A _ | ]; last exact: rV_compact_nondegenerate.
+have P0 : #|{: 'I_1 * 'I_0}| = 0 by rewrite card_prod/= !card_ord muln0.
+pose v0 := Matrix (ffun0 P0 : {ffun 'I_1 * 'I_0 -> T}).
+rewrite (_ : mkset _ = [set v0]); first exact: compact_set1.
+by rewrite predeqE => x /=; split => [ _ | _ []//]; apply/rowP => -[].
+Qed.
+
 Section mx_norm.
 Variables (K : numDomainType) (m n : nat).
 Implicit Types x y : 'M[K]_(m, n).
@@ -177,7 +189,7 @@ HB.instance Definition _ (K : numDomainType) (m n : nat) :=
 Section example_of_sharing.
 Variables (K : numDomainType).
 
-Example matrix_triangle m n (M N : 'M[K]_(m.+1, n.+1)) :
+Example matrix_triangle m n (M N : 'M[K]_(m, n)) :
   `|M + N| <= `|M| + `|N|.
 Proof. exact: ler_normD. Qed.
 
@@ -189,57 +201,57 @@ End example_of_sharing.
 Section matrix_pseudoMetricNormedZmod.
 Variables (K : numFieldType) (m n : nat).
 
-Local Lemma ball_gt0 (x y : 'M[K]_(m.+1, n.+1)) e : ball x e y -> 0 < e.
-Proof. by move/(_ ord0 ord0); apply: le_lt_trans. Qed.
+Local Lemma ball_gt0 (x y : 'M[K]_(m, n)) e : ball x e y -> 0 < e.
+Proof. by case. Qed.
 
-Lemma mx_norm_ball : @ball _ 'M[K]_(m.+1, n.+1) = ball_ (fun x => `| x |).
+Lemma mx_norm_ball : @ball _ 'M[K]_(m, n) = ball_ (fun x => `| x |).
 Proof.
-rewrite /normr /ball_ predeq3E => x e y /=; rewrite mx_normE; split => xey.
-- have e_gt0 : 0 < e := ball_gt0 xey.
-  move: e_gt0 (e_gt0) xey => /ltW/nonnegP[{}e] e_gt0 xey.
+rewrite /normr /ball_ predeq3E => x e y/= /[!mx_normE]; split=> [[]|xey].
+- move=> /[dup] => /ltW/nonnegP[{}e] e_gt0 xey.
   rewrite num_lt; apply/bigmax_ltP => /=.
   by rewrite -num_lt /=; split => // -[? ?] _; rewrite !mxE; exact: xey.
 - have e_gt0 : 0 < e by rewrite (le_lt_trans _ xey).
   move: e_gt0 (e_gt0) xey => /ltW/nonnegP[{}e] e_gt0.
-  move=> /(bigmax_ltP _ _ _ (fun _ => _%:itv)) /= [e0 xey] i j.
+  move=> /(bigmax_ltP _ _ _ (fun=> _%:itv)) /= [e0 xey].
+  split=> // i j.
   by move: (xey (i, j)); rewrite !mxE; exact.
 Qed.
 
 HB.instance Definition _ :=
-  NormedZmod_PseudoMetric_eq.Build K 'M[K]_(m.+1, n.+1) mx_norm_ball.
+  NormedZmod_PseudoMetric_eq.Build K 'M[K]_(m, n) mx_norm_ball.
 
 End matrix_pseudoMetricNormedZmod.
 
-Lemma bounded_closed_compact (R : realType) n (A : set 'rV[R]_n.+1) :
+Lemma bounded_closed_compact (R : realType) n (A : set 'rV[R]_n) :
   bounded_set A -> closed A -> compact A.
 Proof.
 move=> [M [Mreal normAltM]] Acl.
 have Mnco : compact
-  [set v : 'rV[R]_n.+1 | forall i, v ord0 i \in `[(- (M + 1)), (M + 1)]].
-  apply: (@rV_compact _  _ (fun _ => `[(- (M + 1)), (M + 1)]%classic)).
+    [set v : 'rV[R]_n | forall i, v ord0 i \in `[(- (M + 1)), (M + 1)]].
+  apply: (@rV_compact _  _ (fun=> `[(- (M + 1)), (M + 1)]%classic)).
   by move=> _; apply: segment_compact.
 apply: subclosed_compact Acl Mnco _ => v /normAltM normvleM i.
 suff : `|v ord0 i : R| <= M + 1 by rewrite ler_norml.
 apply: le_trans (normvleM _ _); last by rewrite ltrDl.
-have /mapP[j Hj ->] : `|v ord0 i| \in [seq `|v x.1 x.2| | x : 'I_1 * 'I_n.+1].
+have /mapP[j Hj ->] : `|v ord0 i| \in [seq `|v x.1 x.2| | x : 'I_1 * 'I_n].
   by apply/mapP; exists (ord0, i) => //=; rewrite mem_enum.
 by rewrite [leRHS]/normr /= mx_normrE; apply/bigmax_geP; right => /=; exists j.
 Qed.
 
 Section matrix_NormedModule.
-Variables (K : numFieldType) (m n : nat).
 
-Lemma mx_normZ (l : K) (x : 'M[K]_(m.+1, n.+1)) : `| l *: x | = `| l | * `| x |.
+Lemma mx_normZ (K : numDomainType) m n (l : K) (x : 'M[K]_(m, n)) :
+  `| l *: x | = `| l | * `| x |.
 Proof.
 rewrite {1 3}/normr /= !mx_normE
- (eq_bigr (fun i => (`|l| * `|x i.1 i.2|)%:nng)); last first.
+    (eq_bigr (fun i => (`|l| * `|x i.1 i.2|)%:nng)); last first.
   by move=> i _; rewrite mxE //=; apply/eqP; rewrite -num_eq /= normrM.
 elim/big_ind2 : _ => // [|a b c d bE dE]; first by rewrite mulr0.
 by rewrite !num_max bE dE maxr_pMr.
 Qed.
 
-HB.instance Definition _ :=
-  PseudoMetricNormedZmod_Lmodule_isNormedModule.Build K 'M[K]_(m.+1, n.+1)
-    mx_normZ.
+HB.instance Definition _ (K : numFieldType) m n :=
+  PseudoMetricNormedZmod_Lmodule_isNormedModule.Build K 'M[K]_(m, n)
+    (@mx_normZ K m n).
 
 End matrix_NormedModule.

theories/topology_theory/matrix_topology.v

@@ -6,8 +6,9 @@ From mathcomp Require Import uniform_structure pseudometric_structure.
 (**md**************************************************************************)
 (* # Matrix topology                                                          *)
 (* ```                                                                        *)
-(*                  mx_ent m n A == entourages for the m x n matrices         *)
-(*                 mx_ball m n A == balls for the m x n matrices              *)
+(*              @mx_ent m n T == entourages for the m x n matrices with       *)
+(*                               coefficients of type T                       *)
+(*                  mx_ball A == balls for the matrix A                       *)
 (* ```                                                                        *)
 (* Matrices `'M[T]_(m, n)` are endowed with the structures of:                *)
 (* - topology                                                                 *)
@@ -183,30 +184,32 @@ Section matrix_PseudoMetric.
 Variables (m n : nat) (R : numDomainType) (T : pseudoMetricType R).
 Implicit Types (x y : 'M[T]_(m, n)) (e : R).
 
-Definition mx_ball x e y := forall i j, ball (x i j) e (y i j).
+Definition mx_ball x e y := 0 < e /\ forall i j, ball (x i j) e (y i j).
 
 Local Lemma mx_ball_center x e : 0 < e -> mx_ball x e x.
-Proof. by move=> ? ? ?; exact: ballxx. Qed.
+Proof. by move=> ?; split=> [//|? ?]; exact: ballxx. Qed.
 
 Local Lemma mx_ball_sym x y e : mx_ball x e y -> mx_ball y e x.
-Proof. by move=> xe_y ? ?; apply/ball_sym/xe_y. Qed.
+Proof. by move=> [e0 xe_y]; split=>[//|? ?]; apply/ball_sym/xe_y. Qed.
 
 Local Lemma mx_ball_triangle x y z e1 e2 :
   mx_ball x e1 y -> mx_ball y e2 z -> mx_ball x (e1 + e2) z.
 Proof.
-by move=> xe1_y ye2_z ??; apply: ball_triangle; [exact: xe1_y|exact: ye2_z].
+move=> [e10 xe1_y] [e20 ye2_z]; split; first exact: addr_gt0.
+by move=> i j; apply: ball_triangle; [exact: xe1_y|exact: ye2_z].
 Qed.
 
 Local Lemma mx_entourage : entourage = entourage_ mx_ball.
 Proof.
 rewrite predeqE=> A; split; last first.
   move=> [_/posnumP[e] sbeA].
-  exists (fun _ _ => [set xy | ball xy.1 e%:num xy.2]) => //= _ _.
+  exists (fun _ _ => [set xy | ball xy.1 e%:num xy.2]) => //=.
+  by move=> [] ? ? /= P; exact: sbeA.
 move=> [P]; rewrite -entourage_ballE => entP sPA.
 set diag := fun e : {posnum R} => [set xy : T * T | ball xy.1 e%:num xy.2].
 exists (\big[Num.min/1%:pos]_i \big[Num.min/1%:pos]_j xget 1%:pos
   (fun e : {posnum R} => diag e `<=` P i j))%:num => //=.
-move=> MN MN_min; apply: sPA => i j.
+move=> MN/= [] _ MN_min; apply: sPA => i j.
 have /(xgetPex 1%:pos): exists e : {posnum R}, diag e `<=` P i j.
   by have [_/posnumP[e]] := entP i j; exists e.
 apply; apply: le_ball (MN_min i j).
@@ -220,4 +223,3 @@ End matrix_PseudoMetric.
 
 HB.instance Definition _ (R : numFieldType) (T : completePseudoMetricType R)
   (m n : nat) := Uniform_isComplete.Build 'M[T]_(m, n) cauchy_cvg.
-