Feedback.lean

1 import MachineTheory.Instrument
2 
3 /-! Core 3.6, arbitrary finite feedback histories and normalization.
4 The same history-dependent policy is used by both realizations. Its probabilities
5 may depend on all prior observed actions/reports, but not on the hidden state.
6 -/
7 namespace Komorebi.MachineTheory.Instrument
8 open scoped BigOperators
9 noncomputable section
10 variable {X Z A O : Type*} [Fintype X] [Fintype Z]
11 
12 abbrev History (A O : Type*) := List (A × O)
13 
14 structure Policy (A O : Type*) [Fintype A] where
15   probability : History A O → A → ℝ
16   nonnegative : ∀ h a, 0 ≤ probability h a
17   normalized : ∀ h, ∑ a, probability h a = 1
18 
19 /-- Unnormalized state of one named future history, from a specified observed past. -/
20 def evolve (K : A → O → X → X → ℝ) (g : History A O → A → ℝ) :
21     History A O → History A O → (X → ℝ) → (X → ℝ)
22   | _, [], p => p
23   | past, (a, o) :: tail, p =>
24       evolve K g (past ++ [(a, o)]) tail (scale (g past a) (applyKernel (K a o) p))
25 
26 /-- The full joint instrument, not its separate marginals, propagates the same compressed history. -/
27 theorem feedback_unnormalized [DecidableEq Z] (π : X → Z)
28     (K : A → O → X → X → ℝ) (L : A → O → Z → Z → ℝ)
29     (g : History A O → A → ℝ) (h : ∀ a o, Intertwines π (K a o) (L a o))
30     (past events : History A O) (p : X → ℝ) :
31     push π (evolve K g past events p) = evolve L g past events (push π p) := by
32   induction events generalizing past p with
33   | nil => rfl
34   | cons event events ih =>
35     obtain ⟨a, o⟩ := event
36     simp only [evolve]
37     rw [ih, push_scale, h a o]
38 
39 /-- Equality of the probabilities of every finite joint action/report history. -/
40 theorem feedback_history_mass [DecidableEq Z] (π : X → Z)
41     (K : A → O → X → X → ℝ) (L : A → O → Z → Z → ℝ)
42     (g : History A O → A → ℝ) (h : ∀ a o, Intertwines π (K a o) (L a o))
43     (past events : History A O) (p : X → ℝ) :
44     mass (evolve K g past events p) = mass (evolve L g past events (push π p)) := by
45   rw [← mass_push π, feedback_unnormalized π K L g h]
46 
47 /-- Impossible histories are `none` on both sides; positive histories have equal coarse posteriors. -/
48 theorem feedback_posterior [DecidableEq Z] (π : X → Z)
49     (K : A → O → X → X → ℝ) (L : A → O → Z → Z → ℝ)
50     (g : History A O → A → ℝ) (h : ∀ a o, Intertwines π (K a o) (L a o))
51     (past events : History A O) (p : X → ℝ) :
52     Option.map (push π) (posterior? (evolve K g past events p)) =
53       posterior? (evolve L g past events (push π p)) := by
54   unfold posterior?
55   rw [feedback_history_mass π K L g h]
56   split_ifs
57   · simp only [Option.map_some]
58     congr 1
59     rw [push_normalize, feedback_unnormalized π K L g h]
60   · rfl
61 
62 variable [Fintype O]
63 
64 /-- Summing over reports returns exactly the input mass of a normalized instrument. -/
65 theorem report_mass_total (K : Law X A O) (a : A) (p : X → ℝ) :
66     (∑ o, mass (applyKernel (K.kernel a o) p)) = mass p := by
67   unfold mass applyKernel
68   calc
69     (∑ o, ∑ y, ∑ x, K.kernel a o y x * p x) =
70         ∑ o, ∑ x, ∑ y, K.kernel a o y x * p x := by
71       apply Finset.sum_congr rfl
72       intro o _
73       exact Finset.sum_comm
74     _ = ∑ x, ∑ o, ∑ y, K.kernel a o y x * p x := Finset.sum_comm
75     _ = ∑ x, (∑ o, ∑ y, K.kernel a o y x) * p x := by
76       simp only [Finset.sum_mul]
77     _ = ∑ x, p x := by simp_rw [K.normalized, one_mul]
78 
79 variable [Fintype A]
80 
81 /-- Sum over all possible future action/report branches of the declared depth. -/
82 def totalHistoryMass (K : Law X A O) (g : Policy A O) :
83     Nat → History A O → (X → ℝ) → ℝ
84   | 0, _, p => mass p
85   | n + 1, past, p => ∑ a, ∑ o,
86       totalHistoryMass K g n (past ++ [(a, o)])
87         (scale (g.probability past a) (applyKernel (K.kernel a o) p))
88 
89 /-- The policy and instrument produce a normalized finite-history law, not just matching weights. -/
90 theorem totalHistoryMass_eq (K : Law X A O) (g : Policy A O)
91     (n : Nat) (past : History A O) (p : X → ℝ) :
92     totalHistoryMass K g n past p = mass p := by
93   induction n generalizing past p with
94   | zero => rfl
95   | succ n ih =>
96     simp only [totalHistoryMass, ih, mass_scale]
97     simp_rw [← Finset.mul_sum, report_mass_total, ← Finset.sum_mul]
98     rw [g.normalized, one_mul]
99 
100 /-- Nonnegativity is maintained along every real observation history. -/
101 theorem evolve_nonnegative (K : Law X A O) (g : Policy A O)
102     (past events : History A O) (p : X → ℝ) (hp : ∀ x, 0 ≤ p x) :
103     ∀ x, 0 ≤ evolve K.kernel g.probability past events p x := by
104   induction events generalizing past p with
105   | nil => exact hp
106   | cons event events ih =>
107     obtain ⟨a, o⟩ := event
108     apply ih
109     intro x
110     exact mul_nonneg (g.nonnegative past a)
111       (apply_nonnegative _ (K.nonnegative a o) p hp x)
112 
113 /-- A positive history produces a genuine normalized posterior. -/
114 theorem positive_history_posterior_dist (K : Law X A O) (g : Policy A O)
115     (past events : History A O) (p : X → ℝ) (hp : IsDist p)
116     (hm : 0 < mass (evolve K.kernel g.probability past events p)) :
117     IsDist (normalize (evolve K.kernel g.probability past events p)) :=
118   normalize_dist _ (evolve_nonnegative K g past events p hp.1) hm
119 
120 /-- The main Core 3.6 endpoint: constructed coarse instrument, one lawful feedback policy,
121 all finite histories, equal probabilities, and exactly matched optional posteriors. -/
122 theorem quotient_feedback_law [DecidableEq Z] (π : X → Z) (hπ : Function.Surjective π)
123     (K : Law X A O) (hc : FiberCriterion π K.kernel) (g : Policy A O)
124     (p : X → ℝ) (events : History A O) :
125     let L := coarseLaw π hπ K
126     mass (evolve K.kernel g.probability [] events p) =
127       mass (evolve L.kernel g.probability [] events (push π p)) ∧
128     Option.map (push π) (posterior? (evolve K.kernel g.probability [] events p)) =
129       posterior? (evolve L.kernel g.probability [] events (push π p)) := by
130   let L := coarseLaw π hπ K
131   have h := coarseLaw_intertwines π hπ K hc
132   exact ⟨feedback_history_mass π K.kernel L.kernel g.probability h [] events p,
133     feedback_posterior π K.kernel L.kernel g.probability h [] events p⟩
134 
135 /-- A common observed-history policy may instead issue one of finitely many terminal decisions. -/
136 structure StoppingPolicy (A O D : Type*) [Fintype A] [Fintype D] where
137   continueProb : History A O → A → ℝ
138   stopProb : History A O → D → ℝ
139   continue_nonnegative : ∀ h a, 0 ≤ continueProb h a
140   stop_nonnegative : ∀ h d, 0 ≤ stopProb h d
141   normalized : ∀ h, (∑ a, continueProb h a) + (∑ d, stopProb h d) = 1
142 
143 variable {D : Type*} [Fintype D]
144 
145 /-- Joint unnormalized state of a complete finite history and its terminal decision. -/
146 def stoppedState (K : A → O → X → X → ℝ) (g : StoppingPolicy A O D)
147     (events : History A O) (d : D) (p : X → ℝ) : X → ℝ :=
148   scale (g.stopProb events d) (evolve K g.continueProb [] events p)
149 
150 /-- Core 3.6's terminal-choice extension uses the same continuation and stopping probabilities. -/
151 theorem stopped_feedback [DecidableEq Z] (π : X → Z)
152     (K : Law X A O) (L : Law Z A O)
153     (h : ∀ a o, Intertwines π (K.kernel a o) (L.kernel a o))
154     (g : StoppingPolicy A O D) (events : History A O) (d : D) (p : X → ℝ) :
155     push π (stoppedState K.kernel g events d p) =
156       stoppedState L.kernel g events d (push π p) := by
157   unfold stoppedState
158   rw [push_scale, feedback_unnormalized π K.kernel L.kernel g.continueProb h]
159 
160 /-- Terminal decisions preserve the probabilities of complete finite records. -/
161 theorem stopped_history_mass [DecidableEq Z] (π : X → Z)
162     (K : Law X A O) (L : Law Z A O)
163     (h : ∀ a o, Intertwines π (K.kernel a o) (L.kernel a o))
164     (g : StoppingPolicy A O D) (events : History A O) (d : D) (p : X → ℝ) :
165     mass (stoppedState K.kernel g events d p) =
166       mass (stoppedState L.kernel g events d (push π p)) := by
167   rw [← mass_push π, stopped_feedback π K L h]
168 
169 /-- Sum stopped branches and surviving active mass at a finite cutoff.
170 It deliberately does not assert eventual termination of an arbitrary policy. -/
171 def stoppedAndSurvivingMass (K : Law X A O) (g : StoppingPolicy A O D) :
172     Nat → History A O → (X → ℝ) → ℝ
173   | 0, _, p => mass p
174   | n + 1, past, p => (∑ d, mass (scale (g.stopProb past d) p)) +
175       ∑ a, ∑ o, stoppedAndSurvivingMass K g n (past ++ [(a, o)])
176         (scale (g.continueProb past a) (applyKernel (K.kernel a o) p))
177 
178 theorem stoppedAndSurvivingMass_eq (K : Law X A O) (g : StoppingPolicy A O D)
179     (n : Nat) (past : History A O) (p : X → ℝ) :
180     stoppedAndSurvivingMass K g n past p = mass p := by
181   induction n generalizing past p with
182   | zero => rfl
183   | succ n ih =>
184     simp only [stoppedAndSurvivingMass, ih, mass_scale]
185     simp_rw [← Finset.mul_sum, report_mass_total, ← Finset.sum_mul]
186     rw [← add_mul, add_comm (∑ d, g.stopProb past d), g.normalized, one_mul]
187 
188 end
189 end Komorebi.MachineTheory.Instrument

Back to source controls