Coarsening.lean

1 import KomorebiPaperVI.FiniteBayes
2 
3 /-! Author: Komorebi P. Literal finite fibers, zero-mass packets, and profile partitions. -/
4 namespace KomorebiPaperVI.Coarsening
5 open KomorebiPaperVI.FiniteBayes
6 open scoped BigOperators
7 variable {I A : Type*} [Fintype I] [Fintype A] [DecidableEq A]
8 
9 def coarsen (f : I → A) (p : I → ℝ) (a : A) : ℝ :=
10   ∑ i, if f i = a then p i else 0
11 
12 noncomputable def effective (f : I → A) (p l : I → ℝ) (a : A) : ℝ :=
13   coarsen f (fun i => l i*p i) a / coarsen f p a
14 
15 theorem coarsen_mass (f : I → A) (p : I → ℝ) : mass (coarsen f p) = mass p := by
16   simp only [mass, coarsen]
17   rw [Finset.sum_comm]
18   simp
19 
20 omit [Fintype A] in
21 theorem coarsen_nonnegative (f : I → A) (p : I → ℝ) (hp : ∀ i, 0 ≤ p i) (a : A) :
22     0 ≤ coarsen f p a := by
23   apply Finset.sum_nonneg
24   intro i _
25   split_ifs
26   · exact hp i
27   · exact le_rfl
28 
29 theorem coarsen_probability (f : I → A) (p : I → ℝ) (hp : IsProbability p) :
30     IsProbability (coarsen f p) :=
31   ⟨coarsen_nonnegative f p hp.1, (coarsen_mass f p).trans hp.2⟩
32 
33 omit [Fintype A] in
34 theorem coarsen_div (f : I → A) (p : I → ℝ) (z : ℝ) :
35     coarsen f (fun i => p i/z) = fun a => coarsen f p a/z := by
36   funext a
37   simp only [coarsen, Finset.sum_div]
38   apply Finset.sum_congr rfl
39   intro i _
40   split_ifs <;> simp
41 
42 omit [Fintype A] in
43 theorem coarsen_posterior (f : I → A) (p l : I → ℝ) :
44     coarsen f (update p l) = fun a => coarsen f (fun i => l i*p i) a/evidence p l :=
45   coarsen_div f _ _
46 
47 omit [Fintype A] in
48 theorem zero_packet_component (f : I → A) (p : I → ℝ) (hp : ∀ i, 0 ≤ p i)
49     (a : A) (ha : coarsen f p a = 0) (i : I) (hi : f i=a) : p i=0 := by
50   have he : (if f i=a then p i else 0) ≤ coarsen f p a :=
51     Finset.single_le_sum (f := fun j => if f j=a then p j else 0)
52       (fun j _ => by split_ifs; exact hp j; exact le_rfl) (Finset.mem_univ i)
53   rw [ite_eq_left hi, ha] at he
54   exact le_antisymm he (hp i)
55 
56 omit [Fintype A] in
57 theorem zero_packet_weighted (f : I → A) (p l : I → ℝ) (hp : ∀ i, 0 ≤ p i)
58     (a : A) (ha : coarsen f p a=0) : coarsen f (fun i => l i*p i) a=0 := by
59   apply Finset.sum_eq_zero
60   intro i _
61   by_cases hi : f i=a
62   · simp [hi, zero_packet_component f p hp a ha i hi]
63   · simp [hi]
64 
65 omit [Fintype A] in
66 theorem effective_weight (f : I → A) (p l : I → ℝ) (hp : ∀ i, 0 ≤ p i) (a : A) :
67     effective f p l a*coarsen f p a = coarsen f (fun i => l i*p i) a := by
68   by_cases ha : coarsen f p a=0
69   · simp [effective, ha, zero_packet_weighted f p l hp a ha]
70   · exact div_mul_cancel₀ _ ha
71 
72 omit [Fintype A] in
73 theorem effective_nonnegative (f : I → A) (p l : I → ℝ) (hp : ∀ i, 0 ≤ p i)
74     (hl : ∀ i, 0 ≤ l i) (a : A) : 0 ≤ effective f p l a :=
75   div_nonneg (coarsen_nonnegative f _ (fun i => mul_nonneg (hl i) (hp i)) a)
76     (coarsen_nonnegative f p hp a)
77 
78 theorem effective_evidence (f : I → A) (p l : I → ℝ) (hp : ∀ i, 0 ≤ p i) :
79     evidence (coarsen f p) (effective f p l) = evidence p l := by
80   simp only [evidence, effective_weight f p l hp]
81   exact coarsen_mass f _
82 
83 theorem effective_factorization (f : I → A) (p l : I → ℝ) (hp : ∀ i, 0 ≤ p i) :
84     coarsen f (update p l) = update (coarsen f p) (effective f p l) := by
85   rw [coarsen_posterior]
86   funext a
87   simp only [update, effective_weight f p l hp, effective_evidence f p l hp]
88 
89 omit [Fintype A] in
90 theorem packet_reconstruction_point (f : I → A) (w : I → ℝ) (hw : ∀ i, 0 ≤ w i)
91     (i : I) :
92     (coarsen f w (f i)/mass w)*(w i/coarsen f w (f i)) = normalize w i := by
93   by_cases ha : coarsen f w (f i)=0
94   · have hi := zero_packet_component f w hw (f i) ha i rfl
95     simp [ha, hi, FiniteBayes.normalize]
96   · dsimp [FiniteBayes.normalize]
97     field_simp
98 
99 theorem packet_reconstruction (f : I → A) (w : I → ℝ) (hw : ∀ i, 0 ≤ w i) (i : I) :
100     (∑ a, (coarsen f w a/mass w)*(if f i=a then w i/coarsen f w a else 0)) =
101       normalize w i := by
102   simpa [mul_ite] using
103     packet_reconstruction_point f w hw i
104 
105 omit [Fintype A] in
106 theorem blockwise_weight (f : I → A) (p : I → ℝ) (k : A → ℝ) (a : A) :
107     coarsen f (fun i => k (f i)*p i) a = k a*coarsen f p a := by
108   simp only [coarsen, Finset.mul_sum]
109   apply Finset.sum_congr rfl
110   intro i _
111   split_ifs with hi
112   · rw [hi]
113   · simp
114 
115 theorem blockwise_evidence (f : I → A) (p : I → ℝ) (k : A → ℝ) :
116     evidence p (k ∘ f) = evidence (coarsen f p) k := by
117   have h := coarsen_mass f (fun i => k (f i)*p i)
118   simpa only [mass, blockwise_weight, evidence, Function.comp_apply] using h.symm
119 
120 theorem blockwise_sufficiency (f : I → A) (p : I → ℝ) (k : A → ℝ) :
121     coarsen f (update p (k ∘ f)) = update (coarsen f p) k := by
122   rw [coarsen_posterior]
123   funext a
124   simp only [Function.comp_apply, blockwise_weight, blockwise_evidence, update]
125 
126 theorem scaled_blockwise_sufficiency (f : I → A) (p : I → ℝ) (k : A → ℝ)
127     (c : ℝ) (hc : c ≠ 0) (hz : evidence p (k ∘ f) ≠ 0) :
128     coarsen f (update p (fun i => c*k (f i))) = update (coarsen f p) k := by
129   have he := posterior_scale p (k ∘ f) c hc hz
130   simp only [Function.comp_apply] at he
131   rw [he]
132   exact blockwise_sufficiency f p k
133 
134 omit [DecidableEq A] in
135 theorem one_packet_posterior (p k : A → ℝ) [Unique A] (hz : evidence p k ≠ 0) (a : A) :
136     update p k a=1 := by
137   have ha : a = default := Subsingleton.elim a default
138   simpa [mass, ha] using posterior_mass p k hz
139 
140 end KomorebiPaperVI.Coarsening
141 
142 namespace KomorebiPaperVI.Profiles
143 variable {I Y A : Type*}
144 
145 def sameProfile (l : Y → I → ℝ) (i j : I) : Prop := ∀ y, l y i=l y j
146 
147 theorem profile_equivalence (l : Y → I → ℝ) : Equivalence (sameProfile l) := by
148   refine ⟨?_, ?_, ?_⟩
149   · intro i y; rfl
150   · intro i j h y; exact (h y).symm
151   · intro i j k h h' y; exact (h y).trans (h' y)
152 
153 theorem likelihood_resolving_iff_refines (l : Y → I → ℝ) (f : I → A) :
154     (∀ y i j, f i=f j → l y i=l y j) ↔ (∀ i j, f i=f j → sameProfile l i j) := by
155   constructor
156   · intro h i j hij y; exact h y i j hij
157   · intro h y i j hij; exact h i j hij y
158 
159 theorem exact_profile_factorization (l : Y → I → ℝ) (y : Y) (i : I) :
160     (fun profile : Y → ℝ => profile y) (fun z => l z i) = l y i := rfl
161 
162 end KomorebiPaperVI.Profiles

Back to source controls