BehaviorProbability.lean

1 import KomorebiLSM.ObservableRealization
2 
3 /-! Finite interventional word laws and normalized behavior states.
4 Rank is separate from the supplied nonnegativity and causal mass identities. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.Behavior
7 open scoped BigOperators
8 open FiniteInstruments
9 variable {A O : Type*} [Fintype O]
10 
11 structure CausalLaw (f : List (A × O) → ℝ) : Prop where
12   initial : f [] = 1
13   nonneg : ∀ w, 0 ≤ f w
14   sum_next : ∀ h a, ∑ o, f (h ++ [(a,o)]) = f h
15 
16 namespace CausalLaw
17 variable {f : List (A × O) → ℝ} (hf : CausalLaw f)
18 include hf
19 
20 theorem next_le (h : List (A × O)) (a : A) (o : O) :
21     f (h ++ [(a,o)]) ≤ f h := by
22   rw [← hf.sum_next h a]
23   exact Finset.single_le_sum (fun o _ => hf.nonneg (h ++ [(a,o)])) (Finset.mem_univ o)
24 
25 /-- A future experiment is an event under its fixed intervention schedule. -/
26 theorem extension_le (h t : List (A × O)) : f (h ++ t) ≤ f h := by
27   induction t generalizing h with
28   | nil => simp
29   | cons s t ih =>
30     have he := ih (h ++ [s])
31     have hs := hf.next_le h s.1 s.2
32     simpa only [List.append_assoc,List.singleton_append] using he.trans hs
33 
34 theorem word_bounds (w : List (A × O)) : 0 ≤ f w ∧ f w ≤ 1 := by
35   refine ⟨hf.nonneg w, ?_⟩
36   simpa only [List.nil_append,hf.initial] using hf.extension_le [] w
37 
38 theorem conditional_bounds (h t : List (A × O)) (hh : 0 < f h) :
39     0 ≤ f (h ++ t) / f h ∧ f (h ++ t) / f h ≤ 1 := by
40   exact ⟨div_nonneg (hf.nonneg _) hh.le,(div_le_one hh).mpr (hf.extension_le h t)⟩
41 
42 theorem conditional_observation_mass (h : List (A × O)) (a : A) (hh : 0 < f h) :
43     ∑ o, f (h ++ [(a,o)]) / f h = 1 := by
44   rw [← Finset.sum_div,hf.sum_next,div_self (ne_of_gt hh)]
45 
46 /-- The causal mass law extends linearly to the whole behavior space. -/
47 theorem behavior_mass (v : space f) (a : A) :
48     ∑ o, mass f (branch f (a,o) v) = mass f v := by
49   suffices hx : ∀ x, x ∈ space f → (∑ o, x [(a,o)]) = x [] from hx v v.property
50   intro x hx
51   induction hx using Submodule.span_induction with
52   | mem x hx =>
53     obtain ⟨h,rfl⟩ := hx
54     simpa only [column,List.append_nil] using hf.sum_next h a
55   | zero => simp
56   | add x y hx hy ihx ihy =>
57     simp only [Pi.add_apply,Finset.sum_add_distrib,ihx,ihy]
58   | smul c x hx ih =>
59     simp only [Pi.smul_apply,smul_eq_mul,← Finset.mul_sum,ih]
60 
61 theorem normalized_history_nonneg (h : List (A × O)) (hh : 0 < f h)
62     (t : List (A × O)) :
63     0 ≤ (((f h)⁻¹ • history f h : space f) : List (A × O) → ℝ) t := by
64   exact mul_nonneg (inv_nonneg.mpr hh.le) (hf.nonneg _)
65 
66 /-- A model law is not obtained from an invertible table alone. -/
67 theorem canonical_conditional_probability (h t : List (A × O)) (hh : 0 < f h) :
68     0 ≤ mass f (wordAction (branch f) t ((f h)⁻¹ • history f h)) ∧
69       mass f (wordAction (branch f) t ((f h)⁻¹ • history f h)) ≤ 1 := by
70   rw [conditional_test]
71   exact hf.conditional_bounds h t hh
72 
73 end CausalLaw
74 
75 /-- Known hidden instruments supply word-law hypotheses, not unknown-world inference. -/
76 theorem instrument_causal {I : Type*} [Fintype I]
77     (T : Instrument I A O) (p : I → ℝ) (hp : FiniteBayes.IsPrior p) :
78     CausalLaw (fun w => FiniteInstruments.mass (wordAction T.branch w p)) := by
79   refine ⟨?_,fun w => (T.word_probability w p hp).1, ?_⟩
80   · simpa only [wordAction_nil,LinearMap.id_apply] using mass_prior p hp
81   · intro h a
82     simp only [wordAction_append,wordAction_cons,wordAction_nil,LinearMap.id_comp,
83       LinearMap.comp_apply]
84     exact T.instrument_mass a _
85 
86 end Komorebi.LSM.Behavior

Back to source controls