~amiloradovsky/symbolic-dynamics

symbolic-dynamics/Local_Rule.v -rw-r--r-- 4.8 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
(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
 * The equivalence between the local rule and the uniform continuity
 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)

Require Import Symbolic_Dynamics.Patterns_US.

Section Local_Rule.

  Variable 𝔸 : Set.
  Variable 𝕄 : Type.
  Variable S : Symbolic_Dynamics.Families.Family (configuration 𝕄 𝔸).
  Let X := sigT S.

  Variable 𝔹 : Set.
  Variable  : Type.
  Variable T : Symbolic_Dynamics.Families.Family (configuration  𝔹).
  Let Y := sigT T.

  Variable 𝛷 : X -> Y.

  Let pjS := @projT1 _ S.
  Let pjT := @projT1 _ T.

  Definition ensemble_restriction
             (U : Symbolic_Dynamics.Families.Family 𝕄) :
    Symbolic_Dynamics.Families.Family (anchored_pattern 𝕄 𝔸 U) :=
    fun u => {x & restriction 𝕄 𝔸 always_in_full (pjS x) = u}.

  Lemma ensemble_restriction_is_sound : forall U x,
      ensemble_restriction U (restriction 𝕄 𝔸 always_in_full (pjS x)).
  Proof. intros. exists x. reflexivity. Qed.

  Definition is_anchored_local_rule :=
    forall V : Symbolic_Dynamics.Families.Family ,
      exists (U : Symbolic_Dynamics.Families.Family 𝕄)
             (φ : sigT (ensemble_restriction U) ->
                  anchored_pattern _ _ V),
        forall x H,
          φ (existT _ (restriction 𝕄 𝔸 always_in_full (pjS x)) H)
          = restriction _ _ always_in_full (pjT (𝛷 x)).

  Definition is_uniformly_continuous :=
    uniform_continuous _ _ (uniformity 𝕄 𝔸 S) (uniformity  𝔹 T) 𝛷.

  Lemma local_rule_implies_uniform_continuity:
    is_anchored_local_rule -> is_uniformly_continuous.
  Proof.
    intros ? U_ HUU.
    destruct HUU as (EV_ & EV & HIEV & HFSV).
    destruct HFSV as [V].
    specialize (H V).
    destruct H as (U & φ & ?).
    eexists.
    split.
    + constructor.
      eexists.
      split.
      * intros ???. apply H0.
      * constructor.
    + intros.
      apply HIEV.
      constructor.
      destruct H0.

      unfold pjS, pjT in H.
      rewrite <- (H x (ensemble_restriction_is_sound U x)).
      rewrite <- (H y (ensemble_restriction_is_sound U y)).

      (* the existential variable has to be instantiated first *)
      Unshelve.
      2: exact U.

      generalize (ensemble_restriction_is_sound U y).
      generalize (ensemble_restriction_is_sound U x).
      intros ex ey.
      remember (restriction 𝕄 𝔸 always_in_full (_ x)) as u.
      remember (restriction 𝕄 𝔸 always_in_full (_ y)) as v.
      clear Heqv; subst v.
      subst u.
      assert (HH : forall z H0 H1,
                 φ (existT _ (restriction 𝕄 𝔸 always_in_full
                                          (_ z)) H0) =
                 φ (existT _ (restriction 𝕄 𝔸 always_in_full
                                          (_ z)) H1))
        by (intros; do 2 rewrite (H z); reflexivity).
      erewrite HH. reflexivity.
  Qed.

  Lemma uniformly_continuous_localization:
    is_uniformly_continuous ->
    forall V : Symbolic_Dynamics.Families.Family ,
    exists (U : Symbolic_Dynamics.Families.Family 𝕄),
      forall x y, @restriction _ _ U _ always_in_full (pjS x) =
                  @restriction _ _ U _ always_in_full (pjS y) ->
                  @restriction _ _ V _ always_in_full (pjT (𝛷 x)) =
                  @restriction _ _ V _ always_in_full (pjT (𝛷 y)).
  Proof.
    intros ??.
    intros.
    unfold is_uniformly_continuous, uniform_continuous in H.
    specialize (H (entourage_base _ _ _ V)).
    destruct H as [U_].
    + constructor.
      exists (entourage_base _ _ _ V).
      split.
      * intros ???; assumption.
      * constructor.
    + destruct H as [? HI].
      destruct H as (U_ & U & HIUU_ & HUFS).
      destruct HUFS.
      exists U.
      intros x' y' ?.
      specialize (HI x' y').
      assert (Heck: entourage_base 𝕄 𝔸 _ U x' y') by now constructor.
      specialize (HIUU_ x' y' Heck).
      destruct (HI HIUU_); assumption.
  Qed.

  Import FunctionalExtensionality.

  Let f U x := @restriction 𝕄 𝔸 U _ always_in_full (pjS x).
  Let g V y := @restriction  𝔹 V _ always_in_full (pjT y).

  Lemma uniform_continuity_implies_local_rule:
    is_uniformly_continuous -> is_anchored_local_rule.
  Proof.
    intro. assert (UCL := uniformly_continuous_localization H).
    intro. destruct (UCL V) as [U HU]. clear H UCL.
    exists U.
    eexists.
    Unshelve. 2: {
      intro u'. apply (g V), 𝛷.
      destruct u' as [u eru]. destruct eru as [x _]. exact x.
    }
    destruct H.
    apply HU.
    assumption.
  Qed.

  Lemma uniform_continuity_iff_local_rule:
    is_uniformly_continuous <-> is_anchored_local_rule.
  Proof.
    split.
    - exact uniform_continuity_implies_local_rule.
    - exact local_rule_implies_uniform_continuity.
  Qed.

End Local_Rule.