~amiloradovsky/symbolic-dynamics

symbolic-dynamics/Dynamical.v -rw-r--r-- 1.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
(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
 * 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.