Files

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 {TSource code USource code : topologicalType}.

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

Lemma prod_nbhs_filterSource code (pSource code : T * U) : ProperFilter (prod_nbhs p).
Proof.
exact: filter_prod_proper. Qed.

Lemma prod_nbhs_singletonSource code (pSource code : T * U) (ASource code : set (T * U)) : prod_nbhs p A -> A p.
Proof.
by move=> [QR [/nbhs_singleton Qp1 /nbhs_singleton Rp2]]; apply.
Qed.

Lemma prod_nbhs_nbhsSource code (pSource code : T * U) (ASource code : 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.


HBSource code.instanceSource code DefinitionSource code _Source code :=Source code Nbhs_isNbhsTopologicalSource code.Build (T * U)%type
  prod_nbhs_filter prod_nbhs_singleton prod_nbhs_nbhs.

End Prod_Topology.

Lemma fst_openSource code {USource code VSource code : topologicalType} (ASource code : 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 snd_openSource code {USource code VSource code : topologicalType} (ASource code : 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 {USource code VSource code : uniformType}.
Implicit Types A : set ((U * V) * (U * V)).

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

Lemma prod_entPUsed by
  • mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule
Source code (ASource code : set (U * U)) (BSource code : set (V * V)) :
  entourage A -> entourage B ->
  prod_ent [set xySource code | 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 prod_ent_filterSource code : 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_reflSource code ASource code : 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_invSource code ASource code : 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_splitSource code ASource code : prod_ent A ->
  exists2 BSource code, prod_ent B & (B \; B `<=` A).
Proof.
move=> [B [entB1 entB2]] sBA; exists [set xySource code | 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 prod_ent_nbhsESource code : 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 xySource code | 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.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code Nbhs_isUniformSource code.Build (U * V)%type
  prod_ent_filter prod_ent_refl prod_ent_inv prod_ent_split prod_ent_nbhsE.

End prod_Uniform.

Lemma entourage_prod_exSUsed by
  • mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule
Source code (USource code VSource code : uniformType) (PSource code : set ((U * V) * (U * V))) :
    entourage P ->
  exists (ASource code : set (U * U)) (BSource code : set (V * V)),
    [/\ entourage A, entourage B &
      [set xSource code | 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 interchange_prod
Source code {TSource code USource code} (xSource code : (T * U) * (T * U)) : (T * T) * (U * U) :=
  (x.1.1, x.2.1, (x.1.2, x.2.2)).

Lemma entourage_interchange_prodSource code {USource code VSource code : uniformType}
  (BSource code : set (U * U)) (CSource code : 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 {USource code VSource code WSource code : uniformType}.

Lemma pair_unif_continuousUsed by
  • mathcomp.analysis.normedtype_theory.tvs
Source code (fSource code : U -> V) (gSource code : U -> W) :
  unif_continuous f -> unif_continuous g ->
  unif_continuous (fun xSource code => (f x, g x)).
Proof.
move=> cf cg A entA.
have [/= BC [entB entC] BCA] : exists2 BCSource code, 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 fst_unif_continuousUsed by
  • mathcomp.analysis.topology_theory.initial_topology
Source code : 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 snd_unif_continuousUsed by
  • mathcomp.analysis.topology_theory.initial_topology
Source code : 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 {RSource code : numDomainType} {USource code VSource code : pseudoMetricType R}.
Implicit Types (x y : U * V).

Definition prod_ball
Used by
  • mathcomp.analysis.topology_theory.metric_structure
  • mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule
Source code xSource code (epsSource code : R) ySource code := ball x.1 eps y.1 /\ ball x.2 eps y.2.

Lemma prod_ball_centerSource code xSource code (epsSource code : R) : 0 < eps -> prod_ball x eps x.
Proof.
by move=> /posnumP[?]. Qed.

Lemma prod_ball_symSource code xSource code ySource code (epsSource code : R) : prod_ball x eps y -> prod_ball y eps x.
Proof.
by move=> [bxy1 bxy2]; split; apply: ball_sym. Qed.

Lemma prod_ball_triangleSource code xSource code ySource code zSource code (e1Source code e2Source code : 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 prod_entourageSource code : entourage = entourage_ prod_ball.
Proof.
rewrite predeqE => P; split; last first.
  move=> [_/posnumP[e] sbeP].
  exists ([set xySource code | ball xy.1 e%:num xy.2],
          [set xySource code | 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.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code Uniform_isPseudoMetricSource code.Build R (U * V)%type
  prod_ball_center prod_ball_sym prod_ball_triangle prod_entourage.

End prod_PseudoMetric.

Section Nbhs_fct2.
Context {TSource code : Type} {RSource code : numDomainType} {USource code VSource code : pseudoMetricType R}.
Lemma fcvg_ball2PSource code {FSource code : set_system U} {GSource code : set_system V}
  {FFSource code : Filter F} {FGSource code : Filter G} (ySource code : U) (zSource code : V):
  (F, G) --> (y, z) <->
  forall epsSource code : R, eps > 0 -> \forall y'Source code \near F & z'Source code \near G,
                ball y eps y' /\ ball z eps z'.
Proof.
exact: fcvg_ballP. Qed.

Lemma cvg_ball2PSource code {ISource code JSource code} {FSource code : set_system I} {GSource code : set_system J}
  {FFSource code : Filter F} {FGSource code : Filter G} (fSource code : I -> U) (gSource code : J -> V) (ySource code : U) (zSource code : V):
  (f @ F, g @ G) --> (y, z) <->
  forall epsSource code : R, eps > 0 -> \forall iSource code \near F & jSource code \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 compact_setXUsed by
  • mathcomp.analysis.topology_theory.function_spaces
Source code {USource code VSource code : topologicalType} (PSource code : set U) (QSource code : 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 iSource code uSource code => forall qSource code, 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 swap_continuousUsed by
  • mathcomp.analysis.topology_theory.order_topology
  • mathcomp.analysis.topology_theory.function_spaces
Source code {XSource code YSource code : 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 {XSource code YSource code ZSource code : topologicalType}.

Lemma prodA_continuousUsed by
  • mathcomp.analysis.topology_theory.function_spaces
Source code : 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 prodAr_continuousSource code : 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.
Generated by rocqnavi
Source
Uses
Used By