~amiloradovsky/symbolic-dynamics

symbolic-dynamics/Metric_Space.v -rw-r--r-- 6.0 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
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
 * Some properties of the metric spaces, which aren't in Topology
 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)

Require Import MetricSpaces.

Section Metric_Space.

  Variable X: Type.  (* carrier *)
  Variable d: X -> X -> R.  (* distance *)
  Hypothesis metric_space: metric d.
  Let Xt := MetricTopology d metric_space.

  Variable F: point_set Xt -> point_set Xt.  (* one-step iterator *)

  Lemma ball_in_ball: forall (p q: X) (ε: R),
      ε > 0 -> (open_ball X d p ε) q -> exists (δ: R) (_: δ > 0),
          Included (open_ball X d q δ) (open_ball X d p ε).
  Proof. intros ? ? ? He Hq. exists (ε - d p q). split.
         + apply (Rgt_minus ε (d p q)). apply Hq; clear Hq.
         + intros y Hin0. firstorder.
           assert (LTPM: forall a b c: R, a < b - c <-> a + c < b).
           {
             intros t u v. split.
             all: intro.
             1: replace u with (u + 0) by auto with real.
             2: replace t with (t + 0) by auto with real.
             1: replace 0 with (- v + v) by auto with real.
             2: replace 0 with (v + - v) by auto with real.
             all: rewrite <- Rplus_assoc.
             all: apply Rplus_lt_compat_r; assumption.
           }
           apply LTPM in H; clear LTPM.
           rewrite Rplus_comm in H.
           pose proof (triangle_inequality
                         X d metric_space p q y) as TI.
           apply (Rle_lt_trans _ _ _ TI); assumption.
  Qed.

End Metric_Space.

(* Metric space regarded as topological *)

Section Metric_Continuity.

  Variable X Y: Type.  (* carrier *)
  Variable dX: X -> X -> R.  (* distance *)
  Variable dY: Y -> Y -> R.  (* distance *)
  Hypothesis X_metric: metric dX.
  Hypothesis Y_metric: metric dY.
  Let Xt := MetricTopology dX X_metric.
  Let Yt := MetricTopology dY Y_metric.

  Variable F: point_set Xt -> point_set Yt.

  Definition metric_continuous_at (x: X) :=
    forall ε: R, ε > 0 -> exists δ: R, δ > 0 /\ forall y,
          dX x y < δ -> dY (F x) (F y) < ε.

  Lemma continuity_equivalence_0:
    continuous F -> forall x, metric_continuous_at x.
  Proof.
    intros C p ? ?.
    pose (B_ε := open_ball (point_set Yt) dY (F p) ε).
    assert (T: open B_ε); simpl in B_ε.
    {
      replace B_ε with (FamilyUnion (Singleton B_ε)).
      - constructor.
        constructor 1 with (a := F p). destruct H0.
        constructor; assumption.
      - apply Extensionality_Ensembles; split.
        + intros ? [* []]; assumption.
        + constructor 1 with (S := B_ε). constructor. assumption.
    }
    unfold continuous in C.
    pose (C_ε := C B_ε).
    pose (D_ε := C_ε T).
    assert (Ip: inverse_image F B_ε p).
    {
      unfold inverse_image. simpl.
      compute. simpl.
      repeat apply intro_characteristic_sat.
      now rewrite metric_zero.
    }
    unfold open in D_ε. simpl in D_ε.
    inversion D_ε as [? ? HU].
    replace (inverse_image F B_ε) with (FamilyUnion F0) in Ip.
    inversion Ip. subst x.
    unfold Included in H0.
    pose proof (H0 S H1).
    inversion H3. subst x.
    destruct H4 as [* H4].
    destruct (ball_in_ball X dX X_metric a p r H4 H2) as (s & Hs & ?).
    exists s. split.
    - assumption.
    - intros.
      assert (open_ball X dX a r y) by firstorder.
      assert (FamilyUnion F0 y).
      {
        constructor 1 with (S := open_ball X dX a r); trivial.
      }
      rewrite HU in H8.
      firstorder.
  Qed.

  Lemma continuity_equivalence_1:
    (forall x, metric_continuous_at x) -> continuous F.
  Proof.
    intros H U H'. simpl in H'. inversion H'.
    assert (forall q, U q -> exists W, F0 W /\ W q).
    {
      intros. subst U. destruct H2. now exists S.
    }
    assert (forall p: X, U (F p) -> exists q r,
                 r > 0 /\ Included (open_ball Y dY q r) U /\
                 open_ball Y dY q r (F p)).
    {
      intros.
      destruct (H2 (F p) H3) as [W [HW HFp]].
      destruct (H0 W HW) as [* MTNB], MTNB.
      exists a, r.
      repeat split.
      - assumption.
      - unfold Included.
        intros.
        rewrite <- H1.
        apply (family_union_intro _ (open_ball Y dY a r)).
        all: assumption.
      - destruct HFp. assumption.
    }
    assert (forall p: X, U (F p) -> exists r,
                 r > 0 /\ Included (open_ball Y dY (F p) r) U).
    {
      intros.
      destruct (H3 p H4) as (q & r & Hr & HI & HFp).
      destruct (ball_in_ball Y dY Y_metric
                             q (F p) r Hr HFp) as (s & Hs & ?).
      exists s. split.
      - assumption.
      - subst U. firstorder.
    }
    assert (forall p: X, inverse_image F U p -> exists r,
                 r > 0 /\ Included (open_ball X dX p r)
                                   (inverse_image F U)).
    {
      intros * [* UFp].
      destruct (H4 p UFp) as (r & Hr & ?).
      destruct (H p r Hr) as (s & Hs & ?).
      exists s. split.
      - assumption.
      - firstorder.
    }
    remember (IndexedUnion
                (metric_topology_neighborhood_basis dX)) as B.
    pose (F1 := fun E => B E /\ Included E (inverse_image F U)).
    assert (EQ: FamilyUnion F1 = inverse_image F (FamilyUnion F0)).
    {
      apply Extensionality_Ensembles; split.
      - intros y Hy.
        constructor.
        destruct Hy as [S p [? HI] Hp].
        destruct (HI p Hp) as [* UFp].
        subst U; inversion UFp.
        apply (family_union_intro F0 S0 (F p)).
        all: assumption.
      - intros p Hp. subst U. destruct (H5 p Hp) as [r []].
        constructor 1 with (S := open_ball X dX p r).
        + constructor.
          * subst B. constructor 1 with (a := p).
            constructor; assumption.
          * intros. constructor; firstorder.
        + constructor. rewrite metric_zero; trivial.
    }
    rewrite <- EQ. simpl. rewrite <- HeqB.
    constructor; firstorder.
  Qed.

  Lemma continuity_equivalence:
    continuous F <-> forall x: point_set Xt, metric_continuous_at x.
  Proof. split.
         - exact continuity_equivalence_0.
         - exact continuity_equivalence_1. Qed.

End Metric_Continuity.