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.


Unset SsrOldRewriteGoalsOrder.  

Import Order.TTheory GRing.Theory Num.Theory.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Section matrix_Topology.
Variables (mSource code nSource code : nat) (TSource code : topologicalType).

Implicit Types M : 'M[T]_(m, n).

Lemma mx_nbhs_filterSource code MSource code : ProperFilter (nbhs M).

Proof.

apply: (filter_from_proper (filter_from_filter _ _)) => [|P Q M_P M_Q|P M_P].
- by exists (fun iSource code jSource code => setT) => ??; apply: filterT.
- exists (fun iSource code jSource code => P i j `&` Q i j) => [??|mx PQmx]; first exact: filterI.
  by split=> i j; have [] := PQmx i j.
- exists (\matrix_(iSource code, jSource code) 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_singletonSource code MSource code (ASource code : set 'M[T]_(m, n)) : nbhs M A -> A M.

Proof.

by move=> [P M_P]; apply=> ??; apply: nbhs_singleton. Qed.

Lemma mx_nbhs_nbhsSource code MSource code (ASource code : set 'M[T]_(m, n)) : nbhs M A -> nbhs M (nbhs^~ A).

Proof.

move=> [P M_P sPA]; exists (fun iSource code jSource code => (P i j)°).
  by move=> ? ?; apply: nbhs_interior.
by move=> ? ?; exists P.
Qed.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code Nbhs_isNbhsTopologicalSource code.Build 'M[T]_(m, n)
  mx_nbhs_filter mx_nbhs_singleton mx_nbhs_nbhs.

End matrix_Topology.

Section matrix_Uniform.
Local Open Scope relation_scope.
Variables (mSource code nSource code : nat) (TSource code : uniformType).

Implicit Types A : set ('M[T]_(m, n) * 'M[T]_(m, n)).

Definition mx_ent

---

Source code := filter_from
  [set PSource code : 'I_m -> 'I_n -> set (T * T) | forall iSource code jSource code, entourage (P i j)]
  (fun PSource code => [set MNSource code : 'M[T]_(m, n) * 'M[T]_(m, n) |
    forall iSource code jSource code, P i j (MN.1 i j, MN.2 i j)]).

Lemma mx_ent_filterSource code : Filter mx_ent.

Proof.

apply: filter_from_filter => [|A B entA entB].
  by exists (fun _ _ => setT) => _ _; apply: filterT.
exists (fun iSource code jSource code => A i j `&` B i j); first by move=> ??; apply: filterI.
by move=> MN ABMN; split=> i j; have [] := ABMN i j.
Qed.

Lemma mx_ent_reflSource code ASource code : mx_ent A -> diagonal `<=` A.

Proof.

move=> [B entB sBA] MN MN1e2; apply: sBA => i j.
by rewrite MN1e2; exact: entourage_refl.
Qed.

Lemma mx_ent_invSource code ASource code : mx_ent A -> mx_ent A^-1.

Proof.

move=> [B entB sBA]; exists (fun iSource code jSource code => (B i j)^-1).
  by move=> i j; apply: entourage_inv.
by move=> MN BMN; apply: sBA.
Qed.

Lemma mx_ent_splitSource code ASource code : mx_ent A -> exists2 BSource code, mx_ent B & B \; B `<=` A.

Proof.

move=> [B entB sBA].
have Bsplit : forall iSource code jSource code, exists CSource code, entourage C /\ C \; C `<=` B i j.
  by move=> ??; apply/exists2P/entourage_split_ex.
exists [set MNSource code : 'M[T]_(m, n) * 'M[T]_(m, n) |
  forall iSource code jSource code, get [set CSource code | entourage C /\ C \; C `<=` B i j]
  (MN.1 i j, MN.2 i j)].
  by exists (fun iSource code jSource code => get [set CSource code | 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_nbhsESource code : nbhs = nbhs_ mx_ent.

Proof.

rewrite predeq2E => M A; split.
  move=> [B]; rewrite -nbhs_entourageE => M_B sBA.
  set sB := fun iSource code jSource code => [set CSource code | entourage C /\ xsection C (M i j) `<=` B i j].
  have {}M_B : forall iSource code jSource code, sB i j !=set0 by move=> ??; apply/exists2P/M_B.
  exists [set MNSource code : 'M[T]_(m, n) * 'M[T]_(m, n) | forall iSource code jSource code,
    get (sB i j) (MN.1 i j, MN.2 i j)].
    by exists (fun iSource code jSource code => 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 iSource code jSource code => 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.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code Nbhs_isUniformSource code.Build 'M[T]_(m, n)
  mx_ent_filter mx_ent_refl mx_ent_inv mx_ent_split mx_ent_nbhsE.

End matrix_Uniform.

Lemma cvg_mx_entouragePSource code (TSource code : puniformType) mSource code nSource code (FSource code : set_system 'M[T]_(m,n))
  (FFSource code : Filter F) (MSource code : 'M[T]_(m,n)) :
  F --> M <->
  forall ASource code, entourage A -> \forall NSource code \near F,
  forall iSource code jSource code, (M i j, (N : 'M[T]_(m,n)) i j) \in A.

Proof.

split.
  rewrite filter_fromP => FM A ?.
  by apply: (FM (fun iSource code jSource code => 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_ijSource code 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_(ijSource code in [set kSource code | k \in [fset xSource code 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 (mSource code nSource code : nat).
HBSource code.instanceSource code DefinitionSource code _Source code (TSource code :Source code ptopologicalTypeSource code) := Filtered.on 'M[T]_(m, n).
HBSource code.instanceSource code DefinitionSource code _Source code (TSource code :Source code puniformTypeSource code) := Pointed.on 'M[T]_(m, n).
End matrix_PointedTopology.

Section matrix_Complete.
Variables (TSource code : completeType) (mSource code nSource code : nat).

Lemma mx_completeSource code (FSource code : set_system 'M[T]_(m, n)) :
  ProperFilter F -> cauchy F -> cvg F.

Proof.

move=> FF Fc.
have /(_ _ _) /cauchy_cvg /cvg_app_entourageP cvF :
  cauchy ((fun MSource code : '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_(iSource code, jSource code) (lim ((fun MSource code : '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.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code Uniform_isCompleteSource code.Build 'M[T]_(m, n) mx_complete.

End matrix_Complete.

Section matrix_PseudoMetric.
Variables (mSource code nSource code : nat) (RSource code : numDomainType) (TSource code : pseudoMetricType R).
Implicit Types (x y : 'M[T]_(m, n)) (e : R).

Definition mx_ball

---

Source code xSource code eSource code ySource code := 0 < e /\ forall iSource code jSource code, ball (x i j) e (y i j).

Local Lemma mx_ball_centerSource code xSource code eSource code : 0 < e -> mx_ball x e x.

Proof.

by move=> ?; split=> [//|? ?]; exact: ballxx. Qed.

Local Lemma mx_ball_symSource code xSource code ySource code eSource code : mx_ball x e y -> mx_ball y e x.

Proof.

by move=> [e0 xe_y]; split=>[//|? ?]; apply/ball_sym/xe_y. Qed.

Local Lemma mx_ball_triangleSource code xSource code ySource code zSource code e1Source code e2Source 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.

Local Lemma mx_entourageSource code : entourage = entourage_ mx_ball.

Proof.

rewrite predeqE=> A; split; last first.
  move=> [_/posnumP[e] sbeA].
  exists (fun _ _ => [set xySource code | ball xy.1 e%:num xy.2]) => //=.
  by move=> [] ? ? /= P; exact: sbeA.
move=> [P]; rewrite -entourage_ballE => entP sPA.
set diag := fun eSource code : {posnum R} => [set xySource code : T * T | ball xy.1 e%:num xy.2].
exists (\big[Num.min/1%:pos]_iSource code \big[Num.min/1%:pos]_jSource code xget 1%:pos
  (fun eSource code : {posnum R} => diag e `<=` P i j))%:num => //=.
move=> MN/= [] _ MN_min; apply: sPA => i j.
have /(xgetPex 1%:pos): exists eSource code : {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.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code Uniform_isPseudoMetricSource code.Build R 'M[T]_(m, n)
  mx_ball_center mx_ball_sym mx_ball_triangle mx_entourage.
End matrix_PseudoMetric.

HBSource code.instanceSource code DefinitionSource code _Source code (RSource code :Source code numFieldTypeSource code) (T : completePseudoMetricType R)
  (m n : nat) := Uniform_isComplete.Build 'M[T]_(m, n) cauchy_cvg.