FiniteStochastic.lean

1 import KomorebiLSM.JointRefinement
2 import KomorebiLSM.BayesianClosure
3 
4 /-! Actual stochastic quotient kernels and their prediction/update equations. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.FiniteBayes
7 open scoped BigOperators
8 universe u v
9 variable {I : Type u} {A : Type v} [Fintype I]
10 
11 def IsStochastic (K : I → I → ℝ) : Prop := ∀ i, IsPrior (K i)
12 
13 noncomputable def prediction (K : I → I → ℝ) (p : I → ℝ) (j : I) : ℝ :=
14   ∑ i, p i * K i j
15 
16 theorem pointMass_isPrior [DecidableEq I] (i : I) : IsPrior (pointMass i) := by
17   constructor
18   · intro j; simp only [pointMass]; positivity
19   · simp [pointMass]
20 
21 theorem prediction_pointMass [DecidableEq I] (K : I → I → ℝ) (i : I) :
22     prediction K (pointMass i) = K i := by
23   funext j
24   exact pointMass_test i (fun k => K k j)
25 
26 theorem prediction_isPrior (K : I → I → ℝ) (hK : IsStochastic K)
27     (p : I → ℝ) (hp : IsPrior p) : IsPrior (prediction K p) := by
28   constructor
29   · intro j
30     exact Finset.sum_nonneg (fun i _ => mul_nonneg (hp.1 i) ((hK i).1 j))
31   · simp only [prediction]
32     rw [Finset.sum_comm]
33     simp only [← Finset.mul_sum, (hK _).2, mul_one]
34     exact hp.2
35 
36 theorem aggregate_prediction [DecidableEq A] (c : I → A) (K : I → I → ℝ)
37     (p : I → ℝ) (a : A) :
38     aggregate c (prediction K p) a = ∑ i, p i * aggregate c (K i) a := by
39   unfold aggregate prediction
40   have h (j : I) : (if c j = a then ∑ i, p i * K i j else 0) =
41       ∑ i, if c j = a then p i * K i j else 0 := by
42     by_cases hh : c j = a <;> simp [hh]
43   simp only [h]
44   rw [Finset.sum_comm]
45   apply Finset.sum_congr rfl
46   intro i _
47   simp [Finset.mul_sum, mul_ite]
48 
49 theorem prediction_commutes_of_rows [Fintype A] [DecidableEq A]
50     (c : I → A) (K : I → I → ℝ) (Kb : A → A → ℝ)
51     (hrows : ∀ i, aggregate c (K i) = Kb (c i)) (p : I → ℝ) :
52     aggregate c (prediction K p) = prediction Kb (aggregate c p) := by
53   funext a
54   rw [aggregate_prediction]
55   simp only [hrows, prediction]
56   exact (aggregate_weighted_sum c p (fun j => Kb j a)).symm
57 
58 theorem prediction_rows_of_commutes [Fintype A] [DecidableEq A]
59     (c : I → A) (K : I → I → ℝ) (Kb : A → A → ℝ)
60     (hc : ∀ p, IsPrior p → aggregate c (prediction K p) = prediction Kb (aggregate c p))
61     (i : I) : aggregate c (K i) = Kb (c i) := by
62   classical
63   have h := hc (pointMass i) (pointMass_isPrior i)
64   rwa [prediction_pointMass, aggregate_pointMass, prediction_pointMass] at h
65 
66 end Komorebi.LSM.FiniteBayes
67 
68 namespace Komorebi.LSM.FinitePartitions
69 open scoped BigOperators
70 open FiniteBayes
71 universe u v w
72 variable {I : Type u} [Fintype I] {U : Type v} {Y : Type w}
73 
74 noncomputable def quotientKernel (K : U → I → I → ℝ) (r : Setoid I)
75     (h : Lumpable K r) (u : U) : Quotient r → Quotient r → ℝ :=
76   Quotient.lift (fun i => blockAggregate r (K u i)) (fun i j hij => h u i j hij)
77 
78 @[simp] theorem quotientKernel_mk (K : U → I → I → ℝ) (r : Setoid I)
79     (h : Lumpable K r) (u : U) (i : I) :
80     quotientKernel K r h u (Quotient.mk r i) = blockAggregate r (K u i) := rfl
81 
82 theorem quotientKernel_stochastic (K : U → I → I → ℝ) (r : Setoid I)
83     (h : Lumpable K r) (hK : ∀ u, IsStochastic (K u)) (u : U) :
84     IsStochastic (quotientKernel K r h u) := by
85   classical
86   intro q
87   induction q using Quotient.inductionOn with
88   | h i => exact aggregate_prior (Quotient.mk r) (K u i) (hK u i)
89 
90 theorem quotient_prediction_commutes (K : U → I → I → ℝ) (r : Setoid I)
91     (h : Lumpable K r) (u : U) (p : I → ℝ) :
92     blockAggregate r (prediction (K u) p) =
93       prediction (quotientKernel K r h u) (blockAggregate r p) := by
94   classical
95   exact prediction_commutes_of_rows (Quotient.mk r) (K u)
96     (quotientKernel K r h u) (fun _ => rfl) p
97 
98 omit [Fintype I] in
99 noncomputable def quotientLikelihood (l : Y → I → ℝ) (r : Setoid I)
100     (h : LikelihoodConstant l r) (y : Y) : Quotient r → ℝ :=
101   Quotient.lift (l y) (fun i j hij => h y i j hij)
102 
103 omit [Fintype I] in
104 @[simp] theorem quotientLikelihood_mk (l : Y → I → ℝ) (r : Setoid I)
105     (h : LikelihoodConstant l r) (y : Y) (i : I) :
106     quotientLikelihood l r h y (Quotient.mk r i) = l y i := rfl
107 
108 omit [Fintype I] in
109 theorem quotientLikelihood_pos (l : Y → I → ℝ) (r : Setoid I)
110     (h : LikelihoodConstant l r) (hl : ∀ y i, 0 < l y i) (y : Y) (q : Quotient r) :
111     0 < quotientLikelihood l r h y q := by
112   induction q using Quotient.inductionOn with
113   | h i => exact hl y i
114 
115 theorem quotient_bayes_commutes (l : Y → I → ℝ) (r : Setoid I)
116     (h : LikelihoodConstant l r) (y : Y) (p : I → ℝ) :
117     blockAggregate r (posterior p (l y)) =
118       posterior (blockAggregate r p) (quotientLikelihood l r h y) := by
119   classical
120   exact posterior_coarsening_pullback (Quotient.mk r) p (quotientLikelihood l r h y)
121 
122 omit [Fintype I] in
123 theorem nontrivial_refinement {r s : Setoid I} [Nontrivial (Quotient s)]
124     (h : r ≤ s) : Nontrivial (Quotient r) := by
125   obtain ⟨q1, q2, hq⟩ := exists_pair_ne (Quotient s)
126   obtain ⟨p1, hp1⟩ := coarsenMap_surjective h q1
127   obtain ⟨p2, hp2⟩ := coarsenMap_surjective h q2
128   refine ⟨⟨p1,p2,?_⟩⟩
129   intro he
130   exact hq (hp1.symm.trans ((congrArg (coarsenMap h) he).trans hp2))
131 
132 noncomputable def JointlyClosed (K : U → I → I → ℝ) (l : Y → I → ℝ)
133     (r : Setoid I) : Prop := by
134   classical
135   exact ∃ (Kb : U → Quotient r → Quotient r → ℝ) (lb : Y → Quotient r → ℝ),
136     (∀ u, IsStochastic (Kb u)) ∧ (∀ y q, 0 < lb y q) ∧
137     (∀ u p, IsPrior p → blockAggregate r (prediction (K u) p) =
138       prediction (Kb u) (blockAggregate r p)) ∧
139     (∀ y p, IsPrior p → blockAggregate r (posterior p (l y)) =
140       posterior (blockAggregate r p) (lb y))
141 
142 theorem joint_closed_iff (K : U → I → I → ℝ) (l : Y → I → ℝ) (r : Setoid I)
143     [Nontrivial (Quotient r)] (hK : ∀ u, IsStochastic (K u)) (hl : ∀ y i, 0 < l y i) :
144     JointlyClosed K l r ↔ Lumpable K r ∧ LikelihoodConstant l r := by
145   classical
146   constructor
147   · rintro ⟨Kb, lb, _, hlb, hpred, hbay⟩
148     constructor
149     · intro u i j hij
150       have hi := prediction_rows_of_commutes (Quotient.mk r) (K u) (Kb u) (hpred u) i
151       have hj := prediction_rows_of_commutes (Quotient.mk r) (K u) (Kb u) (hpred u) j
152       change blockAggregate r (K u i) = Kb u (Quotient.mk r i) at hi
153       change blockAggregate r (K u j) = Kb u (Quotient.mk r j) at hj
154       rw [hi, hj, Quotient.sound hij]
155     · intro y i j hij
156       exact likelihood_constant_on_fibers (Quotient.mk r) Quotient.mk_surjective
157         (l y) (lb y) (hl y) (hlb y) (hbay y) i j (Quotient.sound hij)
158   · rintro ⟨hk, hlik⟩
159     exact ⟨quotientKernel K r hk, quotientLikelihood l r hlik,
160       quotientKernel_stochastic K r hk hK, quotientLikelihood_pos l r hlik hl,
161       fun u p _ => quotient_prediction_commutes K r hk u p,
162       fun y p _ => quotient_bayes_commutes l r hlik y p⟩
163 
164 theorem jointRefinement_closed (K : U → I → I → ℝ) (l : Y → I → ℝ) (r : Setoid I)
165     (hK : ∀ u, IsStochastic (K u)) (hl : ∀ y i, 0 < l y i) :
166     JointlyClosed K l (jointRefinement K l r) := by
167   classical
168   let t := jointRefinement K l r
169   have hk : Lumpable K t := jointRefinement_lumpable K l r
170   have hlik : LikelihoodConstant l t := jointRefinement_likelihood K l r
171   exact ⟨quotientKernel K t hk, quotientLikelihood l t hlik,
172     quotientKernel_stochastic K t hk hK, quotientLikelihood_pos l t hlik hl,
173     fun u p _ => quotient_prediction_commutes K t hk u p,
174     fun y p _ => quotient_bayes_commutes l t hlik y p⟩
175 
176 theorem jointlyClosed_refines_completion (K : U → I → I → ℝ) (l : Y → I → ℝ)
177     (r s : Setoid I) [Nontrivial (Quotient r)]
178     (hK : ∀ u, IsStochastic (K u)) (hl : ∀ y i, 0 < l y i)
179     (hsr : s ≤ r) (hs : JointlyClosed K l s) : s ≤ jointRefinement K l r := by
180   let := nontrivial_refinement hsr
181   have h := (joint_closed_iff K l s hK hl).mp hs
182   exact jointRefinement_coarsest K l r s hsr h.1 h.2
183 
184 theorem coarsest_jointly_closed (K : U → I → I → ℝ) (l : Y → I → ℝ)
185     (r : Setoid I) [Nontrivial (Quotient r)]
186     (hK : ∀ u, IsStochastic (K u)) (hl : ∀ y i, 0 < l y i) :
187     ∃! t : Setoid I, t ≤ r ∧ JointlyClosed K l t ∧
188       ∀ s : Setoid I, s ≤ r → JointlyClosed K l s → s ≤ t := by
189   have htr := jointRefinement_refines K l r
190   have htc := jointRefinement_closed K l r hK hl
191   have hleast := jointlyClosed_refines_completion K l r
192   refine ⟨jointRefinement K l r, ⟨htr, htc, ?_⟩, ?_⟩
193   · intro s hsr hsc
194     exact hleast s hK hl hsr hsc
195   · intro s hs
196     exact le_antisymm (hleast s hK hl hs.1 hs.2.1)
197       (hs.2.2 (jointRefinement K l r) htr htc)
198 
199 end Komorebi.LSM.FinitePartitions

Back to source controls