~amiloradovsky/symbolic-dynamics

symbolic-dynamics/Uniform.v -rw-r--r-- 3.7 KiB View raw
5857f238Andrew Miloradovsky .build.yml: continuous integration for SourceHut 7 months ago
                                                                                
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
 * Uniform structure and continuity, entourages
 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)

(* The topology library also contains a module on uniform spaces,
 * but it doesn't use or define the notion of an entourage. So... *)

Require Import Relations.Relation_Definitions.

Axiom extensionality_relations:
  forall (U: Type) X Y, same_relation U X Y -> X = Y.
(* Isn't needed here but in applications,
   this axiom should better be in Relations *)

Section Uniform_space.

  Variable X: Type.  (* we suppose, being a set isn't essential here *)

  Inductive uniformity_from_fundamental_system
            (Φ : (relation X) -> Prop) : (relation X) -> Prop :=
  | uniformity_intro: forall U,
      (exists V, inclusion _ V U /\ Φ V) ->
      uniformity_from_fundamental_system Φ U.

  (* These inductive definitions are adapted from Ensembles.
   * Perhaps, they instead should reside somewhere in Relations...
   * and also be unified with Ensembles and general n-ary relations *)

  Inductive composition (R S: relation X): relation X :=
    composition_intro : forall a c: X,
      (exists b: X, R a b /\ S b c) -> (composition R S) a c.
  Inductive diagonal: relation X :=  (* identity *)
    diagonal_intro : forall a: X, diagonal a a.

  (* The transposed relation is not an inverse, this isn't a groupoid *)

  Inductive converse (R: relation X): relation X :=
    converse_intro : forall a b: X, R a b -> (converse R) b a.

  Inductive intersection (R S: relation X): relation X :=
    intersection_intro :
      forall a b: X, R a b -> S a b -> (intersection R S) a b.
  Inductive union (R S: relation X): relation X :=
    | union_introl : forall a b: X, R a b -> (union R S) a b
    | union_intror : forall a b: X, S a b -> (union R S) a b.

  (* Done with general relations, now goes topology-specific stuff: *)

  Variable Φ: (relation X) -> Prop.  (* space (carrier) of entourages *)

  Definition is_reflexive :=
    forall U: relation X, Φ U -> reflexive X U.
  Definition is_upper_closed :=
    forall U V: relation X, inclusion X U V -> Φ U -> Φ V.
  Definition is_stable_by_intersection :=
    forall U V: relation X, Φ U -> Φ V -> Φ (intersection U V).
  Definition is_stable_by_symmetry :=
    forall U: relation X, Φ U -> Φ (converse U).
  Definition squared U := composition U U.
  Definition square_is_in U V := inclusion X (squared U) V.
  Definition there_exist_square_roots :=
    forall V: relation X, Φ V ->
                          exists U: relation X, Φ U /\ square_is_in U V.
  (* These are essentially square roots, except the other inclusion *)
  Definition is_uniform_structure :=
    is_reflexive /\
    is_upper_closed /\
    is_stable_by_symmetry /\
    is_stable_by_intersection /\
    there_exist_square_roots.

  Hypothesis uniform_space: is_uniform_structure.

  (* https://en.wikipedia.org/wiki/Uniform_space#Entourage_definition *)

End Uniform_space.

Arguments uniformity_from_fundamental_system {X}.

Section Uniform_continuity.

  Variables X Y: Type.
  Variable Φ: (relation X) -> Prop.
  Hypothesis uniform_space_X: is_uniform_structure X Φ.
  Variable Ψ: (relation Y) -> Prop.
  Hypothesis uniform_space_Y: is_uniform_structure Y Ψ.

  Definition uniform_continuous (f: X -> Y) :=
    forall U, Ψ U -> exists V, Φ V /\
                               forall x y, V x y -> U (f x) (f y).
  (* if points in Y are U-close, then the points in X are V-close *)

End Uniform_continuity.

Require Import Topology.UniformTopology.

(* TODO: properties, connections with metric and topology; e.g.
   - metric -> uniform
   - compact -> uniform
   - uniform -> metrizable
   - uniform -> topological
 *)