BayesianClosure.lean

1 import KomorebiLSM.FiniteBayes
2 
3 /-! P12: exact all-prior closure, with nonempty blocks and the one-block boundary. -/
4 set_option autoImplicit false
5 namespace Komorebi.LSM.FiniteBayes
6 open scoped BigOperators
7 universe u v
8 variable {I : Type u} {A : Type v}
9 variable [Fintype I] [Fintype A] [DecidableEq A]
10 
11 def BayesCommutes (c : I → A) (l : I → ℝ) (b : A → ℝ) : Prop :=
12   ∀ p, IsPrior p → aggregate c (posterior p l) = posterior (aggregate c p) b
13 
14 theorem cross_ratio_of_commutes (c : I → A) (l : I → ℝ) (b : A → ℝ)
15     (hl : ∀ i, 0 < l i) (hb : ∀ a, 0 < b a) (hc : BayesCommutes c l b)
16     (i j : I) (hij : c i ≠ c j) : l i * b (c j) = l j * b (c i) := by
17   classical
18   have h := congrFun (hc (pairPrior i j) (pairPrior_isPrior i j)) (c i)
19   rw [aggregate_pair_posterior c i j hij l hl, aggregate_pairPrior] at h
20   have ht := aggregate_pair_posterior id (c i) (c j) hij b hb
21   rw [aggregate_id] at ht
22   change posterior (pairPrior (c i) (c j)) b (c i) = _ at ht
23   rw [ht] at h
24   have hz := ne_of_gt (add_pos (hl i) (hl j))
25   have hbz := ne_of_gt (add_pos (hb (c i)) (hb (c j)))
26   have hmul := (div_eq_div_iff hz hbz).mp h
27   nlinarith
28 
29 theorem ratio_constant_of_commutes [Nontrivial A] (c : I → A)
30     (csurj : Function.Surjective c) (l : I → ℝ) (b : A → ℝ)
31     (hl : ∀ i, 0 < l i) (hb : ∀ a, 0 < b a) (hc : BayesCommutes c l b) :
32     ∀ i j, l i / b (c i) = l j / b (c j) := by
33   have hd : ∀ i j, c i ≠ c j → l i / b (c i) = l j / b (c j) := by
34     intro i j hij
35     exact (div_eq_div_iff (ne_of_gt (hb (c i))) (ne_of_gt (hb (c j)))).mpr
36       (cross_ratio_of_commutes c l b hl hb hc i j hij)
37   intro i j
38   by_cases hij : c i = c j
39   · obtain ⟨a, ha⟩ := exists_ne (c i)
40     obtain ⟨k, hk⟩ := csurj a
41     have hik : c i ≠ c k := by simpa [hk] using Ne.symm ha
42     have hjk : c j ≠ c k := by rw [← hij]; exact hik
43     exact (hd i k hik).trans (hd j k hjk).symm
44   · exact hd i j hij
45 
46 theorem bayesian_coarsening_iff [Nontrivial A] (c : I → A)
47     (csurj : Function.Surjective c) (l : I → ℝ) (b : A → ℝ)
48     (hl : ∀ i, 0 < l i) (hb : ∀ a, 0 < b a) :
49     BayesCommutes c l b ↔ ∃ s : ℝ, 0 < s ∧ ∀ i, l i = s * b (c i) := by
50   constructor
51   · intro hc
52     obtain ⟨a0, a1, hne⟩ := exists_pair_ne A
53     obtain ⟨i0, hi0⟩ := csurj a0
54     refine ⟨l i0 / b (c i0), div_pos (hl i0) (hb (c i0)), ?_⟩
55     intro i
56     exact (div_eq_iff (ne_of_gt (hb (c i)))).mp
57       (ratio_constant_of_commutes c csurj l b hl hb hc i i0)
58   · rintro ⟨s, hs, hls⟩ p _
59     exact posterior_coarsening_scaled c p l b s (ne_of_gt hs) hls
60 
61 theorem likelihood_constant_on_fibers [Nontrivial A] (c : I → A)
62     (csurj : Function.Surjective c) (l : I → ℝ) (b : A → ℝ)
63     (hl : ∀ i, 0 < l i) (hb : ∀ a, 0 < b a) (hc : BayesCommutes c l b)
64     (i j : I) (hij : c i = c j) : l i = l j := by
65   obtain ⟨s, _, hs⟩ := (bayesian_coarsening_iff c csurj l b hl hb).mp hc
66   rw [hs i, hs j, hij]
67 
68 omit [Fintype A] [DecidableEq A] in
69 theorem one_block_posterior (p l : I → ℝ) (hz : evidence p l ≠ 0) :
70     aggregate (fun _ : I => ()) (posterior p l) () = 1 := by
71   simpa [aggregate] using posterior_sum p l hz
72 
73 omit [Fintype A] [DecidableEq A] in
74 theorem one_block_commutes (l : I → ℝ) (b : Unit → ℝ)
75     (hl : ∀ i, 0 < l i) (hb : ∀ a, 0 < b a) :
76     BayesCommutes (fun _ : I => ()) l b := by
77   intro p hp
78   funext a
79   cases a
80   rw [one_block_posterior p l (ne_of_gt (evidence_pos p l hp hl))]
81   simp [posterior, evidence, aggregate, hp.2, ne_of_gt (hb ())]
82 
83 end Komorebi.LSM.FiniteBayes

Back to source controls