BayesianPartitions.lean

1 import KomorebiPaperVI.BayesianNecessity
2 
3 /-! Author: Komorebi P. Quotient likelihood-profile partitions and their universal property. -/
4 namespace KomorebiPaperVI.BayesianPartitions
5 open KomorebiPaperVI.FiniteBayes KomorebiPaperVI.Coarsening
6 open KomorebiPaperVI.Profiles KomorebiPaperVI.BayesianNecessity
7 variable {I Y A : Type*} [Fintype I]
8 
9 def profileSetoid (l : Y → I → ℝ) : Setoid I := ⟨sameProfile l,profile_equivalence l⟩
10 abbrev Packet (l : Y → I → ℝ) := Quotient (profileSetoid l)
11 def packetMap (l : Y → I → ℝ) (i : I) : Packet l := Quotient.mk (profileSetoid l) i
12 
13 omit [Fintype I] in
14 theorem packetMap_surjective (l : Y → I → ℝ) : Function.Surjective (packetMap l) :=
15   Quotient.mk_surjective
16 
17 noncomputable instance packetFintype (l : Y → I → ℝ) : Fintype (Packet l) :=
18   by classical exact Fintype.ofSurjective (packetMap l) (packetMap_surjective l)
19 
20 def packetLikelihood (l : Y → I → ℝ) (y : Y) : Packet l → ℝ :=
21   Quotient.lift (l y) (fun _ _ h => h y)
22 
23 omit [Fintype I] in
24 theorem packetLikelihood_apply (l : Y → I → ℝ) (y : Y) (i : I) :
25     packetLikelihood l y (packetMap l i)=l y i := rfl
26 
27 omit [Fintype I] in
28 theorem packet_eq_iff (l : Y → I → ℝ) (i j : I) :
29     packetMap l i=packetMap l j ↔ ∀ y, l y i=l y j :=
30   Quotient.eq
31 
32 omit [Fintype I] in
33 theorem packetLikelihood_positive (l : Y → I → ℝ) (hl : ∀ y i, 0 < l y i)
34     (y : Y) (q : Packet l) : 0 < packetLikelihood l y q := by
35   induction q using Quotient.inductionOn with
36   | h i => exact hl y i
37 
38 theorem canonical_coarsening (l : Y → I → ℝ) [DecidableEq (Packet l)] (y : Y) (p : I → ℝ) :
39     coarsen (packetMap l) (update p (l y)) =
40       update (coarsen (packetMap l) p) (packetLikelihood l y) := by
41   have he : packetLikelihood l y ∘ packetMap l=l y := rfl
42   rw [← he]
43   exact blockwise_sufficiency (packetMap l) p (packetLikelihood l y)
44 
45 omit [Fintype I] in
46 theorem canonical_unique_factor (l : Y → I → ℝ) (f : I → A) (hf : Function.Surjective f)
47     (h : ∀ y i j, f i=f j → l y i=l y j) :
48     ∃! u : A → Packet l, ∀ i, u (f i)=packetMap l i := by
49   classical
50   let u := fun a => packetMap l (hf a).choose
51   have hu : ∀ i, u (f i)=packetMap l i := by
52     intro i
53     apply (packet_eq_iff l _ _).mpr
54     intro y
55     exact h y _ _ (hf (f i)).choose_spec
56   refine ⟨u,hu,?_⟩
57   intro v hv
58   funext a
59   obtain ⟨i,rfl⟩ := hf a
60   exact (hv i).trans (hu i).symm
61 
62 variable [Fintype A] [DecidableEq A] [DecidableEq I]
63 
64 def FamilyCloses (l : Y → I → ℝ) (f : I → A) : Prop :=
65   ∀ y, ∃ k : A → ℝ, (∀ a, 0 < k a) ∧ AllPriorCommutes f (l y) k
66 
67 theorem all_prior_family_iff_resolves (l : Y → I → ℝ) (hl : ∀ y i, 0 < l y i)
68     (f : I → A) (hf : Function.Surjective f) [Nontrivial A] :
69     FamilyCloses l f ↔ ∀ y i j, f i=f j → l y i=l y j := by
70   constructor
71   · intro h y i j hij
72     obtain ⟨k,hk,hc⟩ := h y
73     obtain ⟨c,_,he⟩ := (refinement_iff f hf (l y) k (hl y) hk).mp hc
74     rw [he i, he j,hij]
75   · intro h y
76     let k := fun a => l y (hf a).choose
77     have he : l y=k ∘ f := by
78       funext i
79       exact h y i _ (hf (f i)).choose_spec.symm
80     refine ⟨k,fun a => hl y _,?_⟩
81     intro p _
82     rw [he]
83     exact blockwise_sufficiency f p k
84 
85 theorem canonical_coarsest_nontrivial (l : Y → I → ℝ) (hl : ∀ y i, 0 < l y i)
86     (f : I → A) (hf : Function.Surjective f) [Nontrivial A] (h : FamilyCloses l f) :
87     ∃! u : A → Packet l, ∀ i, u (f i)=packetMap l i :=
88   canonical_unique_factor l f hf ((all_prior_family_iff_resolves l hl f hf).mp h)
89 
90 omit [Fintype I] [DecidableEq I] in
91 theorem canonical_nontrivial (l : Y → I → ℝ)
92     (h : ∃ i j y, l y i≠l y j) : Nontrivial (Packet l) := by
93   obtain ⟨i,j,y,hij⟩ := h
94   exact ⟨⟨packetMap l i,packetMap l j,fun he => hij ((packet_eq_iff l i j).mp he y)⟩⟩
95 
96 end KomorebiPaperVI.BayesianPartitions

Back to source controls