BayesianDefect.lean

1 import KomorebiLSM.BayesianClosure
2 import Mathlib.Data.Matrix.Mul
3 
4 /-! P12's fixed-prior defect, including empty prior-mass blocks. -/
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}
10 variable [Fintype I] [Fintype A] [DecidableEq A]
11 
12 noncomputable def effectiveLikelihood (c : I → A) (p l : I → ℝ) (a : A) : ℝ :=
13   aggregate c (fun i => p i * l i) a / aggregate c p a
14 
15 omit [Fintype A] in
16 theorem zero_mass_weight (c : I → A) (p l : I → ℝ) (hp : ∀ i, 0 ≤ p i)
17     (a : A) (hz : aggregate c p a = 0) : aggregate c (fun i => p i * l i) a = 0 := by
18   have hpoint : ∀ i, c i = a → p i = 0 := by
19     intro i hi
20     have hn : ∀ j ∈ (Finset.univ : Finset I), 0 ≤ (if c j = a then p j else 0) := by
21       intro j _; split_ifs; exact hp j; exact le_rfl
22     have hh := Finset.single_le_sum hn (Finset.mem_univ i)
23     change (if c i = a then p i else 0) ≤ aggregate c p a at hh
24     rw [hz] at hh
25     exact le_antisymm (by simpa [hi] using hh) (hp i)
26   apply Finset.sum_eq_zero
27   intro i _
28   by_cases hi : c i = a
29   · simp [hi, hpoint i hi]
30   · simp [hi]
31 
32 omit [Fintype A] in
33 theorem effectiveLikelihood_product (c : I → A) (p l : I → ℝ)
34     (hp : ∀ i, 0 ≤ p i) (a : A) :
35     aggregate c p a * effectiveLikelihood c p l a = aggregate c (fun i => p i * l i) a := by
36   by_cases h : aggregate c p a = 0
37   · rw [h, zero_mul, zero_mass_weight c p l hp a h]
38   · unfold effectiveLikelihood
39     field_simp
40 
41 theorem effectiveLikelihood_evidence (c : I → A) (p l : I → ℝ)
42     (hp : ∀ i, 0 ≤ p i) :
43     evidence (aggregate c p) (effectiveLikelihood c p l) = evidence p l := by
44   simp only [evidence, effectiveLikelihood_product c p l hp, aggregate_sum]
45 
46 theorem aggregate_posterior_effective (c : I → A) (p l : I → ℝ)
47     (hp : ∀ i, 0 ≤ p i) :
48     aggregate c (posterior p l) = posterior (aggregate c p) (effectiveLikelihood c p l) := by
49   unfold posterior
50   rw [aggregate_div, effectiveLikelihood_evidence c p l hp]
51   funext a
52   rw [effectiveLikelihood_product c p l hp]
53 
54 omit [Fintype A] [DecidableEq A] in
55 theorem posterior_difference (p r b : I → ℝ)
56     (hr : evidence p r ≠ 0) (hb : evidence p b ≠ 0) (i : I) :
57     posterior p r i - posterior p b i =
58       (p i * (r i - b i) - posterior p b i * (∑ j, p j * (r j - b j))) / evidence p r := by
59   have he : (∑ j, p j * (r j - b j)) = evidence p r - evidence p b := by
60     simp [evidence, mul_sub, Finset.sum_sub_distrib]
61   rw [he]
62   unfold posterior
63   field_simp
64   ring
65 
66 theorem bayesian_coarsening_defect (c : I → A) (p l : I → ℝ) (b : A → ℝ)
67     (hp : ∀ i, 0 ≤ p i) (hlz : evidence p l ≠ 0)
68     (hbz : evidence (aggregate c p) b ≠ 0) (a : A) :
69     aggregate c (posterior p l) a - posterior (aggregate c p) b a =
70       (aggregate c p a * (effectiveLikelihood c p l a - b a) -
71         posterior (aggregate c p) b a *
72           (∑ k, aggregate c p k * (effectiveLikelihood c p l k - b k))) /
73           evidence (aggregate c p) (effectiveLikelihood c p l) := by
74   rw [aggregate_posterior_effective c p l hp]
75   exact posterior_difference (aggregate c p) (effectiveLikelihood c p l) b
76     (by rwa [effectiveLikelihood_evidence c p l hp]) hbz a
77 
78 omit [Fintype I] in
79 noncomputable def informationLossMatrix (p b : A → ℝ) : Matrix A A ℝ :=
80   Matrix.diagonal p - Matrix.vecMulVec (posterior p b) p
81 
82 omit [Fintype I] in
83 theorem informationLossMatrix_apply (p b d : A → ℝ) (a : A) :
84     (informationLossMatrix p b).mulVec d a =
85       p a * d a - posterior p b a * (∑ k, p k * d k) := by
86   simp [informationLossMatrix, Matrix.mulVec, dotProduct, sub_mul,
87     Finset.sum_sub_distrib, Matrix.diagonal, Matrix.vecMulVec, mul_assoc, ← Finset.mul_sum]
88 
89 theorem bayesian_coarsening_matrix_defect (c : I → A) (p l : I → ℝ) (b : A → ℝ)
90     (hp : ∀ i, 0 ≤ p i) (hlz : evidence p l ≠ 0)
91     (hbz : evidence (aggregate c p) b ≠ 0) :
92     (fun a => aggregate c (posterior p l) a - posterior (aggregate c p) b a) =
93       fun a => ((informationLossMatrix (aggregate c p) b).mulVec
94         (fun k => effectiveLikelihood c p l k - b k)) a /
95           evidence (aggregate c p) (effectiveLikelihood c p l) := by
96   funext a
97   rw [informationLossMatrix_apply]
98   exact bayesian_coarsening_defect c p l b hp hlz hbz a
99 
100 omit [Fintype I] in
101 theorem informationLossMatrix_scale_null (p b : A → ℝ) (hz : evidence p b ≠ 0) :
102     (informationLossMatrix p b).mulVec b = 0 := by
103   funext a
104   rw [informationLossMatrix_apply]
105   change p a * b a - (p a * b a / evidence p b) * evidence p b = 0
106   rw [div_mul_cancel₀ _ hz, sub_self]
107 
108 end Komorebi.LSM.FiniteBayes

Back to source controls