InformationLoss.lean

1 import KomorebiPaperVI.Coarsening
2 
3 /-! Author: Komorebi P. Literal information-loss matrix and the fine-to-coarse loss estimate. -/
4 namespace KomorebiPaperVI.InformationLoss
5 open KomorebiPaperVI.FiniteBayes KomorebiPaperVI.Coarsening
6 open scoped BigOperators
7 variable {I A : Type*} [Fintype I] [Fintype A] [DecidableEq A]
8 
9 def lossMatrix (P b : A → ℝ) : Matrix A A ℝ :=
10   fun a j => (if a=j then P a else 0)-b a*P j
11 
12 theorem lossMatrix_apply (P b d : A → ℝ) (a : A) :
13     (lossMatrix P b).mulVec d a=P a*d a-b a*(∑ j, P j*d j) := by
14   simp [lossMatrix, Matrix.mulVec, dotProduct, sub_mul, Finset.sum_sub_distrib,
15     ite_mul, mul_assoc, ← Finset.mul_sum]
16 
17 theorem information_loss_matrix (f : I → A) (p l : I → ℝ) (k : A → ℝ)
18     (hp : ∀ i, 0 ≤ p i) (hz : evidence p l ≠ 0)
19     (hk : evidence (coarsen f p) k ≠ 0) (a : A) :
20     coarsen f (update p l) a-update (coarsen f p) k a =
21       (lossMatrix (coarsen f p) (update (coarsen f p) k)).mulVec
22         (fun j => effective f p l j-k j) a/evidence p l := by
23   rw [effective_factorization f p l hp, lossMatrix_apply]
24   have he := posterior_difference (coarsen f p) (effective f p l) k
25     (by rwa [effective_evidence f p l hp]) hk a
26   simpa only [effective_evidence f p l hp] using he
27 
28 theorem information_loss_null (P k : A → ℝ) (hk : evidence P k ≠ 0) :
29     (lossMatrix P (update P k)).mulVec k=0 := by
30   funext a
31   rw [lossMatrix_apply]
32   exact scale_null_direction P k hk a
33 
34 omit [Fintype A] in
35 theorem fiber_loss_bound (f : I → A) (p l : I → ℝ) (k : A → ℝ)
36     (hp : ∀ i, 0 ≤ p i) (a : A) :
37     coarsen f p a*|effective f p l a-k a| ≤
38       coarsen f (fun i => p i*|l i-k (f i)|) a := by
39   have he : (effective f p l a-k a)*coarsen f p a =
40       ∑ i, if f i=a then p i*(l i-k (f i)) else 0 := by
41     rw [sub_mul,effective_weight f p l hp]
42     simp only [coarsen, Finset.mul_sum, ← Finset.sum_sub_distrib]
43     apply Finset.sum_congr rfl
44     intro i _
45     by_cases hi : f i=a
46     · simp only [hi,ite_true]; ring
47     · simp [hi]
48   calc
49     _ = |(effective f p l a-k a)*coarsen f p a| := by
50       rw [abs_mul, abs_of_nonneg (coarsen_nonnegative f p hp a), mul_comm]
51     _ ≤ ∑ i, |if f i=a then p i*(l i-k (f i)) else 0| := by
52       rw [he]; exact Finset.abs_sum_le_sum_abs _ _
53     _ = _ := by
54       apply Finset.sum_congr rfl
55       intro i _
56       by_cases hi : f i=a
57       · simp [hi, abs_mul, abs_of_nonneg (hp i)]
58       · simp [hi]
59 
60 theorem total_loss_bound (f : I → A) (p l : I → ℝ) (k : A → ℝ)
61     (hp : ∀ i, 0 ≤ p i) :
62     (∑ a, coarsen f p a*|effective f p l a-k a|) ≤ ∑ i, p i*|l i-k (f i)| := by
63   calc
64     _ ≤ ∑ a, coarsen f (fun i => p i*|l i-k (f i)|) a :=
65       Finset.sum_le_sum (fun a _ => fiber_loss_bound f p l k hp a)
66     _ = _ := coarsen_mass f _
67 
68 theorem information_loss_norm (f : I → A) (p l : I → ℝ) (k : A → ℝ)
69     (hp : ∀ i, 0 ≤ p i) (hl : ∀ i, 0 ≤ l i) (hk : ∀ a, 0 ≤ k a)
70     (hz : 0 < evidence p l) (hzk : 0 < evidence (coarsen f p) k) :
71     l1 (fun a => coarsen f (update p l) a-update (coarsen f p) k a) ≤
72       2*(∑ a, coarsen f p a*|effective f p l a-k a|)/
73         min (evidence p l) (evidence (coarsen f p) k) := by
74   rw [effective_factorization f p l hp]
75   have he := likelihood_perturbation_bound (coarsen f p) (effective f p l) k
76     (coarsen_nonnegative f p hp) (effective_nonnegative f p l hp hl) hk
77     (by rwa [effective_evidence f p l hp]) hzk
78   simpa only [effective_evidence f p l hp, mul_comm] using he
79 
80 end KomorebiPaperVI.InformationLoss

Back to source controls