BayesianNecessity.lean

1 import KomorebiPaperVI.Coarsening
2 
3 /-! Author: Komorebi P. All-prior necessity is derived from actual two-state priors. -/
4 namespace KomorebiPaperVI.BayesianNecessity
5 open KomorebiPaperVI.FiniteBayes KomorebiPaperVI.Coarsening
6 open scoped BigOperators
7 variable {I A : Type*} [Fintype I] [Fintype A] [DecidableEq I] [DecidableEq A]
8 
9 noncomputable def pairPrior (i j : I) (x : I) : ℝ :=
10   (if x=i then 1/2 else 0)+(if x=j then 1/2 else 0)
11 
12 omit [Fintype A] [DecidableEq A] in
13 theorem pair_weighted_sum (i j : I) (w : I → ℝ) :
14     (∑ x, w x*pairPrior i j x)=(w i+w j)/2 := by
15   simp [pairPrior, mul_add, Finset.sum_add_distrib]
16   ring
17 
18 omit [Fintype A] [DecidableEq A] in
19 theorem pair_probability (i j : I) : IsProbability (pairPrior i j) := by
20   constructor
21   · intro x; unfold pairPrior; split_ifs <;> norm_num
22   · simpa [IsProbability, mass] using pair_weighted_sum i j (fun _ => 1)
23 
24 omit [Fintype A] in
25 theorem pair_fiber_weight (f : I → A) (i j : I) (w : I → ℝ) (a : A) :
26     coarsen f (fun x => w x*pairPrior i j x) a =
27       ((if f i=a then w i else 0)+(if f j=a then w j else 0))/2 := by
28   have he : coarsen f (fun x => w x*pairPrior i j x) a =
29       ∑ x, (if f x=a then w x else 0)*pairPrior i j x := by
30     apply Finset.sum_congr rfl
31     intro x _; split_ifs <;> simp
32   rw [he, pair_weighted_sum]
33 
34 omit [Fintype A] in
35 theorem pair_coarsen (f : I → A) (i j : I) :
36     coarsen f (pairPrior i j)=pairPrior (f i) (f j) := by
37   funext a
38   have he := pair_fiber_weight f i j (fun _ => 1) a
39   simp only [one_mul] at he
40   rw [he]
41   rw [add_div]
42   have h1 : (if f i=a then (1:ℝ) else 0)/2=(if a=f i then 1/2 else 0) := by
43     by_cases hi : f i=a
44     · simp [hi]
45     · simp [hi, Ne.symm hi]
46   have h2 : (if f j=a then (1:ℝ) else 0)/2=(if a=f j then 1/2 else 0) := by
47     by_cases hj : f j=a
48     · simp [hj]
49     · simp [hj, Ne.symm hj]
50   rw [h1,h2]
51   rfl
52 
53 omit [Fintype A] in
54 theorem pair_coarse_posterior (f : I → A) (l : I → ℝ) (i j : I) (hij : f i≠f j) :
55     coarsen f (update (pairPrior i j) l) (f i)=l i/(l i+l j) := by
56   simp only [coarsen_posterior]
57   rw [pair_fiber_weight]
58   have he : evidence (pairPrior i j) l=(l i+l j)/2 := pair_weighted_sum i j l
59   rw [he]
60   simp only [ite_true, ite_eq_right hij.symm, add_zero]
61   rw [div_div_div_comm]
62   norm_num
63 
64 def AllPriorCommutes (f : I → A) (l : I → ℝ) (k : A → ℝ) : Prop :=
65   ∀ p, IsProbability p → coarsen f (update p l)=update (coarsen f p) k
66 
67 theorem cross_packet_ratio (f : I → A) (l : I → ℝ) (k : A → ℝ)
68     (hl : ∀ i, 0 < l i) (hk : ∀ a, 0 < k a)
69     (h : AllPriorCommutes f l k) (i j : I) (hij : f i≠f j) :
70     l i*k (f j)=l j*k (f i) := by
71   have he := congrFun (h (pairPrior i j) (pair_probability i j)) (f i)
72   rw [pair_coarse_posterior f l i j hij, pair_coarsen] at he
73   have hco : update (pairPrior (f i) (f j)) k (f i)=k (f i)/(k (f i)+k (f j)) := by
74     dsimp [update]
75     rw [show evidence (pairPrior (f i) (f j)) k=(k (f i)+k (f j))/2 from
76       pair_weighted_sum _ _ _]
77     simp only [pairPrior, ite_true, ite_eq_right hij, add_zero]
78     rw [mul_div_assoc, div_div_div_comm]
79     norm_num [div_eq_mul_inv]
80   rw [hco] at he
81   have hc := (div_eq_div_iff (ne_of_gt (add_pos (hl i) (hl j)))
82     (ne_of_gt (add_pos (hk (f i)) (hk (f j))))).mp he
83   nlinarith
84 
85 theorem all_packet_ratio (f : I → A) (hf : Function.Surjective f) [Nontrivial A]
86     (l : I → ℝ) (k : A → ℝ) (hl : ∀ i, 0 < l i) (hk : ∀ a, 0 < k a)
87     (h : AllPriorCommutes f l k) (i j : I) : l i*k (f j)=l j*k (f i) := by
88   by_cases hij : f i=f j
89   · obtain ⟨b,hb⟩ := exists_ne (f i)
90     obtain ⟨u,hu⟩ := hf b
91     have hiu : f i≠f u := by rw [hu]; exact hb.symm
92     have hju : f j≠f u := by rw [← hij]; exact hiu
93     have h1 := cross_packet_ratio f l k hl hk h i u hiu
94     have h2 := cross_packet_ratio f l k hl hk h j u hju
95     rw [← hij] at h2
96     have heq : l i=l j := by nlinarith [hk (f u)]
97     rw [hij, heq]
98   · exact cross_packet_ratio f l k hl hk h i j hij
99 
100 omit [DecidableEq I] in
101 theorem positive_evidence (p l : I → ℝ) (hp : IsProbability p) (hl : ∀ i, 0 < l i) :
102     0 < evidence p l := by
103   have hex : ∃ i, 0 < p i := by
104     by_contra h
105     push Not at h
106     have hz : mass p=0 := Finset.sum_eq_zero (fun i _ => le_antisymm (h i) (hp.1 i))
107     linarith [hp.2]
108   obtain ⟨i,hi⟩ := hex
109   exact Finset.sum_pos' (fun j _ => mul_nonneg (hl j).le (hp.1 j))
110     ⟨i,Finset.mem_univ i,mul_pos (hl i) hi⟩
111 
112 theorem refinement_iff (f : I → A) (hf : Function.Surjective f) [Nontrivial A]
113     (l : I → ℝ) (k : A → ℝ) (hl : ∀ i, 0 < l i) (hk : ∀ a, 0 < k a) :
114     AllPriorCommutes f l k ↔ ∃ c : ℝ, 0 < c ∧ ∀ i, l i=c*k (f i) := by
115   constructor
116   · intro h
117     obtain ⟨a⟩ := (inferInstance : Nonempty A)
118     obtain ⟨i,hi⟩ := hf a
119     refine ⟨l i/k (f i), div_pos (hl i) (hk (f i)), ?_⟩
120     intro j
121     have he := all_packet_ratio f hf l k hl hk h j i
122     apply (eq_div_iff (ne_of_gt (hk (f i)))).mpr at he
123     calc
124       l j = (l i*k (f j))/k (f i) := he
125       _ = _ := by ring
126   · rintro ⟨c,hc,he⟩ p hp
127     have heq : l=fun i => c*k (f i) := funext he
128     rw [heq]
129     exact scaled_blockwise_sufficiency f p k c hc.ne'
130       (positive_evidence p (k ∘ f) hp (fun i => hk (f i))).ne'
131 
132 end KomorebiPaperVI.BayesianNecessity

Back to source controls