Module mathcomp.analysis.topology_theory.matrix_topology
From HB Require Import structures.From mathcomp Require Import boot order algebra finmap all_classical.
From mathcomp Require Import interval_inference topology_structure.
From mathcomp Require Import uniform_structure pseudometric_structure.
# Matrix topology
```
@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
- uniform space
- pseudometric space
- complete uniform space
- complete pseudometric space
Unset SsrOldRewriteGoalsOrder.
Import Order.TTheory GRing.Theory Num.Theory.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Section matrix_Topology.
Variables ( : nat) ( : topologicalType).
Implicit Types M : 'M[T]_(m, n).
Lemma
mx_nbhs_filter
Source code
: ProperFilter (nbhs M).Source code
Proof.
apply: (filter_from_proper (filter_from_filter _ _)) => [|P Q M_P M_Q|P M_P].
- by exists (fun => setT) => ??; apply: filterT.
- exists (fun => P i j `&` Q i j) => [??|mx PQmx]; first exact: filterI.
by split=> i j; have [] := PQmx i j.
- exists (\matrix_(, ) xget (M i j) (P i j)) => i j; rewrite mxE.
by apply: xgetPex; exact: filter_ex (M_P i j).
Qed.
- by exists (fun => setT) => ??; apply: filterT.
- exists (fun => P i j `&` Q i j) => [??|mx PQmx]; first exact: filterI.
by split=> i j; have [] := PQmx i j.
- exists (\matrix_(, ) xget (M i j) (P i j)) => i j; rewrite mxE.
by apply: xgetPex; exact: filter_ex (M_P i j).
Qed.
Lemma
mx_nbhs_singleton
Source code
( : set 'M[T]_(m, n)) : nbhs M A -> A M.Source code
Proof.
Lemma
mx_nbhs_nbhs
Source code
( : set 'M[T]_(m, n)) : nbhs M A -> nbhs M (nbhs^~ A).Source code
Proof.
move=> [P M_P sPA]; exists (fun => (P i j)°).
by move=> ? ?; apply: nbhs_interior.
by move=> ? ?; exists P.
Qed.
by move=> ? ?; apply: nbhs_interior.
by move=> ? ?; exists P.
Qed.
.
instance
Source code
Source code
Definition
Source code
Source code
Nbhs_isNbhsTopological
Source code
.Build 'M[T]_(m, n)Source code
mx_nbhs_filter mx_nbhs_singleton mx_nbhs_nbhs.
End matrix_Topology.
Section matrix_Uniform.
Local Open Scope relation_scope.
Variables ( : nat) ( : uniformType).
Implicit Types A : set ('M[T]_(m, n) * 'M[T]_(m, n)).
Definition
mx_ent
Source code
:= filter_frommx_ent : forall (m n : nat) (T : uniformType), set_system ('M_(m, n) * 'M_(m, n)) mx_ent is not universe polymorphic Arguments mx_ent (m n)%_nat_scope T _ mx_ent is transparent Expands to: Constant mathcomp.analysis.topology_theory.matrix_topology.mx_ent Declared in library mathcomp.analysis.topology_theory.matrix_topology, line 66, characters 11-17
Source code
[set : 'I_m -> 'I_n -> set (T * T) | forall , entourage (P i j)]
(fun => [set : 'M[T]_(m, n) * 'M[T]_(m, n) |
forall , P i j (MN.1 i j, MN.2 i j)]).
Lemma
mx_ent_filter
Source code
: Filter mx_ent.Source code
Proof.
Lemma
mx_ent_refl
Source code
: mx_ent A -> diagonal `<=` A.Source code
Proof.
Lemma
mx_ent_inv
Source code
: mx_ent A -> mx_ent A^-1.Source code
Proof.
move=> [B entB sBA]; exists (fun => (B i j)^-1).
by move=> i j; apply: entourage_inv.
by move=> MN BMN; apply: sBA.
Qed.
by move=> i j; apply: entourage_inv.
by move=> MN BMN; apply: sBA.
Qed.
Lemma
mx_ent_split
Source code
: mx_ent A -> exists2 , mx_ent B & B \; B `<=` A.Source code
Proof.
move=> [B entB sBA].
have Bsplit : forall , exists , entourage C /\ C \; C `<=` B i j.
by move=> ??; apply/exists2P/entourage_split_ex.
exists [set : 'M[T]_(m, n) * 'M[T]_(m, n) |
forall , get [set | entourage C /\ C \; C `<=` B i j]
(MN.1 i j, MN.2 i j)].
by exists (fun => get [set | entourage C /\ C \; C `<=` B i j]).
move=> MN [P CMN1P CPMN2]; apply/sBA => i j.
have /getPex [_] := Bsplit i j; apply; exists (P i j); first exact: CMN1P.
exact: CPMN2.
Qed.
have Bsplit : forall , exists , entourage C /\ C \; C `<=` B i j.
by move=> ??; apply/exists2P/entourage_split_ex.
exists [set : 'M[T]_(m, n) * 'M[T]_(m, n) |
forall , get [set | entourage C /\ C \; C `<=` B i j]
(MN.1 i j, MN.2 i j)].
by exists (fun => get [set | entourage C /\ C \; C `<=` B i j]).
move=> MN [P CMN1P CPMN2]; apply/sBA => i j.
have /getPex [_] := Bsplit i j; apply; exists (P i j); first exact: CMN1P.
exact: CPMN2.
Qed.
Lemma
mx_ent_nbhsE
Source code
: nbhs = nbhs_ mx_ent.Source code
Proof.
rewrite predeq2E => M A; split.
move=> [B]; rewrite -nbhs_entourageE => M_B sBA.
set sB := fun => [set | entourage C /\ xsection C (M i j) `<=` B i j].
have {}M_B : forall , sB i j !=set0 by move=> ??; apply/exists2P/M_B.
exists [set : 'M[T]_(m, n) * 'M[T]_(m, n) | forall ,
get (sB i j) (MN.1 i j, MN.2 i j)].
by exists (fun => get (sB i j)) => // i j; have /getPex [] := M_B i j.
move=> N /xsectionP CMN; apply/sBA => i j; have /getPex [_] := M_B i j; apply.
exact/xsectionP/CMN.
move=> [B [C entC sCB] sBA]; exists (fun => xsection (C i j) (M i j)).
by rewrite -nbhs_entourageE => i j; exists (C i j).
by move=> N CMN; apply/sBA; apply/xsectionP/sCB => ? ?; exact/xsectionP/CMN.
Qed.
move=> [B]; rewrite -nbhs_entourageE => M_B sBA.
set sB := fun => [set | entourage C /\ xsection C (M i j) `<=` B i j].
have {}M_B : forall , sB i j !=set0 by move=> ??; apply/exists2P/M_B.
exists [set : 'M[T]_(m, n) * 'M[T]_(m, n) | forall ,
get (sB i j) (MN.1 i j, MN.2 i j)].
by exists (fun => get (sB i j)) => // i j; have /getPex [] := M_B i j.
move=> N /xsectionP CMN; apply/sBA => i j; have /getPex [_] := M_B i j; apply.
exact/xsectionP/CMN.
move=> [B [C entC sCB] sBA]; exists (fun => xsection (C i j) (M i j)).
by rewrite -nbhs_entourageE => i j; exists (C i j).
by move=> N CMN; apply/sBA; apply/xsectionP/sCB => ? ?; exact/xsectionP/CMN.
Qed.
.
instance
Source code
Source code
Definition
Source code
Source code
Nbhs_isUniform
Source code
.Build 'M[T]_(m, n)Source code
mx_ent_filter mx_ent_refl mx_ent_inv mx_ent_split mx_ent_nbhsE.
End matrix_Uniform.
Lemma
cvg_mx_entourageP
Source code
( : puniformType) ( : set_system 'M[T]_(m,n))Source code
( : Filter F) ( : 'M[T]_(m,n)) :
F --> M <->
forall , entourage A -> \forall \near F,
forall , (M i j, (N : 'M[T]_(m,n)) i j) \in A.
Proof.
split.
rewrite filter_fromP => FM A ?.
by apply: (FM (fun => xsection A (M i j))).
move=> FM; apply/cvg_entourageP => A [P entP sPA]; near=> N; apply/xsectionP.
move/subsetP : sPA; apply => /=; near: N; set Q := \bigcap_ P ij.1 ij.2.
apply: filterS (FM Q _).
move=> N QN; rewrite inE/= => i j.
by have := QN i j; rewrite !inE => /(_ (i, j)); exact.
have -> : Q =
\bigcap_( in [set | k \in [fset in predT]%fset]) P ij.1 ij.2.
by rewrite predeqE => t; split=> Qt ij _; apply: Qt => //=; rewrite !inE.
by apply: filter_bigI => ??; apply: entP.
Unshelve. all: by end_near. Qed.
rewrite filter_fromP => FM A ?.
by apply: (FM (fun => xsection A (M i j))).
move=> FM; apply/cvg_entourageP => A [P entP sPA]; near=> N; apply/xsectionP.
move/subsetP : sPA; apply => /=; near: N; set Q := \bigcap_ P ij.1 ij.2.
apply: filterS (FM Q _).
move=> N QN; rewrite inE/= => i j.
by have := QN i j; rewrite !inE => /(_ (i, j)); exact.
have -> : Q =
\bigcap_( in [set | k \in [fset in predT]%fset]) P ij.1 ij.2.
by rewrite predeqE => t; split=> Qt ij _; apply: Qt => //=; rewrite !inE.
by apply: filter_bigI => ??; apply: entP.
Unshelve. all: by end_near. Qed.
Section matrix_PointedTopology.
Variables ( : nat).
.
instance
Source code
Source code
Definition
Source code
(Source code
ptopologicalType
Source code
) := Filtered.on 'M[T]_(m, n).Source code
.
instance
Source code
Source code
Definition
Source code
(Source code
puniformType
Source code
) := Pointed.on 'M[T]_(m, n).Source code
End matrix_PointedTopology.
Section matrix_Complete.
Variables ( : completeType) ( : nat).
Lemma
mx_complete
Source code
( : set_system 'M[T]_(m, n)) :Source code
ProperFilter F -> cauchy F -> cvg F.
Proof.
move=> FF Fc.
have /(_ _ _) /cauchy_cvg /cvg_app_entourageP cvF :
cauchy ((fun : 'M[T]_(m, n) => M _ _) @ F).
move=> i j A /= entA; rewrite near_simpl -near2E near_map2.
by apply: Fc; exists (fun _ _ => A).
apply/cvg_ex.
set Mlim := \matrix_(, ) (lim ((fun : 'M[T]_(m, n) => M i j) @ F) : T).
exists Mlim; apply/cvg_mx_entourageP => A entA; near=> M => i j; near F => M'.
rewrite inE.
apply: subset_split_ent => //; exists (M' i j) => /=.
by near: M'; rewrite mxE; exact: cvF.
move: (i) (j); near: M'; near: M; apply: nearP_dep; apply: Fc.
by exists (fun _ _ => (split_ent A)^-1%relation) => ?? //; apply: entourage_inv.
Unshelve. all: by end_near. Qed.
have /(_ _ _) /cauchy_cvg /cvg_app_entourageP cvF :
cauchy ((fun : 'M[T]_(m, n) => M _ _) @ F).
move=> i j A /= entA; rewrite near_simpl -near2E near_map2.
by apply: Fc; exists (fun _ _ => A).
apply/cvg_ex.
set Mlim := \matrix_(, ) (lim ((fun : 'M[T]_(m, n) => M i j) @ F) : T).
exists Mlim; apply/cvg_mx_entourageP => A entA; near=> M => i j; near F => M'.
rewrite inE.
apply: subset_split_ent => //; exists (M' i j) => /=.
by near: M'; rewrite mxE; exact: cvF.
move: (i) (j); near: M'; near: M; apply: nearP_dep; apply: Fc.
by exists (fun _ _ => (split_ent A)^-1%relation) => ?? //; apply: entourage_inv.
Unshelve. all: by end_near. Qed.
.
instance
Source code
Source code
Definition
Source code
Source code
Uniform_isComplete
Source code
.Build 'M[T]_(m, n) mx_complete.Source code
End matrix_Complete.
Matrices:
Section matrix_PseudoMetric.Variables ( : nat) ( : numDomainType) ( : pseudoMetricType R).
Implicit Types (x y : 'M[T]_(m, n)) (e : R).
Definition
mx_ball
Source code
:= 0 < e /\ forall , ball (x i j) e (y i j).mx_ball : forall (m n : nat) (R : numDomainType) (T : pseudoMetricType R), 'M_(m, n) -> R -> 'M_(m, n) -> Prop mx_ball is not universe polymorphic Arguments mx_ball (m n)%_nat_scope R T (x e y)%_ring_scope mx_ball is transparent Expands to: Constant mathcomp.analysis.topology_theory.matrix_topology.mx_ball Declared in library mathcomp.analysis.topology_theory.matrix_topology, line 195, characters 11-18
Source code
Local Lemma
mx_ball_center
Source code
: 0 < e -> mx_ball x e x.Source code
Proof.
Local Lemma
mx_ball_sym
Source code
: mx_ball x e y -> mx_ball y e x.Source code
Proof.
Local Lemma
mx_ball_triangle
Source code
:Source code
mx_ball x e1 y -> mx_ball y e2 z -> mx_ball x (e1 + e2) z.
Proof.
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.
by move=> i j; apply: ball_triangle; [exact: xe1_y|exact: ye2_z].
Qed.
Local Lemma
mx_entourage
Source code
: entourage = entourage_ mx_ball.Source code
Proof.
rewrite predeqE=> A; split; last first.
move=> [_/posnumP[e] sbeA].
exists (fun _ _ => [set | ball xy.1 e%:num xy.2]) => //=.
by move=> [] ? ? /= P; exact: sbeA.
move=> [P]; rewrite -entourage_ballE => entP sPA.
set diag := fun : {posnum R} => [set : T * T | ball xy.1 e%:num xy.2].
exists (\big[Num.min/1%:pos]_ \big[Num.min/1%:pos]_ xget 1%:pos
(fun : {posnum R} => diag e `<=` P i j))%:num => //=.
move=> MN/= [] _ MN_min; apply: sPA => i j.
have /(xgetPex 1%:pos): exists : {posnum R}, diag e `<=` P i j.
by have [_/posnumP[e]] := entP i j; exists e.
apply; apply: le_ball (MN_min i j).
apply: le_trans (@bigmin_le _ {posnum R} _ _ i _) _.
exact: bigmin_le.
Qed.
move=> [_/posnumP[e] sbeA].
exists (fun _ _ => [set | ball xy.1 e%:num xy.2]) => //=.
by move=> [] ? ? /= P; exact: sbeA.
move=> [P]; rewrite -entourage_ballE => entP sPA.
set diag := fun : {posnum R} => [set : T * T | ball xy.1 e%:num xy.2].
exists (\big[Num.min/1%:pos]_ \big[Num.min/1%:pos]_ xget 1%:pos
(fun : {posnum R} => diag e `<=` P i j))%:num => //=.
move=> MN/= [] _ MN_min; apply: sPA => i j.
have /(xgetPex 1%:pos): exists : {posnum R}, diag e `<=` P i j.
by have [_/posnumP[e]] := entP i j; exists e.
apply; apply: le_ball (MN_min i j).
apply: le_trans (@bigmin_le _ {posnum R} _ _ i _) _.
exact: bigmin_le.
Qed.
.
instance
Source code
Source code
Definition
Source code
Source code
Uniform_isPseudoMetric
Source code
.Build R 'M[T]_(m, n)Source code
mx_ball_center mx_ball_sym mx_ball_triangle mx_entourage.
End matrix_PseudoMetric.
.
instance
Source code
Source code
Definition
Source code
(Source code
numFieldType
Source code
) (T : completePseudoMetricType R)Source code
(m n : nat) := Uniform_isComplete.Build 'M[T]_(m, n) cauchy_cvg.