~amiloradovsky/symbolic-dynamics

symbolic-dynamics/Shifts-N.v -rw-r--r-- 3.3 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
Require Import Sets.Ensembles.

(* Some helper theory first... *)

Section Preimage.

  Variable X Y : Type.

  Definition preimage (f: X -> Y):
    (Y -> Prop) -> (X -> Prop) := fun S x => S (f x).
  Definition image (f: X -> Y):
    (X -> Prop) -> (Y -> Prop) := fun S y => exists x, S x /\ f x = y.
  Lemma image_of_preimage (f: X -> Y):
    forall U, Included _ (image f (preimage f U)) U.
  Proof. intros. unfold Included, In. intros.
         cbv in H. case H as (t & ? & ftx).
         rewrite <- ftx. assumption. Qed.
  (* The converse inclusion doesn't hold in general:
     subsets of Y, out of scope of image f, won't be included.
     Example: f x := x^2, U := [-1, +1] *)
  Lemma preimage_of_image (f: X -> Y):
    forall U, Included _ U (preimage f (image f U)).
  Proof. intro. unfold Included, In. intros.
           cbv. now exists x. Qed.
  (* Again, the converse inclusion doesn't hold in general:
     example is f := sin, U := [0, pi] *)

End Preimage.

Require Import Topology.ProductTopology.

(* We've assumed the LEM implicitly, and are now in classical logic *)
Fact double_negation (X: Prop): ~ ~ X -> X. Proof. tauto. Qed.

Section Subshift_space.

  Let Constant {U V: Type} (C: V) := fun _: U => C.
  Let Discrete (X: Type): TopologicalSpace.
    refine (Build_TopologicalSpace X (fun _ => True) _ _ _).
    all: trivial. Defined.

  Variable 𝔸: Set.  (* the alphabet, has the discrete topology on it,
                      * is not yet assumed to be finite, later *)
  Let 𝕄 := nat.  (* the time domain, let's be concrete first *)

  Let X := @ProductTopology 𝕄 (Constant (Discrete 𝔸)).
  (* the full shift space; the space of maps, now with a topology *)
  (* point-set of X is essentially just the space of maps 𝕄 -> A *)

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

  Require Import FunctionalExtensionality.

  Lemma extend_shift k x y:
    shift_map k x = y -> exists z, shift_map (S k) z = y.
  Proof.
    intro.
    pose (z := fun i : nat => match i with
                                O => y O
                              | S n => x n end).
    exists z.
    unfold shift_map in *.
    remember (fun i : 𝕄 => z (i + S k)) as zS;
      move HeqzS at top.
    cbv in x, y, z, zS |- *.
    apply functional_extensionality; intros.
    subst zS.
    replace (x0 + S k) with (S (x0 + k)) by auto.
    unfold z. rewrite <- H. reflexivity.
  Qed.

  Lemma shift_map_is_surjective k: surjective (shift_map k).
  Proof. unfold surjective. intros.
         induction k.
         - exists y.
           apply trivial_shift.
         - destruct IHk.
           now apply (extend_shift _ x). Qed.

  Lemma shift_map_may_be_not_injective:
    (exists a a': 𝔸, ~ a = a') ->
    exists k, ~ injective (shift_map k).
  Proof. intros.
         unfold injective.
         destruct H as (a & a' & H).
         exists 1. intro H'.
         pose (x  := fun i : nat => a).
         pose (x' := fun i : nat => match i with 0 => a' | _ => a end).
         specialize (H' x x').
         apply H.
         enough (x 0 = x' 0).
         - now cbv.
         - apply equal_f.
           apply H'.
           unfold shift_map, x, x'.
           cbv; apply functional_extensionality.
           intro n. induction n. all: reflexivity. Qed.

  (* * *)

End Subshift_space.