symbolic-dynamics/Shifts-N.v -rw-r--r-- 3.3 KiB
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.
```