~amiloradovsky/symbolic-dynamics

symbolic-dynamics/Shifts.v -rw-r--r-- 5.4 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
(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
 * Basics of Symbolic Dynamics
 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)

Require Import Prodiscrete.
Require Import Algebra.
Require Import FunctionalExtensionality.
Require PropExtensionality.

Section Subshift_space.

  Variable 𝔸 : Set.  (* the alphabet, the space of the symbols,
                        the equality of symbols is proof-irrelevant *)
  Variable 𝕄 : Type.  (* the "time" domain, e.g. N^d or Z^d (d: nat) *)

  Let X := Full_shift_space 𝕄 𝔸.

  Variables (plus : 𝕄 -> 𝕄 -> 𝕄) (zero : 𝕄).
  (* mild bias towards commutativity… *)

  Definition shift_map (k: 𝕄) (f: point_set X): point_set X :=
    fun i => f (plus i k).

  (* Continuity *)

  Lemma inverse_image_of_full_set k:
    inverse_image (shift_map k) Full_set = Full_set.
  Proof.
    apply Extensionality_Ensembles. split. all: repeat constructor.
  Qed.

  Lemma inverse_image_of_cylinder k U:
      (weak_topology_subbasis product_space_proj) U ->
      (weak_topology_subbasis product_space_proj) (inverse_image
                                                     (shift_map k) U).
  Proof.
    intros. destruct H.
    assert (Heq: inverse_image
                   (shift_map k) (inverse_image
                                    (product_space_proj a) V)
                 = inverse_image (product_space_proj (plus a k)) V).
    - apply functional_extensionality; intros.
      unfold inverse_image, In. f_equal.
      rewrite characteristic_function_to_ensemble_is_identity.
      apply functional_extensionality; intros y. f_equal.
    - rewrite Heq; now constructor.
  Qed.

  Import FiniteIntersections PropExtensionality.

  Lemma inverse_image_of_intersection k U V:
      (finite_intersections
         (weak_topology_subbasis product_space_proj)) U ->
      (finite_intersections
         (weak_topology_subbasis product_space_proj)) V ->
      inverse_image (shift_map k) (Intersection U V)
      = Intersection (inverse_image (shift_map k) U)
                     (inverse_image (shift_map k) V).
  Proof.
    intros HU HV.
    unfold inverse_image.
    rewrite characteristic_function_to_ensemble_is_identity.
    apply functional_extensionality; intros y.
    unfold In in *.
    apply propositional_extensionality; split.
    - intro HI; inversion HI.
      constructor. all: now constructor.
    - intro HI. induction HI as [? HU' HV'].
      induction HU', HV'. now constructor.
  Qed.

  Fixpoint inverse_image_of_finite_intersections k U
           (H : finite_intersections
                  (weak_topology_subbasis product_space_proj) U)
           {struct H}:
    finite_intersections
      (weak_topology_subbasis product_space_proj)
      (inverse_image (shift_map k) U).
  Proof.
    intros. inversion H.
    - rewrite inverse_image_of_full_set. constructor.
    - constructor. now apply inverse_image_of_cylinder.
    - rewrite inverse_image_of_intersection.
      constructor 3. all: unfold In; auto.
  Qed.

  Theorem shift_is_continuous: forall k, continuous (shift_map k).
  Proof.
    intro.
    unfold continuous; intros.
    induction H.
    pose (F' U := exists V, F V /\ inverse_image (shift_map k) V = U).
    unfold Included, In in *.
    assert (Heq: FamilyUnion F' = inverse_image (shift_map k)
                                               (FamilyUnion F)).
    {
      apply Extensionality_Ensembles; split.
      - unfold Included; intros x HF'x.
        constructor.
        case HF'x as [? ? F'S Sx].
        case F'S as (U & FU & HI).
        destruct HI.
        case Sx as [H'].
        apply (family_union_intro _ _ _ FU H').
      - unfold Included; intros x HI.
        case HI as [HI].
        inversion HI as [S y].
        pose (U := inverse_image (shift_map k) S).
        assert (Ux: U x) by now constructor.
        assert (F'U: F' U) by now exists S.
        apply (family_union_intro _ _ _ F'U Ux).
    }
    rewrite <- Heq.
    constructor.
    unfold Included; intros x F'x.
    unfold In in *.
    unfold F' in F'x.
    destruct F'x as (V & FV & HI).
    rewrite <- HI.
    apply inverse_image_of_finite_intersections.
    auto.
  Qed.

  (* Actionable *)

  Hypothesis time_is_a_monoid: is_a_monoid 𝕄 plus zero.

  Lemma trivial_shift f: shift_map zero f = f.
  Proof.
    unfold shift_map.
    remember (fun i : 𝕄 => f (plus i zero)) as f0.
    cbv in f, f0 |- *.
    apply functional_extensionality; intros.
    f_equal; intros _.
    subst f0.
    case time_is_a_monoid as [_ [ln rn]].
    now rewrite <- rn.
  Qed.

  Lemma composite_shift k l f:
    shift_map k (shift_map l f) = shift_map (plus k l) f.
  Proof.
    unfold shift_map. cbv.
    apply functional_extensionality; intros.
    f_equal.
    case time_is_a_monoid as [assoc _].
    now rewrite assoc.
  Qed.

  (* Main definitions *)

  Variable S: Ensemble (point_set X).

  Definition invariant_subset f := forall x, S x -> S (f x).
  Definition is_shift_invariant := forall k, invariant_subset
                                               (shift_map k).
  Definition is_a_subshift_space := is_shift_invariant /\ closed S.

  Hypothesis S_is_a_subshift_space: is_a_subshift_space.

  Let Y := SubspaceTopology S.

  Lemma compact_subshift_space : compact (Discrete 𝔸) -> compact Y.
  Proof.
    intro CA; apply closed_compact.
    - apply compact_full_shift_space; assumption.
    - destruct S_is_a_subshift_space as [_ ?]; assumption.
  Qed.

End Subshift_space.