Module mathcomp.analysis.topology_theory.product_topology

From HB Require Import structures.
From mathcomp Require Import boot order algebra all_classical.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import interval_inference topology_structure.
From mathcomp Require Import uniform_structure pseudometric_structure compact.

# Product topology Product `(T * U)%type` are endowed with the structures of: - topology - uniform space - pseudometric space - metric space

Import Order.TTheory GRing.Theory Num.Theory.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Section Prod_Topology.
Context { : topologicalType}.

Let ( : T * U) := filter_prod (nbhs p.1) (nbhs p.2).

Lemma ( : T * U) : ProperFilter (prod_nbhs p).

Proof.

exact: filter_prod_proper. Qed.

Lemma ( : T * U) ( : set (T * U)) : prod_nbhs p A -> A p.

Proof.

by move=> [QR [/nbhs_singleton Qp1 /nbhs_singleton Rp2]]; apply.
Qed.

Lemma ( : T * U) ( : set (T * U)) :
prod_nbhs p A -> prod_nbhs p (prod_nbhs^~ A).

Proof.

move=> [QR [/nbhs_interior p1_Q /nbhs_interior p2_R] sQRA].
by exists (QR.1°, QR.2°) => // ??; exists QR.
Qed.

..Build (T * U)%type
prod_nbhs_filter prod_nbhs_singleton prod_nbhs_nbhs.

End Prod_Topology.

Lemma { : topologicalType} ( : set (U * V)) :
open A -> open (fst @` A).

Proof.

rewrite !openE => oA z [[a b/=] Aab <-]; rewrite /interior.
have [[P Q] [Pa Qb] pqA] := oA _ Aab; apply: (@filterS _ _ _ P) => // p Pp.
by exists (p, b) => //=; apply: pqA; split=> //=; exact: nbhs_singleton.
Qed.

Lemma { : topologicalType} ( : set (U * V)) :
open A -> open (snd @` A).

Proof.

rewrite !openE => oA z [[a b/=] Aab <-]; rewrite /interior.
have [[P Q] [Pa Qb] pqA] := oA _ Aab; apply: (@filterS _ _ _ Q) => // q Qq.
by exists (a, q) => //=; apply: pqA; split => //; exact: nbhs_singleton.
Qed.

product of two uniform spaces

Section prod_Uniform.
Local Open Scope relation_scope.
Context { : uniformType}.
Implicit Types A : set ((U * V) * (U * V)).

Definition :=
  [set : set ((U * V) * (U * V)) |
    filter_prod (@entourage U) (@entourage V)
    [set ((xy.1.1,xy.2.1),(xy.1.2,xy.2.2)) | in A]].

Lemma ( : set (U * U)) ( : set (V * V)) :
  entourage A -> entourage B ->
  prod_ent [set | A (xy.1.1, xy.2.1) /\ B (xy.1.2, xy.2.2)].

Proof.

move=> entA entB; exists (A,B) => // xy ABxy.
by exists ((xy.1.1, xy.2.1),(xy.1.2,xy.2.2)); rewrite /= -!surjective_pairing.
Qed.

Lemma : Filter prod_ent.

Proof.

have prodF := filter_prod_filter (@entourage_filter U) (@entourage_filter V).
split; rewrite /prod_ent.
- by rewrite -setXTT; apply: prod_entP filterT filterT.
- move=> A B /= entA entB; apply: filterS (filterI entA entB) => xy [].
  move=> [zt Azt ztexy] [zt' Bzt' zt'exy]; exists zt => //; split=> //.
  move/eqP: ztexy; rewrite -zt'exy !xpair_eqE.
  by rewrite andbACA -!xpair_eqE -!surjective_pairing => /eqP->.
- by move=> A B sAB /=; apply: filterS => ? [xy /sAB ??]; exists xy.
Qed.

Lemma : prod_ent A -> diagonal `<=` A.

Proof.

move=> [B [entB1 entB2] sBA] xy /eqP.
rewrite [_.1]surjective_pairing [xy.2]surjective_pairing xpair_eqE.
move=> /andP [/eqP xy1e /eqP xy2e].
have /sBA : (B.1 `*` B.2) ((xy.1.1, xy.2.1), (xy.1.2, xy.2.2)).
by rewrite xy1e xy2e; split=> /=; exact: entourage_refl.
move=> [zt Azt /eqP]; rewrite !xpair_eqE.
by rewrite andbACA -!xpair_eqE -!surjective_pairing => /eqP<-.
Qed.

Lemma : prod_ent A -> prod_ent A^-1.

Proof.

move=> [B [/entourage_inv entB1 /entourage_inv entB2] sBA].
have:= prod_entP entB1 entB2; rewrite /prod_ent/=; apply: filterS.
move=> _ [p /(sBA (_,_)) [[x y] ? xyE] <-]; exists (y,x) => //; move/eqP: xyE.
by rewrite !xpair_eqE => /andP[/andP[/eqP-> /eqP->] /andP[/eqP-> /eqP->]].
Qed.

Lemma : prod_ent A ->
exists2 , prod_ent B & (B \; B `<=` A).

Proof.

move=> [B [entB1 entB2]] sBA; exists [set | split_ent B.1 (xy.1.1,xy.2.1) /\
  split_ent B.2 (xy.1.2,xy.2.2)].
  by apply: prod_entP; apply: entourage_split_ent.
move=> xy [uv /= [hB1xyuv1 hB2xyuv1] [hB1xyuv2 hB2xyuv2]].
have /sBA : (B.1 `*` B.2) ((xy.1.1, xy.2.1),(xy.1.2,xy.2.2)).
  by split=> /=; apply: subset_split_ent => //; [exists uv.1|exists uv.2].
move=> [zt Azt /eqP]; rewrite !xpair_eqE andbACA -!xpair_eqE.
by rewrite -!surjective_pairing => /eqP<-.
Qed.

Lemma : nbhs = nbhs_ prod_ent.

Proof.

rewrite predeq2E => xy A; split=> [[B []] | [B [C [entC1 entC2] sCB] sBA]].
  rewrite -!nbhs_entourageE => - [C1 entC1 sCB1] [C2 entC2 sCB2] sBA.
  exists [set | C1 (xy.1.1, xy.2.1) /\ C2 (xy.1.2, xy.2.2)].
    exact: prod_entP.
  move=> uv /xsectionP/= [/xsectionP/sCB1 Buv1 /xsectionP/sCB2/(conj Buv1)].
  exact: sBA.
exists (xsection C.1 xy.1, xsection C.2 xy.2).
  by rewrite -!nbhs_entourageE; split; [exists C.1|exists C.2].
move=> uv [/= /xsectionP Cxyuv1 /xsectionP Cxyuv2]; apply: sBA.
have /sCB : (C.1 `*` C.2) ((xy.1,uv.1), (xy.2,uv.2)) => //.
move=> [zt Bzt /eqP]; rewrite !xpair_eqE andbACA -!xpair_eqE.
by  rewrite -!surjective_pairing => /eqP ztE; apply/xsectionP; rewrite -ztE.
Qed.

..Build (U * V)%type
  prod_ent_filter prod_ent_refl prod_ent_inv prod_ent_split prod_ent_nbhsE.

End prod_Uniform.

Lemma ( : uniformType) ( : set ((U * V) * (U * V))) :
    entourage P ->
  exists ( : set (U * U)) ( : set (V * V)),
    [/\ entourage A, entourage B &
      [set | A (x.1.1, x.2.1) /\ B (x.1.2, x.2.2)] `<=` P].

Proof.

move=> [[A B] /= [entA entB] ABP].
exists A, B; split => // -[[x1 y1] [x2 y2]] /= [Axx Byy].
have /ABP [[[a b] [c d]] Pabcd]/= : (A `*` B) ((x1, x2), (y1, y2)) by [].
by case=> <- <- <- <-.
Qed.

TODO: mv to `unstable.v`?

Definition { } ( : (T * U) * (T * U)) : (T * T) * (U * U) :=
(x.1.1, x.2.1, (x.1.2, x.2.2)).

Lemma { : uniformType}
( : set (U * U)) ( : set (V * V)) :
entourage B -> entourage C -> entourage (interchange_prod @^-1` (B `*` C)).

Proof.

move=> entB entC; exists (B, C) => //= -[[x1 x2] [x3 x4]] [/= HB HC].
by exists (x1, x3, (x2, x4)).
Qed.

Section unif_continuous_pair.
Context { : uniformType}.

Lemma ( : U -> V) ( : U -> W) :
unif_continuous f -> unif_continuous g ->
unif_continuous (fun => (f x, g x)).

Proof.

move=> cf cg A entA.
have [/= BC [entB entC] BCA] : exists2 , entourage BC.1 /\ entourage BC.2 &
    interchange_prod @^-1` (BC.1 `*` BC.2) `<=` A.
  move: entA => -[[B C]] entBD BCA; exists (B, C) => //=.
  move=> [[x1 x2] [x3 x4]] [/=] Bx Cx.
  have /= := BCA (x1, x3, _) (conj Bx Cx).
  by move=> [[[a1 a2] [b1 b2]]]/= ? [<- <- <- <-].
apply: (@filterS _ _ _ (map_pair f @^-1` BC.1 `&` (map_pair g) @^-1` BC.2)).
  by move=> xy [Bxy Cxy]; exact: BCA.
by apply: filterI; [exact: cf|exact: cg].
Qed.

Lemma : unif_continuous (@fst U V).

Proof.

move=> A entA; exists (A, setT) => /=; first by split => //; exact: entourageT.
by move=> [[x1 x2] [y1 y2]] [/= Ax _]; exists (x1, y1, (x2, y2)).
Qed.

Lemma : unif_continuous (@snd U V).

Proof.

move=> B entB; exists (setT, B) => /=; first by split => //; exact: entourageT.
by move=> [[x1 x2] [y1 y2]] [/= _ Bx]; exists (x1, y1, (x2, y2)).
Qed.

End unif_continuous_pair.

product of two pseudoMetric spaces

Section prod_PseudoMetric.
Context { : numDomainType} { : pseudoMetricType R}.
Implicit Types (x y : U * V).

Definition ( : R) := ball x.1 eps y.1 /\ ball x.2 eps y.2.

Lemma ( : R) : 0 < eps -> prod_ball x eps x.

Proof.

by move=> /posnumP[?]. Qed.

Lemma ( : R) : prod_ball x eps y -> prod_ball y eps x.

Proof.

by move=> [bxy1 bxy2]; split; apply: ball_sym. Qed.

Lemma ( : R) :
prod_ball x e1 y -> prod_ball y e2 z -> prod_ball x (e1 + e2) z.

Proof.

by move=> [bxy1 bxy2] [byz1 byz2]; split; apply: ball_triangle; eassumption.
Qed.

Lemma : entourage = entourage_ prod_ball.

Proof.

rewrite predeqE => P; split; last first.
  move=> [_/posnumP[e] sbeP].
  exists ([set | ball xy.1 e%:num xy.2],
          [set | ball xy.1 e%:num xy.2]) => //=.
  move=> [[a b] [c d]] [bab bcd]; exists ((a, c), (b, d))=> //=.
  exact: sbeP.
move=> [[A B]] /=; rewrite -!entourage_ballE.
move=> [[_/posnumP[eA] sbA] [_/posnumP[eB] sbB] sABP].
exists (Num.min eA eB)%:num => //= -[[a b] [c d] [/= bac bbd]].
suff /sABP [] : (A `*` B) ((a, c), (b, d)).
  by move=> [[? ?] [? ?]] ? [<- <- <- <-].
(split; [apply: sbA|apply: sbB]) => /=.
  by apply: le_ball bac; rewrite num_le ge_min lexx.
by apply: le_ball bbd; rewrite num_le ge_min lexx orbT.
Qed.

..Build R (U * V)%type
  prod_ball_center prod_ball_sym prod_ball_triangle prod_entourage.

End prod_PseudoMetric.

Section Nbhs_fct2.
Context { : Type} { : numDomainType} { : pseudoMetricType R}.
Lemma { : set_system U} { : set_system V}
  { : Filter F} { : Filter G} ( : U) ( : V):
  (F, G) --> (y, z) <->
  forall : R, eps > 0 -> \forall \near F & \near G,
                ball y eps y' /\ ball z eps z'.

Proof.

exact: fcvg_ballP. Qed.

Lemma { } { : set_system I} { : set_system J}
  { : Filter F} { : Filter G} ( : I -> U) ( : J -> V) ( : U) ( : V):
  (f @ F, g @ G) --> (y, z) <->
  forall : R, eps > 0 -> \forall \near F & \near G,
                ball y eps (f i) /\ ball z eps (g j).

Proof.

rewrite fcvg_ball2P; split=> + e e0 => /(_ e e0).
by rewrite near_map2; apply.
by move=> fgyz; rewrite near_map2; apply: fgyz.
Qed.

End Nbhs_fct2.

Lemma { : topologicalType} ( : set U) ( : set V) :
compact P -> compact Q -> compact (P `*` Q).

Proof.

rewrite !compact_near_coveringP => cptP cptQ I F Pr Ff cvfPQ.
have := cptP I F (fun => forall , Q q -> Pr i (u, q)) Ff.
set R := (R in (R -> _) -> _); suff R' : R.
by move/(_ R'); apply:filter_app; near=> i => + [a b] [Pa Qb]; apply.
rewrite /R => x Px; apply: (@cptQ _ (filter_prod _ _)) => v Qv.
case: (cvfPQ (x, v)) => // [[N G]] /= [[[N1 N2 /= [N1x N2v]]]] N1N2N FG ngPr.
exists (N2, N1`*`G); first by split => //; exists (N1, G).
case=> a [b i] /= [N2a [N1b]] Gi.
by apply: (ngPr (b, a, i)); split => //; exact: N1N2N.
Unshelve. all: by end_near. Qed.

Lemma { : topologicalType} : continuous (@swap X Y).

Proof.

case=> a b W /= [[U V]][] /= Ub Va UVW; exists (V, U); first by split.
by case => //= ? ? [] ? ?; exact: UVW.
Qed.

Section reassociate_continuous.
Context { : topologicalType}.

Lemma : continuous (@prodA X Y Z).

Proof.

move=> [] [a b] c U [[/= P V]] [Pa] [][/= Q R][ Qb Rc] QRV PVU.
exists ((P `*` Q), R); first split.
- exists (P, Q); first by [].
by case=> x y /= [Px Qy].
- by [].
- by move=> [[x y] z] [] [] ? ? ?; apply: PVU; split => //; exact: QRV.
Qed.

Lemma : continuous (@prodAr X Y Z).

Proof.

case=> a [b c] U [[V R]] [/= [[P Q /=]]] [Pa Qb] PQV Rc VRU.
exists (P, (Q `*` R)); first split => //.
- exists (Q, R); first by [].
by case=> ? ? /= [].
- by case=> x [y z] [? [? ?]]; apply: VRU; split => //; exact: PQV.
Qed.

End reassociate_continuous.

Files

Module mathcomp.analysis.topology_theory.product_topology