MissingIntervention.lean

1 import KomorebiLSM.BehaviorProbability
2 import Mathlib.Tactic.NormNum
3 import Mathlib.Tactic.FinCases
4 import Mathlib.Algebra.BigOperators.Fin
5 
6 /-! P31: actual one-state stochastic instruments agree on every passive record
7 and disagree under an unobserved intervention. False is action a, true is b.
8 The model tag specifies the deterministic observation under action b. -/
9 set_option autoImplicit false
10 namespace Komorebi.LSM.MissingIntervention
11 open scoped BigOperators
12 open FiniteInstruments
13 
14 /-- One hidden state, two actions and two observations. -/
15 noncomputable def model (tag : Bool) : Instrument (Fin 1) Bool Bool where
16   matrix a o _ _ := if a then (if o = tag then 1 else 0) else 1/2
17   nonneg := by
18     intro a o j i
19     cases a <;> cases o <;> cases tag <;> norm_num
20   mass_one := by
21     intro a i
22     cases a <;> cases tag <;> norm_num [Fin.sum_univ_succ, Fintype.sum_bool]
23 
24 /-- The unique hidden state has probability one. -/
25 def initial : Fin 1 → ℝ := fun _ => 1
26 
27 theorem initial_valid : FiniteBayes.IsPrior initial := by
28   constructor
29   · intro i; norm_num [initial]
30   · norm_num [initial, Fin.sum_univ_succ]
31 
32 /-- Chronological word probabilities of the actual instruments. -/
33 noncomputable def process (tag : Bool) (w : List (Bool × Bool)) : ℝ :=
34   mass (wordAction (model tag).branch w initial)
35 
36 theorem process_causal (tag : Bool) : Behavior.CausalLaw (process tag) :=
37   Behavior.instrument_causal (model tag) initial initial_valid
38 
39 theorem process_bounds (tag : Bool) (w : List (Bool × Bool)) :
40     0 ≤ process tag w ∧ process tag w ≤ 1 :=
41   (process_causal tag).word_bounds w
42 
43 /-- Each a-branch multiplies every unnormalized state by one half. -/
44 theorem branch_a (tag o : Bool) (p : Fin 1 → ℝ) :
45     (model tag).branch (false, o) p = (1/2 : ℝ) • p := by
46   funext j
47   fin_cases j
48   simp [Instrument.branch_apply, model]
49 
50 /-- All lengths and all observation records, not a finite test fixture. -/
51 theorem passive_word_state (tag : Bool) (os : List Bool) (p : Fin 1 → ℝ) :
52     wordAction (model tag).branch (os.map (fun o => (false, o))) p =
53       ((1/2 : ℝ) ^ os.length) • p := by
54   induction os with
55   | nil => simp
56   | cons o os ih =>
57     simp only [List.map_cons, List.length_cons, wordAction_cons, LinearMap.comp_apply]
58     rw [branch_a, map_smul, ih]
59     simp [smul_smul, pow_succ, mul_comm]
60 
61 /-- Every length-k a-only record has probability 2^(-k). -/
62 theorem passive_word_probability (tag : Bool) (os : List Bool) :
63     process tag (os.map (fun o => (false, o))) = (1/2 : ℝ) ^ os.length := by
64   unfold process
65   rw [passive_word_state, map_smul, mass_prior initial initial_valid]
66   simp
67 
68 theorem passive_agreement (os : List Bool) :
69     process false (os.map (fun o => (false, o))) =
70       process true (os.map (fun o => (false, o))) := by
71   rw [passive_word_probability, passive_word_probability]
72 
73 /-- One unseen intervention distinguishes the two models with certainty. -/
74 theorem intervention_disagreement :
75     process false [(true, false)] = 1 ∧ process true [(true, false)] = 0 := by
76   norm_num [process, wordAction, Instrument.branch_apply, model, initial,
77     mass_apply, Fin.sum_univ_succ]
78 
79 theorem full_laws_distinct : process false ≠ process true := by
80   intro h
81   have hw := congrFun h [(true, false)]
82   rw [intervention_disagreement.1, intervention_disagreement.2] at hw
83   norm_num at hw
84 
85 /-- P31's existential form, with validity supplied by the Instrument type. -/
86 theorem missing_intervention_nonidentifiability :
87     ∃ T₀ T₁ : Instrument (Fin 1) Bool Bool,
88       (∀ os : List Bool,
89         mass (wordAction T₀.branch (os.map (fun o => (false, o))) initial) =
90         mass (wordAction T₁.branch (os.map (fun o => (false, o))) initial)) ∧
91       mass (wordAction T₀.branch [(true, false)] initial) = 1 ∧
92       mass (wordAction T₁.branch [(true, false)] initial) = 0 := by
93   exact ⟨model false, model true, passive_agreement,
94     intervention_disagreement.1, intervention_disagreement.2⟩
95 
96 /-- Even the complete exact passive probability law cannot determine the
97 unrestricted controlled law for both models. This is not a sample-size bound. -/
98 theorem no_passive_identification
99     (learn : (List Bool → ℝ) → List (Bool × Bool) → ℝ) :
100     ¬ ((learn (fun os : List Bool => process false (os.map (fun o => (false, o)))) = process false) ∧
101        (learn (fun os : List Bool => process true (os.map (fun o => (false, o)))) = process true)) := by
102   rintro ⟨h₀, h₁⟩
103   have hp : (fun os : List Bool => process false (os.map (fun o => (false, o)))) =
104       (fun os : List Bool => process true (os.map (fun o => (false, o)))) :=
105     funext passive_agreement
106   exact full_laws_distinct (h₀.symm.trans ((congrArg learn hp).trans h₁))
107 
108 end Komorebi.LSM.MissingIntervention

Back to source controls