symbolic-dynamics/Dynamical.v -rw-r--r-- 1.8 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```
```(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
* Miscellaneous properties regarding discrete-time dynamical systems
* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)

Section Power.

(* Church numerals; monoid generated by endo-function *)

Variable X: Type.

Definition endo := X -> X.
Definition id: endo := fun x => x.
Fixpoint power (F: endo) (t: nat): endo :=
match t with O => id | S t' => fun (x: X) => F ((power F t') x) end.

End Power.

Require Import Topology.Continuity.

Section Discrete_Time.

(* Discrete-time autonomous topological dynamical system *)

Variable X: TopologicalSpace.

Variable F: endo (point_set X).  (* one-step iterator *)
Hypothesis continuity: continuous F.

Let F' := power _ F.  (* multiple-steps iterator *)
Lemma power_continuous: forall t, continuous (F' t).
Proof. intro; induction t.
- apply continuous_identity.
- apply (continuous_composition F); trivial.
Qed.

Section Local_Properties.

Variable x: point_set X.

Definition isolated := open (Singleton x).
Definition periodic := exists t, F' (S t) x = x.
Definition recurrent :=
forall U: Ensemble (point_set X),
open U -> U x -> exists t a b, U a /\ U b /\ F' (S t) b = a.

Example isolated_recurrent_is_periodic:
isolated -> recurrent -> periodic.
Proof. intros HI HR.
unfold periodic.
unfold isolated in HI.
unfold recurrent in HR.
destruct (HR (Singleton x) HI) as [n].
- constructor.
- destruct H as (a & b & Spa & Spb & ?), Spb, Spa.
exists n; assumption.
Qed.

End Local_Properties.

Definition perfect := forall x: point_set X, ~ isolated x.

End Discrete_Time.
```