BayesianLumping.lean

1 import MachineTheory.Bayes
2 import Mathlib.Data.Setoid.Basic
3 import Mathlib.Data.Fintype.EquivFin
4 
5 /-! Separate all-prior Bayesian updates are stronger than one chosen combined
6 transition/report schedule. Strictly positive likelihoods and a nontrivial retained
7 partition force the fine likelihood to be constant on retained fibres. -/
8 namespace Komorebi.MachineTheory
9 namespace BayesianLumping
10 open scoped BigOperators
11 open Instrument Bayes
12 noncomputable section
13 variable {X Z : Type*} [Fintype X] [Fintype Z] [DecidableEq X] [DecidableEq Z]
14 
15 def twoPoint (x y : X) : X → ℝ := fun u => (basis x u + basis y u) / 2
16 
17 omit [Fintype Z] [DecidableEq Z] in
18 theorem sum_twoPoint (f : X → ℝ) (x y : X) :
19     (∑ u, f u * twoPoint x y u) = (f x + f y) / 2 := by
20   simp only [twoPoint, ← mul_div_assoc, mul_add]
21   rw [← Finset.sum_div, Finset.sum_add_distrib]
22   simp [basis, mul_ite]
23 
24 omit [Fintype Z] [DecidableEq Z] in
25 theorem twoPoint_dist (x y : X) : IsDist (twoPoint x y) := by
26   constructor
27   · intro u; unfold twoPoint basis; positivity
28   · have h := sum_twoPoint (fun _ : X => (1 : ℝ)) x y
29     norm_num [mass] at h ⊢
30     exact h
31 
32 omit [Fintype Z] [DecidableEq Z] in
33 theorem evidence_twoPoint (l : X → ℝ) (x y : X) :
34     evidence (twoPoint x y) l = (l x + l y) / 2 := sum_twoPoint l x y
35 
36 omit [Fintype Z] in
37 theorem push_twoPoint (π : X → Z) (x y : X) :
38     push π (twoPoint x y) = twoPoint (π x) (π y) := by
39   funext z
40   have h := sum_twoPoint (fun u => if π u = z then (1 : ℝ) else 0) x y
41   simpa [push, twoPoint, basis, ite_mul, eq_comm] using h
42 
43 /-- The posterior mass of one of two distinct retained blocks. -/
44 theorem posterior_twoPoint (π : X → Z) (l : X → ℝ) (x y : X)
45     (hxy : π x ≠ π y) :
46     push π (update (twoPoint x y) l) (π x) = l x / (l x + l y) := by
47   rw [show update (twoPoint x y) l = normalize (weights (twoPoint x y) l) from rfl,
48     push_normalize]
49   simp only [normalize, mass_push]
50   change push π (weights (twoPoint x y) l) (π x) / evidence (twoPoint x y) l = _
51   rw [evidence_twoPoint]
52   have hn := sum_twoPoint (fun u => if π u = π x then l u else 0) x y
53   have hn' : push π (weights (twoPoint x y) l) (π x) = l x / 2 := by
54     simpa only [push, weights, ite_mul, zero_mul, ↓reduceIte, Ne.symm hxy, add_zero] using hn
55   rw [hn']
56   exact div_div_div_cancel_right₀ (by norm_num : (2 : ℝ) ≠ 0) _ _
57 
58 /-- The coarse posterior is determined by the coarse prior. This deliberately
59 asks for all priors, not only one reachable family. -/
60 def UpdateDetermined (π : X → Z) (l : X → ℝ) : Prop :=
61   ∀ p q, IsDist p → IsDist q → push π p = push π q →
62     push π (update p l) = push π (update q l)
63 
64 /-- Two attained blocks are essential. Positivity excludes degenerate zero-likelihood odds. -/
65 theorem likelihood_constant_on_fibres (π : X → Z) (l : X → ℝ)
66     (hl : ∀ x, 0 < l x) (hnt : ∃ u v, π u ≠ π v)
67     (hu : UpdateDetermined π l) : ∀ x y, π x = π y → l x = l y := by
68   intro x y hxy
69   obtain ⟨u,v,huv⟩ := hnt
70   have hz : ∃ z, π x ≠ π z := by
71     by_cases hx : π x = π u
72     · exact ⟨v, fun hh => huv (hx.symm.trans hh)⟩
73     · exact ⟨u,hx⟩
74   obtain ⟨z,hxz⟩ := hz
75   have hyz : π y ≠ π z := by simpa [← hxy] using hxz
76   have hpush : push π (twoPoint x z) = push π (twoPoint y z) := by
77     rw [push_twoPoint, push_twoPoint, hxy]
78   have h := congrFun (hu _ _ (twoPoint_dist x z) (twoPoint_dist y z) hpush) (π x)
79   rw [posterior_twoPoint π l x z hxz] at h
80   rw [hxy, posterior_twoPoint π l y z hyz] at h
81   have hxd : l x + l z ≠ 0 := ne_of_gt (add_pos (hl x) (hl z))
82   have hyd : l y + l z ≠ 0 := ne_of_gt (add_pos (hl y) (hl z))
83   have he := (div_eq_div_iff hxd hyd).mp h
84   have hprod : (l x - l y) * l z = 0 := by nlinarith
85   exact sub_eq_zero.mp ((mul_eq_zero.mp hprod).resolve_right (ne_of_gt (hl z)))
86 
87 omit [DecidableEq X] in
88 /-- Grouping the numerator and denominator commutes with exact correction. -/
89 theorem update_commutes_of_factored (π : X → Z) (l : X → ℝ) (g : Z → ℝ)
90     (hf : ∀ x, l x = g (π x)) (p : X → ℝ) :
91     push π (update p l) = update (push π p) g := by
92   have hw : push π (weights p l) = weights (push π p) g := by
93     funext z
94     simp only [push, weights, Finset.mul_sum]
95     apply Finset.sum_congr rfl
96     intro x _
97     split_ifs with hx
98     · rw [hf x, hx]
99     · simp
100   change push π (normalize (weights p l)) = normalize (weights (push π p) g)
101   rw [push_normalize, hw]
102 
103 omit [DecidableEq X] in
104 theorem update_determined_of_factored (π : X → Z) (l : X → ℝ) (g : Z → ℝ)
105     (hf : ∀ x, l x = g (π x)) : UpdateDetermined π l := by
106   intro p q _ _ hpq
107   rw [update_commutes_of_factored π l g hf p,
108       update_commutes_of_factored π l g hf q, hpq]
109 
110 /-- Core 3.5's Bayesian gate, with the coarse likelihood constructed on attained blocks. -/
111 theorem fixed_positive_coarse_iff (π : X → Z) (hπ : Function.Surjective π)
112     (l : X → ℝ) (hl : ∀ x, 0 < l x) (hnt : ∃ u v, π u ≠ π v) :
113     (∃ g : Z → ℝ, (∀ z, 0 < g z) ∧
114       ∀ p, IsDist p → push π (update p l) = update (push π p) g) ↔
115       (∀ x y, π x = π y → l x = l y) := by
116   constructor
117   · rintro ⟨g,_,hg⟩
118     apply likelihood_constant_on_fibres π l hl hnt
119     intro p q hp hq he
120     rw [hg p hp, hg q hq, he]
121   · intro h
122     let g : Z → ℝ := fun z => l (Classical.choose (hπ z))
123     have hf : ∀ x, l x = g (π x) :=
124       fun x => h x _ (Classical.choose_spec (hπ (π x))).symm
125     exact ⟨g,fun z => hl _,fun p _ => update_commutes_of_factored π l g hf p⟩
126 
127 end
128 end BayesianLumping
129 end Komorebi.MachineTheory

Back to source controls