BehaviorMinimality.lean

1 import KomorebiLSM.BehaviorSpace
2 import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
3 
4 /-! Canonical reachability, observability and the uniqueness of minimal models.
5 Similarity transports operators, initial state and mass together. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.Behavior
8 open FiniteInstruments
9 variable {S : Type*} (f : List S → ℝ)
10 
11 theorem history_span : Submodule.span ℝ (Set.range (history f)) = ⊤ := by
12   exact (Submodule.span_range_subtype_eq_top_iff (space f)
13     (fun h => Submodule.subset_span ⟨h,rfl⟩)).mpr rfl
14 
15 theorem canonical_reachable : (canonical f).IsReachable := by
16   have hs : (canonical f).state = history f := by
17     funext h
18     simpa [Realization.state,canonical] using word_history f h []
19   change Submodule.span ℝ (Set.range (canonical f).state) = ⊤
20   rw [hs,history_span]
21 
22 theorem canonical_observable : (canonical f).IsObservable := by
23   intro x y h
24   apply Subtype.ext
25   funext t
26   have ht := congrFun h t
27   simpa only [Realization.observe_apply,canonical,test_evaluation] using ht
28 
29 namespace Realization
30 variable {f}
31 variable {E F : Type*} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F]
32 
33 /-- Any finite model implies finite-dimensional behavior; this is not inferred
34 from a finite sampled table without a rank hypothesis. -/
35 theorem behavior_finite [FiniteDimensional ℝ E] (r : Realization f E) :
36     FiniteDimensional ℝ (space f) :=
37   Module.Finite.of_surjective r.toBehavior r.toBehavior_surjective
38 
39 noncomputable def similarity (r : Realization f E) (q : Realization f F)
40     (hr : r.IsReachable) (ho : r.IsObservable)
41     (hq : q.IsReachable) (hp : q.IsObservable) : E ≃ₗ[ℝ] F :=
42   (r.equiv hr ho).trans (q.equiv hq hp).symm
43 
44 theorem similarity_initial (r : Realization f E) (q : Realization f F)
45     (hr : r.IsReachable) (ho : r.IsObservable)
46     (hq : q.IsReachable) (hp : q.IsObservable) :
47     similarity r q hr ho hq hp r.initial = q.initial := by
48   apply (q.equiv hq hp).injective
49   change q.equiv hq hp ((q.equiv hq hp).symm (r.equiv hr ho r.initial)) = _
50   rw [LinearEquiv.apply_symm_apply,r.equiv_initial hr ho,q.equiv_initial hq hp]
51 
52 theorem similarity_operator (r : Realization f E) (q : Realization f F)
53     (hr : r.IsReachable) (ho : r.IsObservable)
54     (hq : q.IsReachable) (hp : q.IsObservable) (s : S) (x : E) :
55     similarity r q hr ho hq hp (r.operator s x) =
56       q.operator s (similarity r q hr ho hq hp x) := by
57   apply (q.equiv hq hp).injective
58   change q.equiv hq hp ((q.equiv hq hp).symm (r.equiv hr ho (r.operator s x))) = _
59   rw [LinearEquiv.apply_symm_apply,r.equiv_operator hr ho,q.equiv_operator hq hp]
60   congr 1
61   exact (q.equiv hq hp).apply_symm_apply _ |>.symm
62 
63 theorem similarity_mass (r : Realization f E) (q : Realization f F)
64     (hr : r.IsReachable) (ho : r.IsObservable)
65     (hq : q.IsReachable) (hp : q.IsObservable) (x : E) :
66     q.readout (similarity r q hr ho hq hp x) = r.readout x := by
67   rw [← q.equiv_mass hq hp,← r.equiv_mass hr ho]
68   change mass f (q.equiv hq hp ((q.equiv hq hp).symm (r.equiv hr ho x))) = _
69   rw [LinearEquiv.apply_symm_apply]
70 
71 /-- Reachability makes an initial-state/operator intertwiner unique. -/
72 theorem intertwiner_unique (r : Realization f E) (q : Realization f F)
73     (hr : r.IsReachable) (T U : E →ₗ[ℝ] F)
74     (hT0 : T r.initial = q.initial) (hU0 : U r.initial = q.initial)
75     (hT : ∀ s, T.comp (r.operator s) = (q.operator s).comp T)
76     (hU : ∀ s, U.comp (r.operator s) = (q.operator s).comp U) : T = U := by
77   apply LinearMap.ext
78   intro x
79   have hx : x ∈ r.reachable := by rw [hr]; trivial
80   induction hx using Submodule.span_induction with
81   | mem x hx =>
82     obtain ⟨w,rfl⟩ := hx
83     have htw := word_intertwining r.operator q.operator T (fun s => (hT s).symm) w
84     have huw := word_intertwining r.operator q.operator U (fun s => (hU s).symm) w
85     have ht := congrArg (fun L : E →ₗ[ℝ] F => L r.initial) htw
86     have hu := congrArg (fun L : E →ₗ[ℝ] F => L r.initial) huw
87     change T (wordAction r.operator w r.initial) = U (wordAction r.operator w r.initial)
88     simp only [LinearMap.comp_apply,hT0] at ht
89     simp only [LinearMap.comp_apply,hU0] at hu
90     exact ht.symm.trans hu
91   | zero => simp
92   | add x y hx hy ihx ihy => simp only [map_add,ihx,ihy]
93   | smul c x hx ih => simp only [map_smul,ih]
94 
95 /-- The dimension of any reachable observable finite realization is the full
96 behavior dimension, not just the rank of a selected sample. -/
97 theorem minimal_dimension [FiniteDimensional ℝ E] (r : Realization f E)
98     (hr : r.IsReachable) (ho : r.IsObservable) :
99     Module.finrank ℝ E = Module.finrank ℝ (space f) :=
100   (r.equiv hr ho).finrank_eq
101 
102 /-- P27 uniqueness includes the two boundary vectors, not only matrix conjugacy. -/
103 theorem minimal_realizations_similar (r : Realization f E) (q : Realization f F)
104     (hr : r.IsReachable) (ho : r.IsObservable)
105     (hq : q.IsReachable) (hp : q.IsObservable) :
106     ∃ T : E ≃ₗ[ℝ] F,
107       T r.initial = q.initial ∧
108       (∀ s x, T (r.operator s x) = q.operator s (T x)) ∧
109       (∀ x, q.readout (T x) = r.readout x) :=
110   ⟨similarity r q hr ho hq hp, similarity_initial r q hr ho hq hp,
111     similarity_operator r q hr ho hq hp, similarity_mass r q hr ho hq hp⟩
112 
113 end Realization
114 end Komorebi.LSM.Behavior

Back to source controls