Instrument.lean

1 import MachineTheory.Behavior
2 import Mathlib.Basic.Real.Basic
3 import Mathlib.Algebra.BigOperators.Field
4 import Mathlib.Tactic.Positivity
5 
6 /-!
7 Reviewed Core v0.2, Theorem 3.6.
8 Column convention: K a o y x is the joint probability of successor y and report o
9 conditional on initial x and action a. Report and transition marginals are not substituted
10 for this joint instrument. All laws are exact real-valued finite distributions.
11 -/
12 namespace Komorebi.MachineTheory
13 namespace Instrument
14 open scoped BigOperators
15 noncomputable section
16 
17 variable {X Z A O : Type*}
18 
19 def mass [Fintype X] (p : X → ℝ) : ℝ := ∑ x, p x
20 
21 def push [Fintype X] [DecidableEq Z] (π : X → Z) (p : X → ℝ) : Z → ℝ :=
22   fun z => ∑ x, if π x = z then p x else 0
23 
24 def applyKernel [Fintype X] (K : Z → X → ℝ) (p : X → ℝ) : Z → ℝ :=
25   fun z => ∑ x, K z x * p x
26 
27 def scale (c : ℝ) (p : X → ℝ) : X → ℝ := fun x => c * p x
28 
29 def basis [DecidableEq X] (i : X) : X → ℝ := fun x => if x = i then 1 else 0
30 
31 def normalize [Fintype X] (p : X → ℝ) : X → ℝ := fun x => p x / mass p
32 
33 def IsDist [Fintype X] (p : X → ℝ) : Prop := (∀ x, 0 ≤ p x) ∧ mass p = 1
34 
35 structure Law (X A O : Type*) [Fintype X] [Fintype O] where
36   kernel : A → O → X → X → ℝ
37   nonnegative : ∀ a o y x, 0 ≤ kernel a o y x
38   normalized : ∀ a x, (∑ o, ∑ y, kernel a o y x) = 1
39 
40 variable [Fintype X] [Fintype Z] [DecidableEq Z]
41 
42 /-- Aggregation preserves total mass for any real vector, including unnormalized ones. -/
43 theorem mass_push (π : X → Z) (p : X → ℝ) : mass (push π p) = mass p := by
44   unfold mass push
45   rw [Finset.sum_comm]
46   apply Finset.sum_congr rfl
47   intro x _
48   simp
49 
50 omit [Fintype Z] in
51 theorem push_scale (π : X → Z) (c : ℝ) (p : X → ℝ) :
52     push π (scale c p) = scale c (push π p) := by
53   funext z
54   simp only [push, scale, Finset.mul_sum, mul_ite, mul_zero]
55 
56 theorem mass_scale (c : ℝ) (p : X → ℝ) : mass (scale c p) = c * mass p := by
57   simp [mass, scale, Finset.mul_sum]
58 
59 omit [Fintype Z] in
60 theorem push_nonnegative (π : X → Z) (p : X → ℝ) (hp : ∀ x, 0 ≤ p x) :
61     ∀ z, 0 ≤ push π p z := by
62   intro z
63   apply Finset.sum_nonneg
64   intro x _
65   split_ifs <;> simp_all
66 
67 omit [Fintype Z] [DecidableEq Z] in
68 theorem apply_nonnegative (K : Z → X → ℝ) (hK : ∀ z x, 0 ≤ K z x)
69     (p : X → ℝ) (hp : ∀ x, 0 ≤ p x) : ∀ z, 0 ≤ applyKernel K p z := by
70   intro z
71   exact Finset.sum_nonneg (fun x _ => mul_nonneg (hK z x) (hp x))
72 
73 /-- Aggregation of a normalized nonnegative prior is a prior. -/
74 theorem push_dist (π : X → Z) (p : X → ℝ) (hp : IsDist p) : IsDist (push π p) :=
75   ⟨push_nonnegative π p hp.1, (mass_push π p).trans hp.2⟩
76 
77 omit [Fintype Z] in
78 theorem push_apply_expansion (π : X → Z) (K : X → X → ℝ) (p : X → ℝ) (z : Z) :
79     push π (applyKernel K p) z = ∑ x, (∑ y, if π y = z then K y x else 0) * p x := by
80   unfold push applyKernel
81   have hi : ∀ y, (if π y = z then ∑ x, K y x * p x else 0) =
82       ∑ x, (if π y = z then K y x else 0) * p x := by
83     intro y
84     split_ifs <;> simp_all
85   simp_rw [hi]
86   rw [Finset.sum_comm]
87   simp only [Finset.sum_mul]
88 
89 theorem apply_push_expansion (π : X → Z) (L : Z → Z → ℝ) (p : X → ℝ) (z : Z) :
90     applyKernel L (push π p) z = ∑ x, L z (π x) * p x := by
91   unfold applyKernel push
92   simp_rw [Finset.mul_sum, mul_ite, mul_zero]
93   rw [Finset.sum_comm]
94   apply Finset.sum_congr rfl
95   intro x _
96   simp
97 
98 omit [Fintype Z] [DecidableEq Z] in
99 theorem apply_basis [DecidableEq X] (K : Z → X → ℝ) (x : X) :
100     applyKernel K (basis x) = fun z => K z x := by
101   funext z
102   simp [applyKernel, basis]
103 
104 theorem basis_dist [DecidableEq X] (x : X) : IsDist (basis x) := by
105   constructor
106   · intro y
107     simp only [basis]
108     split_ifs <;> norm_num
109   · simp [mass, basis]
110 
111 /-- The literal column-fibre criterion, for a proposed coarse kernel. -/
112 def RowsMatch (π : X → Z) (K : X → X → ℝ) (L : Z → Z → ℝ) : Prop :=
113   ∀ z x, (∑ y, if π y = z then K y x else 0) = L z (π x)
114 
115 def Intertwines (π : X → Z) (K : X → X → ℝ) (L : Z → Z → ℝ) : Prop :=
116   ∀ p, push π (applyKernel K p) = applyKernel L (push π p)
117 
118 /-- Core 3.6: point-mass checking is equivalent to the full linear intertwining. -/
119 theorem intertwines_iff_rows (π : X → Z) (K : X → X → ℝ) (L : Z → Z → ℝ) :
120     Intertwines π K L ↔ RowsMatch π K L := by
121   classical
122   constructor
123   · intro h z x
124     have he := congrFun (h (basis x)) z
125     rw [push_apply_expansion, apply_push_expansion] at he
126     simpa [basis] using he
127   · intro h p
128     funext z
129     rw [push_apply_expansion, apply_push_expansion]
130     apply Finset.sum_congr rfl
131     intro x _
132     rw [h z x]
133 
134 /-- Probability priors suffice to identify the linear interface, since they include point masses. -/
135 theorem intertwines_of_priors (π : X → Z) (K : X → X → ℝ) (L : Z → Z → ℝ)
136     (h : ∀ p, IsDist p → push π (applyKernel K p) = applyKernel L (push π p)) :
137     Intertwines π K L := by
138   classical
139   apply (intertwines_iff_rows π K L).mpr
140   intro z x
141   have he := congrFun (h (basis x) (basis_dist x)) z
142   rw [push_apply_expansion, apply_push_expansion] at he
143   simpa [basis] using he
144 
145 
146 variable [Fintype O]
147 
148 /-- Report-indexed successor masses must be constant on each *input* fibre. -/
149 def FiberCriterion (π : X → Z) (K : A → O → X → X → ℝ) : Prop :=
150   ∀ a o z x y, π x = π y →
151     (∑ u, if π u = z then K a o u x else 0) =
152     (∑ u, if π u = z then K a o u y else 0)
153 
154 /-- Choose attained input representatives, then aggregate the joint columns. -/
155 def coarseLaw (π : X → Z) (hπ : Function.Surjective π) (K : Law X A O) : Law Z A O where
156   kernel a o z' z := ∑ y, if π y = z' then K.kernel a o y (Classical.choose (hπ z)) else 0
157   nonnegative a o z' z := by
158     apply Finset.sum_nonneg
159     intro y _
160     split_ifs
161     · exact K.nonnegative a o y _
162     · exact le_rfl
163   normalized a z := by
164     change (∑ o, mass (push π (fun y => K.kernel a o y (Classical.choose (hπ z))))) = 1
165     simp_rw [mass_push]
166     exact K.normalized a _
167 
168 /-- With the fibre condition, the constructed coarse law is a true intertwiner. -/
169 theorem coarseLaw_intertwines (π : X → Z) (hπ : Function.Surjective π)
170     (K : Law X A O) (hc : FiberCriterion π K.kernel) (a : A) (o : O) :
171     Intertwines π (K.kernel a o) ((coarseLaw π hπ K).kernel a o) := by
172   apply (intertwines_iff_rows _ _ _).mpr
173   intro z x
174   exact hc a o z x _ (Classical.choose_spec (hπ (π x))).symm
175 
176 /-- Core 3.6, existence of a normalized nonnegative coarse instrument iff the fibre criterion. -/
177 theorem quotient_exists_iff (π : X → Z) (hπ : Function.Surjective π) (K : Law X A O) :
178     (∃ L : Law Z A O, ∀ a o, Intertwines π (K.kernel a o) (L.kernel a o)) ↔
179       FiberCriterion π K.kernel := by
180   constructor
181   · rintro ⟨L, hL⟩ a o z x y hxy
182     have hrow := (intertwines_iff_rows π (K.kernel a o) (L.kernel a o)).mp (hL a o)
183     rw [hrow z x, hrow z y, hxy]
184   · intro hc
185     exact ⟨coarseLaw π hπ K, coarseLaw_intertwines π hπ K hc⟩
186 
187 /-- Surjectivity is used here: unobserved coarse input columns would not be identified. -/
188 theorem quotient_kernel_unique (π : X → Z) (hπ : Function.Surjective π)
189     (K : Law X A O) (L M : Law Z A O)
190     (hL : ∀ a o, Intertwines π (K.kernel a o) (L.kernel a o))
191     (hM : ∀ a o, Intertwines π (K.kernel a o) (M.kernel a o)) : L.kernel = M.kernel := by
192   funext a o z' z
193   obtain ⟨x, rfl⟩ := hπ z
194   exact ((intertwines_iff_rows _ _ _).mp (hL a o) z' x).symm.trans
195     ((intertwines_iff_rows _ _ _).mp (hM a o) z' x)
196 
197 /-- Algebraic normalization commutes with aggregation; probability meaning needs positive mass. -/
198 theorem push_normalize (π : X → Z) (p : X → ℝ) :
199     push π (normalize p) = normalize (push π p) := by
200   funext z
201   simp only [push, normalize, mass_push, Finset.sum_div]
202   apply Finset.sum_congr rfl
203   intro x _
204   split_ifs <;> simp_all
205 
206 theorem normalize_dist (p : X → ℝ) (hp : ∀ x, 0 ≤ p x) (hm : 0 < mass p) :
207     IsDist (normalize p) := by
208   constructor
209   · intro x
210     exact div_nonneg (hp x) (le_of_lt hm)
211   · change (∑ x, p x / mass p) = 1
212     rw [← Finset.sum_div]
213     exact div_self (ne_of_gt hm)
214 
215 /-- An impossible report has no posterior at the public interface. -/
216 def posterior? (p : X → ℝ) : Option (X → ℝ) :=
217   if 0 < mass p then some (normalize p) else none
218 
219 theorem report_mass_eq (π : X → Z) {K : X → X → ℝ} {L : Z → Z → ℝ}
220     (h : Intertwines π K L) (p : X → ℝ) :
221     mass (applyKernel K p) = mass (applyKernel L (push π p)) := by
222   rw [← mass_push π (applyKernel K p), h p]
223 
224 /-- Exact Bayesian correction for every positive-probability report, represented as an Option. -/
225 theorem posterior_transport (π : X → Z) {K : X → X → ℝ} {L : Z → Z → ℝ}
226     (h : Intertwines π K L) (p : X → ℝ) :
227     Option.map (push π) (posterior? (applyKernel K p)) =
228       posterior? (applyKernel L (push π p)) := by
229   unfold posterior?
230   rw [report_mass_eq π h p]
231   split_ifs
232   · simp only [Option.map_some]
233     congr 1
234     rw [push_normalize, h p]
235   · rfl
236 
237 /-- For nonnegative finite weights, zero total mass forces every weight to be zero. -/
238 theorem zero_of_zero_mass (p : X → ℝ) (hp : ∀ x, 0 ≤ p x) (hm : mass p = 0) :
239     p = fun _ => 0 := by
240   funext x
241   have h := (Finset.sum_eq_zero_iff_of_nonneg (fun y (_ : y ∈ (Finset.univ : Finset X)) => hp y)).mp hm
242   exact h x (Finset.mem_univ x)
243 
244 /-- Reverse direction: report probabilities and positive-report posteriors determine the joint interface. -/
245 theorem intertwines_of_mass_and_posteriors (π : X → Z)
246     (K : X → X → ℝ) (L : Z → Z → ℝ)
247     (hK : ∀ y x, 0 ≤ K y x) (hL : ∀ z' z, 0 ≤ L z' z)
248     (h : ∀ p, IsDist p →
249       mass (applyKernel K p) = mass (applyKernel L (push π p)) ∧
250       (0 < mass (applyKernel K p) →
251         push π (normalize (applyKernel K p)) = normalize (applyKernel L (push π p)))) :
252     Intertwines π K L := by
253   apply intertwines_of_priors
254   intro p hp
255   obtain ⟨hm, hn⟩ := h p hp
256   have hnn := apply_nonnegative K hK p hp.1
257   have hnn' := apply_nonnegative L hL (push π p) (push_nonnegative π p hp.1)
258   by_cases hz : mass (applyKernel K p) = 0
259   · have hu := zero_of_zero_mass _ hnn hz
260     have hv := zero_of_zero_mass _ hnn' (hm.symm.trans hz)
261     rw [hu, hv]
262     funext z
263     simp [push]
264   · have hmpos : 0 < mass (applyKernel K p) :=
265       lt_of_le_of_ne (Finset.sum_nonneg (fun x _ => hnn x)) (Ne.symm hz)
266     have he := hn hmpos
267     rw [push_normalize] at he
268     funext z
269     have hd := congrFun he z
270     simp only [normalize, mass_push] at hd
271     rw [← hm] at hd
272     calc
273       push π (applyKernel K p) z =
274           (push π (applyKernel K p) z / mass (applyKernel K p)) * mass (applyKernel K p) :=
275         (div_mul_cancel₀ _ hz).symm
276       _ = (applyKernel L (push π p) z / mass (applyKernel K p)) * mass (applyKernel K p) :=
277         congrArg (fun v => v * mass (applyKernel K p)) hd
278       _ = applyKernel L (push π p) z := div_mul_cancel₀ _ hz
279 
280 /-- Proof fields carry no extra choice: uniqueness of kernels is uniqueness of instruments. -/
281 theorem quotient_unique (π : X → Z) (hπ : Function.Surjective π)
282     (K : Law X A O) (L M : Law Z A O)
283     (hL : ∀ a o, Intertwines π (K.kernel a o) (L.kernel a o))
284     (hM : ∀ a o, Intertwines π (K.kernel a o) (M.kernel a o)) : L = M := by
285   have he := quotient_kernel_unique π hπ K L M hL hM
286   cases L
287   cases M
288   cases he
289   rfl
290 
291 /-- The report-probability / positive-posterior characterization is an iff, for actual laws. -/
292 theorem instrument_iff_reports_and_posteriors (π : X → Z)
293     (K : Law X A O) (L : Law Z A O) :
294     (∀ a o, Intertwines π (K.kernel a o) (L.kernel a o)) ↔
295     (∀ a o p, IsDist p →
296       mass (applyKernel (K.kernel a o) p) = mass (applyKernel (L.kernel a o) (push π p)) ∧
297       (0 < mass (applyKernel (K.kernel a o) p) →
298         push π (normalize (applyKernel (K.kernel a o) p)) =
299           normalize (applyKernel (L.kernel a o) (push π p)))) := by
300   constructor
301   · intro h a o p _
302     refine ⟨report_mass_eq π (h a o) p, ?_⟩
303     intro _
304     rw [push_normalize, h a o p]
305   · intro h a o
306     exact intertwines_of_mass_and_posteriors π (K.kernel a o) (L.kernel a o)
307       (K.nonnegative a o) (L.nonnegative a o) (h a o)
308 
309 end
310 end Instrument
311 end Komorebi.MachineTheory

Back to source controls