Bayes.lean

1 import MachineTheory.Instrument
2 import Mathlib.Tactic.FieldSimp
3 import Mathlib.Tactic.Linarith
4 
5 /-!
6 Core 3.4: reporting sufficiency for the actual joint experiment.
7 All posterior equalities below are guarded by positive event mass. Impossible retained
8 reports receive an arbitrary normalized reconstruction row, not a posterior belief.
9 The common reporting channel has no model argument.
10 -/
11 namespace Komorebi.MachineTheory
12 namespace Bayes
13 open scoped BigOperators
14 open Instrument
15 noncomputable section
16 variable {M O Z : Type*} [Fintype M]
17 
18 /-- Unnormalized Bayesian weights. -/
19 def weights (p l : M → ℝ) : M → ℝ := fun m => l m * p m
20 
21 def evidence (p l : M → ℝ) : ℝ := mass (weights p l)
22 
23 def update (p l : M → ℝ) : M → ℝ := normalize (weights p l)
24 
25 theorem evidence_nonneg (p l : M → ℝ) (hp : ∀ m, 0 ≤ p m) (hl : ∀ m, 0 ≤ l m) :
26     0 ≤ evidence p l :=
27   Finset.sum_nonneg (fun m _ => mul_nonneg (hl m) (hp m))
28 
29 theorem evidence_scale (p l : M → ℝ) (c : ℝ) :
30     evidence p (fun m => c * l m) = c * evidence p l := by
31   simp only [evidence, weights, mass, mul_assoc, ← Finset.mul_sum]
32 
33 theorem update_scale (p l : M → ℝ) (c : ℝ) (hc : c ≠ 0) :
34     update p (fun m => c * l m) = update p l := by
35   funext m
36   change (c * l m * p m) / evidence p (fun m => c * l m) =
37     (l m * p m) / evidence p l
38   rw [evidence_scale, mul_assoc, mul_div_mul_left _ _ hc]
39 
40 /-- Positive prior support makes an impossible event impossible in every model. -/
41 theorem likelihood_zero_of_evidence_zero (p l : M → ℝ)
42     (hp : ∀ m, 0 < p m) (hl : ∀ m, 0 ≤ l m) (he : evidence p l = 0) :
43     ∀ m, l m = 0 := by
44   have h := zero_of_zero_mass (weights p l)
45     (fun m => mul_nonneg (hl m) (le_of_lt (hp m))) he
46   intro m
47   have hz : l m * p m = 0 := congrFun h m
48   exact (mul_eq_zero.mp hz).resolve_right (ne_of_gt (hp m))
49 
50 theorem uniform_dist [Nonempty M] : IsDist (fun _ : M => (Fintype.card M : ℝ)⁻¹) := by
51   have hc : (0 : ℝ) < Fintype.card M := by exact_mod_cast Fintype.card_pos
52   constructor
53   · intro _; positivity
54   · simp only [mass, Finset.sum_const, Finset.card_univ, nsmul_eq_mul]
55     exact mul_inv_cancel₀ (ne_of_gt hc)
56 
57 theorem uniform_pos [Nonempty M] : 0 < (Fintype.card M : ℝ)⁻¹ := by
58   have hc : (0 : ℝ) < Fintype.card M := by exact_mod_cast Fintype.card_pos
59   positivity
60 
61 variable [Fintype O] [Fintype Z]
62 
63 structure ReportingModel (M O Z : Type*) [Fintype O] [Fintype Z] where
64   likelihood : M → O → ℝ
65   likelihood_nonneg : ∀ m o, 0 ≤ likelihood m o
66   likelihood_sum : ∀ m, ∑ o, likelihood m o = 1
67   channel : O → Z → ℝ
68   channel_nonneg : ∀ o z, 0 ≤ channel o z
69   channel_sum : ∀ o, ∑ z, channel o z = 1
70 
71 namespace ReportingModel
72 variable (E : ReportingModel M O Z)
73 
74 def raw (o : O) : M → ℝ := fun m => E.likelihood m o
75 
76 def joint (o : O) (z : Z) : M → ℝ := fun m => E.likelihood m o * E.channel o z
77 
78 def report (z : Z) : M → ℝ := fun m => ∑ o, E.joint o z m
79 
80 omit [Fintype M] in
81 theorem joint_nonneg (o : O) (z : Z) (m : M) : 0 ≤ E.joint o z m :=
82   mul_nonneg (E.likelihood_nonneg m o) (E.channel_nonneg o z)
83 
84 omit [Fintype M] in
85 theorem report_nonneg (z : Z) (m : M) : 0 ≤ E.report z m :=
86   Finset.sum_nonneg (fun o _ => E.joint_nonneg o z m)
87 
88 omit [Fintype M] in
89 theorem report_sum (m : M) : ∑ z, E.report z m = 1 := by
90   unfold report joint
91   rw [Finset.sum_comm]
92   simp_rw [← Finset.mul_sum, E.channel_sum, mul_one]
93   exact E.likelihood_sum m
94 
95 theorem joint_mass (p : M → ℝ) (o : O) (z : Z) :
96     evidence p (E.joint o z) = E.channel o z * evidence p (E.raw o) := by
97   have hf : E.joint o z = fun m => E.channel o z * E.raw o m := by
98     funext m; exact mul_comm _ _
99   rw [hf, evidence_scale]
100 
101 theorem report_mass (p : M → ℝ) (z : Z) :
102     evidence p (E.report z) = ∑ o, evidence p (E.joint o z) := by
103   simp only [evidence, mass, weights, report, Finset.sum_mul]
104   exact Finset.sum_comm
105 
106 theorem joint_le_report (p : M → ℝ) (hp : ∀ m, 0 ≤ p m) (o : O) (z : Z) :
107     evidence p (E.joint o z) ≤ evidence p (E.report z) := by
108   rw [E.report_mass]
109   exact Finset.single_le_sum
110     (fun o' _ => evidence_nonneg p _ hp (E.joint_nonneg o' z)) (Finset.mem_univ o)
111 
112 theorem positive_pair (p : M → ℝ) (hp : ∀ m, 0 ≤ p m) (o : O) (z : Z)
113     (h : 0 < evidence p (E.joint o z)) :
114     0 < E.channel o z ∧ 0 < evidence p (E.raw o) ∧ 0 < evidence p (E.report z) := by
115   have he := h
116   rw [E.joint_mass] at he
117   have hn := evidence_nonneg p (E.raw o) hp (fun m => E.likelihood_nonneg m o)
118   have hc := E.channel_nonneg o z
119   constructor
120   · exact lt_of_le_of_ne hc (fun hz => by rw [← hz, zero_mul] at he; exact (lt_irrefl 0) he)
121   constructor
122   · exact lt_of_le_of_ne hn (fun hz => by rw [← hz, mul_zero] at he; exact (lt_irrefl 0) he)
123   · exact lt_of_lt_of_le h (E.joint_le_report p hp o z)
124 
125 theorem joint_update_eq_raw (p : M → ℝ) (o : O) (z : Z)
126     (hb : E.channel o z ≠ 0) : update p (E.joint o z) = update p (E.raw o) := by
127   have hf : E.joint o z = fun m => E.channel o z * E.raw o m := by
128     funext m; exact mul_comm _ _
129   rw [hf, update_scale p (E.raw o) _ hb]
130 
131 /-- Equality on every positive-probability pair in the actual coupling. -/
132 def PreservesAt (p : M → ℝ) : Prop :=
133   ∀ o z, 0 < evidence p (E.joint o z) → update p (E.raw o) = update p (E.report z)
134 
135 def PreservesAll : Prop := ∀ p, IsDist p → E.PreservesAt p
136 
137 /-- This is an explicit reconstruction kernel, not an existence assumption. -/
138 def reconstruction [Nonempty O] (p : M → ℝ) (z : Z) (o : O) : ℝ :=
139   if 0 < evidence p (E.report z) then
140     evidence p (E.joint o z) / evidence p (E.report z)
141   else (Fintype.card O : ℝ)⁻¹
142 
143 def Reconstructs (ρ : Z → O → ℝ) : Prop :=
144   (∀ z o, 0 ≤ ρ z o) ∧ (∀ z, ∑ o, ρ z o = 1) ∧
145     ∀ m o z, E.joint o z m = E.report z m * ρ z o
146 
147 theorem reconstruction_nonneg [Nonempty O] (p : M → ℝ) (hp : ∀ m, 0 ≤ p m)
148     (z : Z) (o : O) : 0 ≤ E.reconstruction p z o := by
149   unfold reconstruction
150   split_ifs with hz
151   · exact div_nonneg (evidence_nonneg p _ hp (E.joint_nonneg o z)) (le_of_lt hz)
152   · positivity
153 
154 theorem reconstruction_sum [Nonempty O] (p : M → ℝ) (z : Z) :
155     ∑ o, E.reconstruction p z o = 1 := by
156   unfold reconstruction
157   by_cases hz : 0 < evidence p (E.report z)
158   · simp only [hz, ↓reduceIte, ← Finset.sum_div, ← E.report_mass]
159     exact div_self (ne_of_gt hz)
160   · simp only [hz, ↓reduceIte, Finset.sum_const, Finset.card_univ, nsmul_eq_mul]
161     have hc : (Fintype.card O : ℝ) ≠ 0 := by exact_mod_cast Fintype.card_ne_zero
162     exact mul_inv_cancel₀ hc
163 
164 /-- Full support is used only to cancel the prior and resolve impossible events modelwise. -/
165 theorem reconstruction_factor [Nonempty O] (p : M → ℝ) (hp : ∀ m, 0 < p m)
166     (hpres : E.PreservesAt p) :
167     ∀ m o z, E.joint o z m = E.report z m * E.reconstruction p z o := by
168   intro m o z
169   have hpn : ∀ m, 0 ≤ p m := fun m => le_of_lt (hp m)
170   have hjn := evidence_nonneg p (E.joint o z) hpn (E.joint_nonneg o z)
171   have hrn := evidence_nonneg p (E.report z) hpn (E.report_nonneg z)
172   by_cases hr : 0 < evidence p (E.report z)
173   · simp only [reconstruction, hr, ↓reduceIte]
174     by_cases hj : 0 < evidence p (E.joint o z)
175     · have hb := (E.positive_pair p hpn o z hj).1
176       have hpost : update p (E.joint o z) = update p (E.report z) :=
177         (E.joint_update_eq_raw p o z (ne_of_gt hb)).trans (hpres o z hj)
178       have he := congrFun hpost m
179       change (E.joint o z m * p m) / evidence p (E.joint o z) =
180         (E.report z m * p m) / evidence p (E.report z) at he
181       have hc := (div_eq_div_iff (ne_of_gt hj) (ne_of_gt hr)).mp he
182       have hc' : E.joint o z m * evidence p (E.report z) =
183           E.report z m * evidence p (E.joint o z) := by
184         apply (mul_right_cancel₀ (ne_of_gt (hp m)))
185         nlinarith [hc]
186       calc
187         E.joint o z m = (E.report z m * evidence p (E.joint o z)) /
188             evidence p (E.report z) := (eq_div_iff (ne_of_gt hr)).2 hc'
189         _ = E.report z m * (evidence p (E.joint o z) /
190             evidence p (E.report z)) := by rw [mul_div_assoc]
191     · have hz : evidence p (E.joint o z) = 0 := le_antisymm (le_of_not_gt hj) hjn
192       have h0 := likelihood_zero_of_evidence_zero p (E.joint o z) hp (E.joint_nonneg o z) hz
193       rw [h0 m, hz, zero_div, mul_zero]
194   · have hz : evidence p (E.report z) = 0 := le_antisymm (le_of_not_gt hr) hrn
195     have h0 := likelihood_zero_of_evidence_zero p (E.report z) hp (E.report_nonneg z) hz
196     have hjz : evidence p (E.joint o z) = 0 :=
197       le_antisymm ((E.joint_le_report p hpn o z).trans_eq hz) hjn
198     have hj0 := likelihood_zero_of_evidence_zero p (E.joint o z) hp (E.joint_nonneg o z) hjz
199     rw [hj0 m, h0 m, zero_mul]
200 
201 theorem reconstructs_of_full_support [Nonempty O] (p : M → ℝ)
202     (hp : ∀ m, 0 < p m) (hpres : E.PreservesAt p) :
203     E.Reconstructs (E.reconstruction p) :=
204   ⟨E.reconstruction_nonneg p (fun m => le_of_lt (hp m)),
205     E.reconstruction_sum p, E.reconstruction_factor p hp hpres⟩
206 
207 theorem preservesAll_of_reconstructs {ρ : Z → O → ℝ} (hρ : E.Reconstructs ρ) :
208     E.PreservesAll := by
209   intro p hp o z hj
210   have hp' := E.positive_pair p hp.1 o z hj
211   have hf : E.joint o z = fun m => ρ z o * E.report z m := by
212     funext m; rw [hρ.2.2 m o z, mul_comm]
213   have hrho : ρ z o ≠ 0 := by
214     intro hz
215     have he := hj
216     rw [hf, evidence_scale, hz, zero_mul] at he
217     exact (lt_irrefl 0) he
218   calc
219     update p (E.raw o) = update p (E.joint o z) :=
220       (E.joint_update_eq_raw p o z (ne_of_gt hp'.1)).symm
221     _ = update p (E.report z) := by rw [hf, update_scale p (E.report z) _ hrho]
222 
223 /-- Core 3.4: one specified full-support probability prior suffices for every prior. -/
224 theorem all_iff_full_support_prior [Nonempty O] (p : M → ℝ) (hp : IsDist p)
225     (hfull : ∀ m, 0 < p m) : E.PreservesAll ↔ E.PreservesAt p := by
226   constructor
227   · intro h; exact h p hp
228   · intro h; exact E.preservesAll_of_reconstructs (E.reconstructs_of_full_support p hfull h)
229 
230 /-- Core 3.4: all-prior posterior preservation iff a stochastic reconstruction
231 of the actual joint experiment exists, including impossible retained reports. -/
232 theorem all_iff_reconstruction [Nonempty M] [Nonempty O] :
233     E.PreservesAll ↔ ∃ ρ, E.Reconstructs ρ := by
234   constructor
235   · intro h
236     let p : M → ℝ := fun _ => (Fintype.card M : ℝ)⁻¹
237     exact ⟨E.reconstruction p, E.reconstructs_of_full_support p
238       (fun _ => uniform_pos (M := M)) (h p uniform_dist)⟩
239   · rintro ⟨ρ,hρ⟩; exact E.preservesAll_of_reconstructs hρ
240 
241 theorem all_iff_exists_full_support [Nonempty M] [Nonempty O] :
242     E.PreservesAll ↔ ∃ p, IsDist p ∧ (∀ m, 0 < p m) ∧ E.PreservesAt p := by
243   constructor
244   · intro h
245     exact ⟨_, uniform_dist, (fun _ => uniform_pos (M := M)), h _ uniform_dist⟩
246   · rintro ⟨p,hp,hfull,h⟩
247     exact (E.all_iff_full_support_prior p hp hfull).mpr h
248 
249 end ReportingModel
250 end
251 end Bayes
252 end Komorebi.MachineTheory

Back to source controls