Block3Examples.lean

1 import KomorebiLSM.FiniteStochastic
2 import KomorebiLSM.BayesianDefect
3 import Mathlib.Tactic.NormNum
4 import Mathlib.Tactic.FinCases
5 import Mathlib.Algebra.BigOperators.Fin
6 
7 /-! Exact finite Bayesian defects, boundary cases and a six-state joint quotient. -/
8 set_option autoImplicit false
9 namespace Komorebi.LSM.Block3Examples
10 open scoped BigOperators
11 open FiniteBayes FinitePartitions
12 
13 def coarse3 (i : Fin 3) : Bool := decide (i.val = 2)
14 noncomputable def prior3 (i : Fin 3) : ℝ := if i.val = 0 then 1/2 else 1/4
15 def likelihood3 (i : Fin 3) : ℝ := if i.val = 0 then 1 else if i.val = 1 then 3 else 2
16 
17 theorem prior3_valid : IsPrior prior3 := by
18   constructor
19   · intro i; fin_cases i <;> norm_num [prior3]
20   · norm_num [prior3, Fin.sum_univ_succ]
21 
22 theorem likelihood3_positive : ∀ i, 0 < likelihood3 i := by
23   intro i; fin_cases i <;> norm_num [likelihood3]
24 
25 theorem prior3_coarse_masses :
26     aggregate coarse3 prior3 false = 3/4 ∧ aggregate coarse3 prior3 true = 1/4 := by
27   norm_num [aggregate, coarse3, prior3, Fin.sum_univ_succ]
28 
29 theorem prior3_effective_likelihood :
30     effectiveLikelihood coarse3 prior3 likelihood3 false = 5/3 ∧
31     effectiveLikelihood coarse3 prior3 likelihood3 true = 2 := by
32   norm_num [effectiveLikelihood, aggregate, coarse3, prior3, likelihood3, Fin.sum_univ_succ]
33 
34 theorem prior3_evidence : evidence prior3 likelihood3 = 7/4 := by
35   norm_num [evidence, prior3, likelihood3, Fin.sum_univ_succ]
36 
37 theorem prior3_updated_masses :
38     aggregate coarse3 (posterior prior3 likelihood3) false = 5/7 ∧
39     aggregate coarse3 (posterior prior3 likelihood3) true = 2/7 := by
40   norm_num [aggregate, posterior, evidence, coarse3, prior3, likelihood3, Fin.sum_univ_succ]
41 
42 theorem prior3_exact_defect :
43     aggregate coarse3 (posterior prior3 likelihood3) false -
44       posterior (aggregate coarse3 prior3) (fun _ => 1) false = -1/28 ∧
45     aggregate coarse3 (posterior prior3 likelihood3) true -
46       posterior (aggregate coarse3 prior3) (fun _ => 1) true = 1/28 := by
47   norm_num [aggregate, posterior, evidence, coarse3, prior3, likelihood3, Fin.sum_univ_succ]
48 
49 theorem prior3_updates_do_not_commute :
50     ¬ BayesCommutes coarse3 likelihood3 (fun _ => 1) := by
51   intro h
52   have he := congrFun (h prior3 prior3_valid) false
53   have hd := prior3_exact_defect.1
54   rw [he, sub_self] at hd
55   norm_num at hd
56 
57 noncomputable def balanced3 (i : Fin 3) : ℝ := if i.val = 2 then 1/2 else 1/4
58 
59 theorem one_prior_can_hide_a_defect :
60     aggregate coarse3 (posterior balanced3 likelihood3) =
61       posterior (aggregate coarse3 balanced3) (fun _ => 1) := by
62   funext a
63   cases a <;> norm_num [aggregate, posterior, evidence, coarse3, balanced3, likelihood3,
64     Fin.sum_univ_succ]
65 
66 theorem empty_mass_block_is_harmless :
67     effectiveLikelihood coarse3 (pointMass 0) likelihood3 true = 0 ∧
68     aggregate coarse3 (posterior (pointMass 0) likelihood3) true = 0 := by
69   norm_num [show (2 : Fin 3) ≠ 0 by decide, effectiveLikelihood, aggregate, posterior, evidence, coarse3, pointMass,
70     likelihood3, Fin.sum_univ_succ]
71 
72 def unequal2 (i : Fin 2) : ℝ := if i.val = 0 then 1 else 2
73 
74 theorem unequal2_positive : ∀ i, 0 < unequal2 i := by
75   intro i; fin_cases i <;> norm_num [unequal2]
76 
77 theorem one_block_commutes_with_unequal_likelihoods :
78     BayesCommutes (fun _ : Fin 2 => ()) unequal2 (fun _ => 1) :=
79   one_block_commutes unequal2 (fun _ => 1) unequal2_positive (fun _ => by norm_num)
80 
81 theorem one_block_global_scale_is_not_necessary :
82     ¬ ∃ s : ℝ, 0 < s ∧ ∀ i : Fin 2, unequal2 i = s * (1 : ℝ) := by
83   rintro ⟨s, _, h⟩
84   have h0 := h 0
85   have h1 := h 1
86   norm_num [unequal2] at h0 h1
87   linarith
88 
89 theorem zero_evidence_is_not_an_update :
90     ¬ IsPrior (posterior prior3 (fun _ => 0)) := by
91   intro h
92   have hs := h.2
93   norm_num [posterior, evidence] at hs
94 
95 
96 /-- One deterministic transition. States zero and one remain equivalent. -/
97 def next6 (i : Fin 6) : Fin 6 :=
98   if i.val = 0 then 3 else if i.val = 1 then 3 else if i.val = 2 then 5 else
99     if i.val = 3 then 0 else if i.val = 4 then 2 else 5
100 
101 def kernel6 (_ : Unit) (i : Fin 6) : Fin 6 → ℝ := pointMass (next6 i)
102 def likelihood6 (_ : Unit) (i : Fin 6) : ℝ := if i.val = 5 then 2 else 1
103 
104 def label0 (i : Fin 6) : Fin 2 := if i.val < 3 then 0 else 1
105 def label1 (i : Fin 6) : Fin 3 := if i.val < 3 then 0 else if i.val < 5 then 1 else 2
106 def label2 (i : Fin 6) : Fin 4 :=
107   if i.val < 2 then 0 else if i.val = 2 then 1 else if i.val < 5 then 2 else 3
108 def label3 (i : Fin 6) : Fin 5 :=
109   if i.val < 2 then 0 else if i.val = 2 then 1 else if i.val = 3 then 2 else if i.val = 4 then 3 else 4
110 
111 def partition0 : Setoid (Fin 6) := Setoid.ker label0
112 def partition1 : Setoid (Fin 6) := Setoid.ker label1
113 def partition2 : Setoid (Fin 6) := Setoid.ker label2
114 def partition3 : Setoid (Fin 6) := Setoid.ker label3
115 
116 @[simp] theorem partition0_rel (i j : Fin 6) : partition0 i j ↔ label0 i = label0 j := Iff.rfl
117 
118 @[simp] theorem partition1_rel (i j : Fin 6) : partition1 i j ↔ label1 i = label1 j := Iff.rfl
119 
120 @[simp] theorem partition2_rel (i j : Fin 6) : partition2 i j ↔ label2 i = label2 j := Iff.rfl
121 
122 @[simp] theorem partition3_rel (i j : Fin 6) : partition3 i j ↔ label3 i = label3 j := Iff.rfl
123 
124 theorem kernel6_stochastic : ∀ u, IsStochastic (kernel6 u) := by
125   intro u i
126   exact pointMass_isPrior (next6 i)
127 
128 theorem likelihood6_positive : ∀ y i, 0 < likelihood6 y i := by
129   intro y i
130   unfold likelihood6
131   split_ifs <;> norm_num
132 
133 theorem likelihood_split_six : likelihoodSplit partition0 likelihood6 = partition1 := by
134   apply Setoid.ext
135   intro i j
136   fin_cases i <;> fin_cases j <;>
137     norm_num [likelihoodSplit_rel, partition0_rel, partition1_rel, Setoid.ker_def, label0, label1, likelihood6]
138   all_goals decide
139 
140 theorem first_transition_split_six : transitionSplit kernel6 partition1 = partition2 := by
141   apply Setoid.ext
142   intro i j
143   change transitionSplit (fun (_ : Unit) x => pointMass (next6 x)) partition1 i j ↔ partition2 i j
144   rw [transitionSplit_deterministic]
145   fin_cases i <;> fin_cases j <;>
146     norm_num [partition1_rel, partition2_rel, Setoid.ker_def, label1, label2, next6]
147   all_goals decide
148 
149 theorem second_transition_split_six : transitionSplit kernel6 partition2 = partition3 := by
150   apply Setoid.ext
151   intro i j
152   change transitionSplit (fun (_ : Unit) x => pointMass (next6 x)) partition2 i j ↔ partition3 i j
153   rw [transitionSplit_deterministic]
154   fin_cases i <;> fin_cases j <;>
155     norm_num [partition2_rel, partition3_rel, Setoid.ker_def, label2, label3, next6]
156   all_goals decide
157 
158 theorem final_transition_split_six : transitionSplit kernel6 partition3 = partition3 := by
159   apply Setoid.ext
160   intro i j
161   change transitionSplit (fun (_ : Unit) x => pointMass (next6 x)) partition3 i j ↔ partition3 i j
162   rw [transitionSplit_deterministic]
163   fin_cases i <;> fin_cases j <;>
164     norm_num [partition3_rel, Setoid.ker_def, label3, next6]
165   all_goals decide
166 
167 theorem label0_surjective : Function.Surjective label0 := by
168   intro a
169   fin_cases a
170   · exact ⟨0, rfl⟩
171   · exact ⟨3, rfl⟩
172 
173 theorem label1_surjective : Function.Surjective label1 := by
174   intro a
175   fin_cases a
176   · exact ⟨0, rfl⟩
177   · exact ⟨3, rfl⟩
178   · exact ⟨5, rfl⟩
179 
180 theorem label2_surjective : Function.Surjective label2 := by
181   intro a
182   fin_cases a
183   · exact ⟨0, rfl⟩
184   · exact ⟨2, rfl⟩
185   · exact ⟨3, rfl⟩
186   · exact ⟨5, rfl⟩
187 
188 theorem label3_surjective : Function.Surjective label3 := by
189   intro a
190   fin_cases a
191   · exact ⟨0, rfl⟩
192   · exact ⟨2, rfl⟩
193   · exact ⟨3, rfl⟩
194   · exact ⟨4, rfl⟩
195   · exact ⟨5, rfl⟩
196 
197 theorem six_state_block_counts :
198     blockCount partition0 = 2 ∧ blockCount partition1 = 3 ∧
199     blockCount partition2 = 4 ∧ blockCount partition3 = 5 := by
200   exact ⟨blockCount_kernel label0 label0_surjective,
201     blockCount_kernel label1 label1_surjective,
202     blockCount_kernel label2 label2_surjective,
203     blockCount_kernel label3 label3_surjective⟩
204 
205 theorem six_state_actual_completion : jointRefinement kernel6 likelihood6 partition0 = partition3 := by
206   unfold jointRefinement
207   rw [likelihood_split_six]
208   unfold stableRefinement
209   rw [six_state_block_counts.2.1]
210   change refinementIter kernel6 partition1 3 = partition3
211   simp only [refinementIter_succ, refinementIter_zero, first_transition_split_six,
212     second_transition_split_six, final_transition_split_six]
213 
214 theorem six_state_joint_closure : JointlyClosed kernel6 likelihood6 partition3 := by
215   rw [← six_state_actual_completion]
216   exact jointRefinement_closed kernel6 likelihood6 partition0 kernel6_stochastic likelihood6_positive
217 
218 theorem two_states_remain_equivalent : partition3 0 1 := by
219   change label3 0 = label3 1
220   rfl
221 
222 theorem transition_distinction_is_retained : ¬ partition3 3 4 := by
223   change ¬ label3 3 = label3 4
224   decide
225 
226 theorem likelihood_split_is_not_prediction_closed : ¬ Lumpable kernel6 partition1 := by
227   intro h
228   have he := (transitionSplit_fixed_iff kernel6 partition1).mpr h
229   rw [first_transition_split_six] at he
230   have h02 : partition1 0 2 := by change label1 0 = label1 2; rfl
231   rw [← he] at h02
232   change label2 0 = label2 2 at h02
233   norm_num [label2] at h02
234 
235 theorem second_split_is_still_required : ¬ Lumpable kernel6 partition2 := by
236   intro h
237   have he := (transitionSplit_fixed_iff kernel6 partition2).mpr h
238   rw [second_transition_split_six] at he
239   have h34 : partition2 3 4 := by change label2 3 = label2 4; rfl
240   rw [← he] at h34
241   exact transition_distinction_is_retained h34
242 
243 theorem initial_partition_has_two_blocks : Nontrivial (Quotient partition0) := by
244   refine ⟨⟨Quotient.mk partition0 0, Quotient.mk partition0 5, ?_⟩⟩
245   intro he
246   have hr := Quotient.exact he
247   change label0 0 = label0 5 at hr
248   norm_num [label0] at hr
249 
250 theorem six_state_semantic_minimality (r : Setoid (Fin 6))
251     (hr : r ≤ partition0) (hc : JointlyClosed kernel6 likelihood6 r) : r ≤ partition3 := by
252   let := initial_partition_has_two_blocks
253   rw [← six_state_actual_completion]
254   exact jointlyClosed_refines_completion kernel6 likelihood6 partition0 r
255     kernel6_stochastic likelihood6_positive hr hc
256 
257 end Komorebi.LSM.Block3Examples
258 

Back to source controls