BayesianTowers.lean

1 import KomorebiPaperVI.BayesianNecessity
2 
3 /-! Author: Komorebi P. Variable-state finite towers with explicit singleton boundaries. -/
4 namespace KomorebiPaperVI.BayesianTowers
5 open KomorebiPaperVI.FiniteBayes KomorebiPaperVI.Coarsening
6 open KomorebiPaperVI.BayesianNecessity
7 open scoped BigOperators
8 variable {I A B : Type*} [Fintype I] [Fintype A] [Fintype B]
9     [DecidableEq I] [DecidableEq A] [DecidableEq B]
10 
11 omit [DecidableEq I] [Fintype B] in
12 theorem coarsen_comp (f : I → A) (g : A → B) (p : I → ℝ) :
13     coarsen g (coarsen f p)=coarsen (g ∘ f) p := by
14   funext b
15   dsimp [coarsen]
16   have hi (q : Prop) [Decidable q] (v : I → ℝ) :
17       (if q then ∑ i, v i else 0)=∑ i, if q then v i else 0 := by
18     split_ifs <;> simp
19   simp_rw [hi]
20   rw [Finset.sum_comm]
21   apply Finset.sum_congr rfl
22   intro i _
23   have he : (fun a => if g a=b then (if f i=a then p i else 0) else 0)=
24       (fun a => if f i=a then (if g a=b then p i else 0) else 0) := by
25     funext a; split_ifs <;> rfl
26   rw [he]
27   simp
28 
29 omit [DecidableEq I] in
30 theorem singleton_commutes (f : I → A) (l : I → ℝ) (k : A → ℝ)
31     (hl : ∀ i, 0 < l i) (hk : ∀ a, 0 < k a) [Subsingleton A] :
32     AllPriorCommutes f l k := by
33   intro p hp
34   funext a
35   have hs (v : A → ℝ) : mass v=v a :=
36     Finset.sum_eq_single a (fun b _ hb => False.elim (hb (Subsingleton.elim b a))) (by simp)
37   have h1 : mass (coarsen f (update p l))=1 :=
38     (coarsen_mass f _).trans (posterior_mass p l (positive_evidence p l hp hl).ne')
39   have h2 := posterior_mass (coarsen f p) k
40     (positive_evidence _ k (coarsen_probability f p hp) hk).ne'
41   exact (hs _).symm.trans (h1.trans (h2.symm.trans (hs _)))
42 
43 theorem adjacent_criterion (f : I → A) (hf : Function.Surjective f)
44     (l : I → ℝ) (k : A → ℝ) (hl : ∀ i, 0 < l i) (hk : ∀ a, 0 < k a) :
45     AllPriorCommutes f l k ↔
46       Subsingleton A ∨ ∃ c : ℝ, 0 < c ∧ ∀ i, l i=c*k (f i) := by
47   cases subsingleton_or_nontrivial A with
48   | inl h =>
49     let := h
50     exact ⟨fun _ => Or.inl h,fun _ => singleton_commutes f l k hl hk⟩
51   | inr h =>
52     let := h
53     rw [refinement_iff f hf l k hl hk]
54     simp only [not_subsingleton, false_or]
55 
56 omit [DecidableEq I] in
57 theorem compose_commutes (f : I → A) (g : A → B) (l : I → ℝ) (k : A → ℝ) (m : B → ℝ)
58     (hf : AllPriorCommutes f l k) (hg : AllPriorCommutes g k m) :
59     AllPriorCommutes (g ∘ f) l m := by
60   intro p hp
61   rw [← coarsen_comp f g, hf p hp, hg (coarsen f p) (coarsen_probability f p hp),coarsen_comp]
62 
63 section Tower
64 variable {X : ℕ → Type*} [∀ n, Fintype (X n)] [∀ n, DecidableEq (X n)]
65 
66 def towerMap (f : ∀ n, X n → X (n+1)) (s : ℕ) : (n : ℕ) → X s → X (s+n)
67   | 0 => id
68   | n+1 => f (s+n) ∘ towerMap f s n
69 
70 theorem coarsen_id (p : I → ℝ) : coarsen id p=p := by
71   funext i; simp [coarsen]
72 
73 theorem tower_commutes (f : ∀ n, X n → X (n+1)) (l : ∀ n, X n → ℝ)
74     (h : ∀ n, AllPriorCommutes (f n) (l n) (l (n+1))) (s n : ℕ) :
75     AllPriorCommutes (towerMap f s n) (l s) (l (s+n)) := by
76   induction n with
77   | zero => intro p _; simp [towerMap,coarsen_id]
78   | succ n ih => exact compose_commutes (towerMap f s n) (f (s+n)) _ _ _ ih (h (s+n))
79 
80 theorem tower_criterion (f : ∀ n, X n → X (n+1)) (hf : ∀ n, Function.Surjective (f n))
81     (l : ∀ n, X n → ℝ) (hl : ∀ n i, 0 < l n i) :
82     (∀ n, AllPriorCommutes (f n) (l n) (l (n+1))) ↔
83       ∀ n, Subsingleton (X (n+1)) ∨ ∃ c : ℝ, 0 < c ∧ ∀ i, l n i=c*l (n+1) (f n i) := by
84   exact forall_congr' (fun n => adjacent_criterion (f n) (hf n) _ _ (hl n) (hl (n+1)))
85 
86 end Tower
87 end KomorebiPaperVI.BayesianTowers

Back to source controls