FiniteBayes.lean

1 import Mathlib.Analysis.SpecialFunctions.ExpDeriv
2 import Mathlib.Tactic
3 
4 /-! Author: Komorebi P. Finite Bayesian normalization with explicit evidence conditions. -/
5 namespace KomorebiPaperVI.FiniteBayes
6 open scoped BigOperators
7 variable {I : Type*} [Fintype I]
8 
9 def mass (p : I → ℝ) : ℝ := ∑ i, p i
10 noncomputable def normalize (p : I → ℝ) (i : I) : ℝ := p i / mass p
11 def evidence (p l : I → ℝ) : ℝ := ∑ i, l i*p i
12 noncomputable def update (p l : I → ℝ) (i : I) : ℝ := l i*p i / evidence p l
13 def l1 (p : I → ℝ) : ℝ := ∑ i, |p i|
14 
15 theorem normalized_mass (p : I → ℝ) (hp : mass p ≠ 0) : mass (normalize p) = 1 := by
16   simp only [mass, normalize, ← Finset.sum_div]
17   exact div_self hp
18 
19 theorem posterior_mass (p l : I → ℝ) (hz : evidence p l ≠ 0) : mass (update p l) = 1 := by
20   simp only [mass, update, ← Finset.sum_div]
21   exact div_self hz
22 
23 theorem posterior_nonnegative (p l : I → ℝ) (hp : ∀ i, 0 ≤ p i)
24     (hl : ∀ i, 0 ≤ l i) (hz : 0 < evidence p l) (i : I) : 0 ≤ update p l i :=
25   div_nonneg (mul_nonneg (hl i) (hp i)) hz.le
26 
27 theorem evidence_scale (p l : I → ℝ) (c : ℝ) :
28     evidence p (fun i => c*l i) = c*evidence p l := by
29   simp only [evidence, Finset.mul_sum, mul_assoc]
30 
31 theorem posterior_scale (p l : I → ℝ) (c : ℝ) (hc : c ≠ 0)
32     (hz : evidence p l ≠ 0) : update p (fun i => c*l i) = update p l := by
33   funext i
34   simp only [update, evidence_scale]
35   field_simp
36 
37 theorem sequential_evidence (p l k : I → ℝ) :
38     evidence (update p l) k = evidence p (fun i => l i*k i) / evidence p l := by
39   simp only [evidence, update, ← mul_div_assoc, ← Finset.sum_div]
40   congr 1
41   apply Finset.sum_congr rfl
42   intro i _
43   ring
44 
45 theorem posterior_composition (p l k : I → ℝ) (hz : evidence p l ≠ 0)
46     (hzk : evidence p (fun i => l i*k i) ≠ 0) :
47     update (update p l) k = update p (fun i => l i*k i) := by
48   funext i
49   rw [update, sequential_evidence]
50   dsimp [update]
51   field_simp
52 
53 theorem posterior_difference (p l k : I → ℝ) (hl : evidence p l ≠ 0)
54     (hk : evidence p k ≠ 0) (i : I) :
55     update p l i-update p k i =
56       (p i*(l i-k i)-update p k i*(∑ j, p j*(l j-k j))) / evidence p l := by
57   have hs : (∑ j, p j*(l j-k j)) = evidence p l-evidence p k := by
58     simp only [evidence, mul_sub, Finset.sum_sub_distrib]
59     congr 1 <;> apply Finset.sum_congr rfl <;> intros <;> ring
60   rw [hs]
61   dsimp [update]
62   field_simp
63   ring
64 
65 theorem scale_null_direction (p k : I → ℝ) (hk : evidence p k ≠ 0) (i : I) :
66     p i*k i-update p k i*(∑ j, p j*k j)=0 := by
67   have hs : (∑ j, p j*k j) = evidence p k := by simp [evidence, mul_comm]
68   rw [hs]
69   dsimp [update]
70   field_simp
71   ring
72 
73 theorem normalized_l1_bound_left (w v : I → ℝ) (hv : ∀ i, 0 ≤ v i)
74     (hW : 0 < mass w) (hV : 0 < mass v) :
75     l1 (fun i => normalize w i-normalize v i) ≤
76       2*l1 (fun i => w i-v i)/mass w := by
77   have hd : |mass v-mass w| ≤ l1 (fun i => w i-v i) := by
78     rw [mass, mass, ← Finset.sum_sub_distrib]
79     simpa only [l1, abs_sub_comm] using Finset.abs_sum_le_sum_abs (fun i => v i-w i) Finset.univ
80   have point (i : I) : |normalize w i-normalize v i| ≤
81       |w i-v i|/mass w + (v i/mass v)*(|mass v-mass w|/mass w) := by
82     have he : normalize w i-normalize v i =
83         (w i-v i)/mass w+(v i/mass v)*((mass v-mass w)/mass w) := by
84       dsimp [normalize]
85       field_simp
86       ring
87     rw [he]
88     calc
89       _ ≤ |(w i-v i)/mass w|+|(v i/mass v)*((mass v-mass w)/mass w)| := abs_add_le _ _
90       _ = _ := by simp only [abs_mul, abs_div, abs_of_pos hW, abs_of_pos hV, abs_of_nonneg (hv i)]
91   calc
92     _ ≤ ∑ i, (|w i-v i|/mass w+(v i/mass v)*(|mass v-mass w|/mass w)) :=
93       Finset.sum_le_sum (fun i _ => point i)
94     _ = l1 (fun i => w i-v i)/mass w+|mass v-mass w|/mass w := by
95       rw [Finset.sum_add_distrib, ← Finset.sum_div, ← Finset.sum_mul, ← Finset.sum_div]
96       simp only [mass, l1] at *
97       rw [div_self (ne_of_gt hV), one_mul]
98     _ ≤ l1 (fun i => w i-v i)/mass w+l1 (fun i => w i-v i)/mass w :=
99       add_le_add_right (div_le_div_of_nonneg_right hd hW.le) _
100     _ = _ := by ring
101 
102 theorem likelihood_perturbation_bound (p l k : I → ℝ)
103     (hp : ∀ i, 0 ≤ p i) (_hl : ∀ i, 0 ≤ l i) (hk : ∀ i, 0 ≤ k i)
104     (hZl : 0 < evidence p l) (hZk : 0 < evidence p k) :
105     l1 (fun i => update p l i-update p k i) ≤
106       2*(∑ i, |l i-k i| *p i)/min (evidence p l) (evidence p k) := by
107   have he : l1 (fun i => l i*p i-k i*p i) = ∑ i, |l i-k i| *p i := by
108     simp only [l1, ← sub_mul, abs_mul, abs_of_nonneg (hp _)]
109   have h := normalized_l1_bound_left (fun i => l i*p i) (fun i => k i*p i)
110     (fun i => mul_nonneg (hk i) (hp i)) hZl hZk
111   change l1 (fun i => update p l i-update p k i) ≤
112     2*l1 (fun i => l i*p i-k i*p i)/evidence p l at h
113   rw [he] at h
114   exact h.trans (div_le_div_of_nonneg_left
115     (mul_nonneg (by norm_num) (Finset.sum_nonneg (fun i _ => mul_nonneg (abs_nonneg _) (hp i))))
116     (lt_min hZl hZk) (min_le_left _ _))
117 
118 def IsProbability (p : I → ℝ) : Prop := (∀ i, 0 ≤ p i) ∧ mass p = 1
119 
120 theorem posterior_probability (p l : I → ℝ) (hp : IsProbability p)
121     (hl : ∀ i, 0 ≤ l i) (hz : 0 < evidence p l) : IsProbability (update p l) :=
122   ⟨posterior_nonnegative p l hp.1 hl hz, posterior_mass p l hz.ne'⟩
123 
124 theorem prediction_probability (K : Matrix I I ℝ) (hK : ∀ i j, 0 ≤ K i j)
125     (hs : ∀ j, ∑ i, K i j=1) (p : I → ℝ) (hp : IsProbability p) :
126     IsProbability (K.mulVec p) := by
127   constructor
128   · intro i
129     exact Finset.sum_nonneg (fun j _ => mul_nonneg (hK i j) (hp.1 j))
130   · dsimp [mass, Matrix.mulVec, dotProduct]
131     rw [Finset.sum_comm]
132     simp only [← Finset.sum_mul, hs, one_mul]
133     exact hp.2
134 
135 theorem prediction_update_probability (K : Matrix I I ℝ) (hK : ∀ i j, 0 ≤ K i j)
136     (hs : ∀ j, ∑ i, K i j=1) (p l : I → ℝ) (hp : IsProbability p)
137     (hl : ∀ i, 0 ≤ l i) (hz : 0 < evidence (K.mulVec p) l) :
138     IsProbability (update (K.mulVec p) l) :=
139   posterior_probability _ _ (prediction_probability K hK hs p hp) hl hz
140 
141 end KomorebiPaperVI.FiniteBayes

Back to source controls