CanonicalCone.lean

1 import KomorebiLSM.TestTopology
2 import KomorebiLSM.BehaviorProbability
3 
4 /-! P29: the probability cone is the actual all-test cone of the behavior span.
5 Finite-dimensional compactness is derived in its inherited function-space topology. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.Behavior
8 open scoped BigOperators
9 open FiniteInstruments
10 variable {A O : Type*}
11 variable {f : List (A × O) → ℝ}
12 
13 noncomputable def probabilityCone (f : List (A × O) → ℝ) : Set (space f) :=
14   {v | ∀ w, 0 ≤ (v : List (A × O) → ℝ) w}
15 
16 noncomputable def probabilityBase (f : List (A × O) → ℝ) : Set (space f) :=
17   {v | v ∈ probabilityCone f ∧ mass f v = 1}
18 
19 theorem probabilityCone_eq_tests :
20     probabilityCone f = TestDomains.allTests (branch f) (mass f) := by
21   ext v
22   simp only [probabilityCone,TestDomains.allTests,Set.mem_ofPred_eq,
23     TestDomains.observe_apply,test_evaluation]
24 
25 theorem probabilityBase_eq_tests :
26     probabilityBase f = TestDomains.base (branch f) (mass f) := by
27   unfold probabilityBase TestDomains.base
28   rw [probabilityCone_eq_tests]
29 
30 theorem probability_observe_injective :
31     Function.Injective (TestDomains.observe (branch f) (mass f)) := by
32   intro x y h
33   apply Subtype.ext
34   funext w
35   have he := congrFun h w
36   simpa only [TestDomains.observe_apply,test_evaluation] using he
37 
38 theorem probabilityCone_convex : Convex ℝ (probabilityCone f) := by
39   rw [probabilityCone_eq_tests]
40   exact TestDomains.allTests_convex _ _
41 
42 theorem probabilityCone_pointed {v : space f}
43     (hv : v ∈ probabilityCone f) (hn : -v ∈ probabilityCone f) : v = 0 := by
44   rw [probabilityCone_eq_tests] at hv hn
45   exact TestDomains.allTests_pointed _ _ probability_observe_injective hv hn
46 
47 theorem probabilityCone_closed [FiniteDimensional ℝ (space f)] :
48     IsClosed (probabilityCone f) := by
49   rw [probabilityCone_eq_tests]
50   exact TestDomains.allTests_closed _ _
51 
52 theorem probabilityCone_invariant (s : A × O) {v : space f}
53     (hv : v ∈ probabilityCone f) : branch f s v ∈ probabilityCone f := by
54   intro w; exact hv (s::w)
55 
56 theorem probabilityCone_smul {c : ℝ} (hc : 0 ≤ c) {v : space f}
57     (hv : v ∈ probabilityCone f) : c • v ∈ probabilityCone f := by
58   rw [probabilityCone_eq_tests] at hv ⊢
59   exact TestDomains.allTests_smul _ _ hc hv
60 
61 theorem probabilityCone_add {v w : space f}
62     (hv : v ∈ probabilityCone f) (hw : w ∈ probabilityCone f) :
63     v+w ∈ probabilityCone f := by
64   rw [probabilityCone_eq_tests] at hv hw ⊢
65   exact TestDomains.allTests_add _ _ hv hw
66 
67 theorem history_mem_probabilityCone [Fintype O] (hf : CausalLaw f) (h : List (A × O)) :
68     history f h ∈ probabilityCone f := by
69   intro w; exact hf.nonneg (h ++ w)
70 
71 theorem probabilityCone_spans [Fintype O] (hf : CausalLaw f) :
72     Submodule.span ℝ (probabilityCone f) = ⊤ := by
73   apply top_unique
74   rw [← history_span (f := f)]
75   apply Submodule.span_mono
76   rintro _ ⟨h,rfl⟩
77   exact history_mem_probabilityCone hf h
78 
79 theorem probabilityCone_strict_mass [Fintype O] (hf : CausalLaw f) {v : space f}
80     (hv : v ∈ probabilityCone f) (hne : v ≠ 0) : 0 < mass f v := by
81   rw [probabilityCone_eq_tests] at hv
82   exact TestDomains.allTests_strict_mass _ _ (fun a x => hf.behavior_mass x a)
83     probability_observe_injective hv hne
84 
85 theorem probabilityBase_test_bounds [Fintype O] (hf : CausalLaw f) {v : space f}
86     (hv : v ∈ probabilityBase f) (w : List (A × O)) :
87     0 ≤ (v : List (A × O) → ℝ) w ∧ (v : List (A × O) → ℝ) w ≤ 1 := by
88   rw [probabilityBase_eq_tests] at hv
89   simpa only [TestDomains.observe_apply,test_evaluation] using
90     TestDomains.base_test_bounds _ _ (fun a x => hf.behavior_mass x a) hv w
91 
92 theorem probabilityBase_compact [Fintype O] (hf : CausalLaw f) [FiniteDimensional ℝ (space f)] :
93     IsCompact (probabilityBase f) := by
94   rw [probabilityBase_eq_tests]
95   exact TestDomains.base_compact _ _ (fun a x => hf.behavior_mass x a)
96     probability_observe_injective
97 
98 theorem probabilityBase_convex : Convex ℝ (probabilityBase f) := by
99   rw [probabilityBase_eq_tests]
100   exact TestDomains.base_convex _ _
101 
102 theorem initial_mem_probabilityBase [Fintype O] (hf : CausalLaw f) :
103     history f [] ∈ probabilityBase f :=
104   ⟨history_mem_probabilityCone hf [], by simpa using hf.initial⟩
105 
106 theorem probabilityBase_posterior {v : space f} (hv : v ∈ probabilityBase f)
107     (s : A × O) (hp : 0 < mass f (branch f s v)) :
108     normalize (mass f) (branch f s v) ∈ probabilityBase f := by
109   rw [probabilityBase_eq_tests] at hv ⊢
110   exact TestDomains.base_posterior _ _ hv.1 s hp
111 
112 /-- In test coordinates every component lies in [0,1] and the empty test is one. -/
113 theorem probabilityBase_core_bounds [Fintype O] {I : Type*} (hf : CausalLaw f)
114     (tests : I → List (A × O)) (i₀ : I) (hi : tests i₀ = [])
115     {v : space f} (hv : v ∈ probabilityBase f) :
116     (evaluate f tests v) i₀ = 1 ∧ ∀ i, (evaluate f tests v) i ∈ Set.Icc (0 : ℝ) 1 := by
117   refine ⟨?_,fun i => probabilityBase_test_bounds hf hv (tests i)⟩
118   simpa only [evaluate_apply,hi,mass_apply] using hv.2
119 
120 /-- Collected P29 conclusions for the actual canonical behavior space. -/
121 theorem canonical_probability_cone [Fintype O] (hf : CausalLaw f) [FiniteDimensional ℝ (space f)] :
122     IsClosed (probabilityCone f) ∧ Convex ℝ (probabilityCone f) ∧
123     (∀ v, v ∈ probabilityCone f → -v ∈ probabilityCone f → v = 0) ∧
124     Submodule.span ℝ (probabilityCone f) = ⊤ ∧
125     (∀ s v, v ∈ probabilityCone f → branch f s v ∈ probabilityCone f) ∧
126     (∀ v, v ∈ probabilityCone f → v ≠ 0 → 0 < mass f v) ∧
127     (∀ a v, ∑ o, mass f (branch f (a,o) v) = mass f v) ∧
128     IsCompact (probabilityBase f) ∧ Convex ℝ (probabilityBase f) ∧
129     (probabilityBase f).Nonempty :=
130   ⟨probabilityCone_closed,probabilityCone_convex,
131    fun _ => probabilityCone_pointed,probabilityCone_spans hf,
132    fun s _ => probabilityCone_invariant s,fun _ => probabilityCone_strict_mass hf,
133    fun a v => hf.behavior_mass v a,probabilityBase_compact hf,probabilityBase_convex,
134    ⟨history f [],initial_mem_probabilityBase hf⟩⟩
135 
136 end Komorebi.LSM.Behavior

Back to source controls