ProgramRefinement.lean

1 import Mathlib.Topology.Algebra.InfiniteSum.Real
2 import Mathlib.Tactic.NormNum
3 
4 
5 set_option autoImplicit false
6 
7 /-!
8 # Prior-preserving program refinement
9 
10 A child is selected once for the whole record. The likelihood mixture assumed
11 below is the whole-record likelihood, and for prediction the joint likelihood
12 of that record and the predicted event. No product-of-one-step-mixtures identity
13 is assumed. The index sets may be infinite.
14 -/
15 
16 namespace Komorebi.LSM.ProgramRefinement
17 
18 noncomputable section
19 
20 variable {J G : Type*}
21 
22 /-- The prior of a child after splitting the parent's prior mass. -/
23 def childPrior (parentPrior : ℝ) (weight : J → ℝ) (j : J) : ℝ :=
24   parentPrior * weight j
25 
26 /-- The unnormalized evidence contributed by all children. -/
27 def childEvidence (parentPrior : ℝ) (weight likelihood : J → ℝ) : ℝ :=
28   ∑' j, childPrior parentPrior weight j * likelihood j
29 
30 /-- The original normalizer, with the parent distinguished from other programs. -/
31 def originalEvidence (otherPrior otherLikelihood : G → ℝ)
32     (parentPrior parentLikelihood : ℝ) : ℝ :=
33   (∑' g, otherPrior g * otherLikelihood g) + parentPrior * parentLikelihood
34 
35 /-- The refined normalizer, leaving every other program unchanged. -/
36 def refinedEvidence (otherPrior otherLikelihood : G → ℝ)
37     (parentPrior : ℝ) (weight likelihood : J → ℝ) : ℝ :=
38   (∑' g, otherPrior g * otherLikelihood g) + childEvidence parentPrior weight likelihood
39 
40 /-- Child prior masses remain nonnegative. -/
41 theorem childPrior_nonneg (parentPrior : ℝ) (weight : J → ℝ)
42     (hparent : 0 ≤ parentPrior) (hweight : ∀ j, 0 ≤ weight j) (j : J) :
43     0 ≤ childPrior parentPrior weight j :=
44   mul_nonneg hparent (hweight j)
45 
46 /-- The sum of all child prior masses is exactly the former parent mass. -/
47 theorem childPrior_sum (parentPrior : ℝ) (weight : J → ℝ)
48     (hweight : ∑' j, weight j = 1) :
49     (∑' j, childPrior parentPrior weight j) = parentPrior := by
50   simp only [childPrior, tsum_mul_left, hweight, mul_one]
51 
52 /-- Factoring out the original prior is legitimate for the entire infinite sum. -/
53 theorem childEvidence_factor (parentPrior : ℝ) (weight likelihood : J → ℝ) :
54     childEvidence parentPrior weight likelihood =
55       parentPrior * ∑' j, weight j * likelihood j := by
56   simp only [childEvidence, childPrior, mul_assoc, tsum_mul_left]
57 
58 /-- The whole-record mixture identity preserves the parent's evidence exactly. -/
59 theorem childEvidence_eq (parentPrior parentLikelihood : ℝ)
60     (weight likelihood : J → ℝ)
61     (hmixture : parentLikelihood = ∑' j, weight j * likelihood j) :
62     childEvidence parentPrior weight likelihood = parentPrior * parentLikelihood := by
63   rw [childEvidence_factor, ← hmixture]
64 
65 /-- Splitting a parent into mixture children leaves the total evidence unchanged. -/
66 theorem total_evidence_unchanged (otherPrior otherLikelihood : G → ℝ)
67     (parentPrior parentLikelihood : ℝ) (weight likelihood : J → ℝ)
68     (hmixture : parentLikelihood = ∑' j, weight j * likelihood j) :
69     refinedEvidence otherPrior otherLikelihood parentPrior weight likelihood =
70       originalEvidence otherPrior otherLikelihood parentPrior parentLikelihood := by
71   rw [refinedEvidence, originalEvidence, childEvidence_eq _ _ _ _ hmixture]
72 
73 /-- The child posterior masses sum to the former parent's posterior mass. -/
74 theorem child_posterior_sum (otherPrior otherLikelihood : G → ℝ)
75     (parentPrior parentLikelihood : ℝ) (weight likelihood : J → ℝ)
76     (hmixture : parentLikelihood = ∑' j, weight j * likelihood j) :
77     (∑' j, (childPrior parentPrior weight j * likelihood j) /
78       refinedEvidence otherPrior otherLikelihood parentPrior weight likelihood) =
79     (parentPrior * parentLikelihood) /
80       originalEvidence otherPrior otherLikelihood parentPrior parentLikelihood := by
81   rw [tsum_div_const]
82   change childEvidence parentPrior weight likelihood / _ = _
83   rw [childEvidence_eq _ _ _ _ hmixture,
84     total_evidence_unchanged _ _ _ _ _ _ hmixture]
85 
86 /-- Every other program has the same posterior mass after the split. -/
87 theorem other_posterior_unchanged (otherPrior otherLikelihood : G → ℝ)
88     (parentPrior parentLikelihood : ℝ) (weight likelihood : J → ℝ)
89     (hmixture : parentLikelihood = ∑' j, weight j * likelihood j) (g : G) :
90     (otherPrior g * otherLikelihood g) /
91         refinedEvidence otherPrior otherLikelihood parentPrior weight likelihood =
92       (otherPrior g * otherLikelihood g) /
93         originalEvidence otherPrior otherLikelihood parentPrior parentLikelihood := by
94   rw [total_evidence_unchanged _ _ _ _ _ _ hmixture]
95 
96 /-- Joint-likelihood mixture consistency also preserves every predictive event. -/
97 theorem predictive_event_unchanged (otherPrior otherLikelihood otherJoint : G → ℝ)
98     (parentPrior parentLikelihood parentJoint : ℝ)
99     (weight likelihood jointLikelihood : J → ℝ)
100     (hmixture : parentLikelihood = ∑' j, weight j * likelihood j)
101     (hjoint : parentJoint = ∑' j, weight j * jointLikelihood j) :
102     refinedEvidence otherPrior otherJoint parentPrior weight jointLikelihood /
103         refinedEvidence otherPrior otherLikelihood parentPrior weight likelihood =
104       originalEvidence otherPrior otherJoint parentPrior parentJoint /
105         originalEvidence otherPrior otherLikelihood parentPrior parentLikelihood := by
106   rw [total_evidence_unchanged _ _ _ _ _ _ hjoint,
107     total_evidence_unchanged _ _ _ _ _ _ hmixture]
108 
109 /-- Atlas recodings with identical likelihood conserve the original evidence. -/
110 theorem identical_likelihood_evidence (parentPrior parentLikelihood : ℝ)
111     (weight : J → ℝ) (hweight : ∑' j, weight j = 1) :
112     childEvidence parentPrior weight (fun _ => parentLikelihood) =
113       parentPrior * parentLikelihood := by
114   rw [childEvidence_factor, tsum_mul_right, hweight, one_mul]
115 
116 /-- Selecting a fixed child for the whole record differs from switching at each step. -/
117 theorem fixed_child_ne_stepwise_switching :
118     (1 / 2 : ℝ) * (1 * 1) + (1 / 2 : ℝ) * (0 * 0) ≠
119       ((1 / 2 : ℝ) * 1 + (1 / 2 : ℝ) * 0) ^ 2 := by
120   norm_num
121 
122 /-- The declared hypotheses of Proposition 24, including a genuine positive normalizer. -/
123 structure RefinementContract (G J : Type*) where
124   otherPrior : G → ℝ
125   otherLikelihood : G → ℝ
126   parentPrior : ℝ
127   parentLikelihood : ℝ
128   weight : J → ℝ
129   likelihood : J → ℝ
130   otherPrior_nonneg : ∀ g, 0 ≤ otherPrior g
131   otherLikelihood_nonneg : ∀ g, 0 ≤ otherLikelihood g
132   parentPrior_nonneg : 0 ≤ parentPrior
133   weight_nonneg : ∀ j, 0 ≤ weight j
134   likelihood_nonneg : ∀ j, 0 ≤ likelihood j
135   weight_summable : Summable weight
136   weight_sum : ∑' j, weight j = 1
137   otherEvidence_summable : Summable (fun g => otherPrior g * otherLikelihood g)
138   weightedLikelihood_summable : Summable (fun j => weight j * likelihood j)
139   whole_record_mixture : parentLikelihood = ∑' j, weight j * likelihood j
140   otherPrior_summable : Summable otherPrior
141   prior_normalized : (∑' g, otherPrior g) + parentPrior = 1
142   normalizer_pos : 0 < originalEvidence otherPrior otherLikelihood parentPrior parentLikelihood
143 
144 /-- Refined priors conserve total probability mass. -/
145 theorem refined_prior_normalized (c : RefinementContract G J) :
146     (∑' g, c.otherPrior g) + (∑' j, childPrior c.parentPrior c.weight j) = 1 := by
147   rw [childPrior_sum _ _ c.weight_sum]
148   exact c.prior_normalized
149 
150 /-- The refined normalizer remains strictly positive. -/
151 theorem refined_normalizer_pos (c : RefinementContract G J) :
152     0 < refinedEvidence c.otherPrior c.otherLikelihood c.parentPrior c.weight c.likelihood := by
153   rw [total_evidence_unchanged _ _ _ _ _ _ c.whole_record_mixture]
154   exact c.normalizer_pos
155 
156 /-- The children have summable unnormalized evidence under the contract. -/
157 theorem child_evidence_summable (c : RefinementContract G J) :
158     Summable (fun j => childPrior c.parentPrior c.weight j * c.likelihood j) := by
159   simpa only [childPrior, mul_assoc] using
160     c.weightedLikelihood_summable.mul_left c.parentPrior
161 
162 /-- The child posterior is an actual summable nonnegative mass family. -/
163 theorem child_posterior_summable (c : RefinementContract G J) :
164     Summable (fun j => (childPrior c.parentPrior c.weight j * c.likelihood j) /
165       refinedEvidence c.otherPrior c.otherLikelihood c.parentPrior c.weight c.likelihood) :=
166   (child_evidence_summable c).div_const _
167 
168 /-- Child posterior masses are nonnegative. -/
169 theorem child_posterior_nonneg (c : RefinementContract G J) (j : J) :
170     0 ≤ (childPrior c.parentPrior c.weight j * c.likelihood j) /
171       refinedEvidence c.otherPrior c.otherLikelihood c.parentPrior c.weight c.likelihood := by
172   exact div_nonneg
173     (mul_nonneg (childPrior_nonneg _ _ c.parentPrior_nonneg c.weight_nonneg j)
174       (c.likelihood_nonneg j)) (le_of_lt (refined_normalizer_pos c))
175 
176 /-- Refined posterior masses, including all unchanged programs, sum to one. -/
177 theorem refined_posterior_normalized (c : RefinementContract G J) :
178     (∑' g, (c.otherPrior g * c.otherLikelihood g) /
179       refinedEvidence c.otherPrior c.otherLikelihood c.parentPrior c.weight c.likelihood) +
180     (∑' j, (childPrior c.parentPrior c.weight j * c.likelihood j) /
181       refinedEvidence c.otherPrior c.otherLikelihood c.parentPrior c.weight c.likelihood) = 1 := by
182   rw [tsum_div_const, tsum_div_const, ← add_div]
183   exact div_self (ne_of_gt (refined_normalizer_pos c))
184 
185 /-- Proposition 24: prior, evidence, child posterior and other posteriors are preserved. -/
186 theorem prior_preserving_refinement (c : RefinementContract G J) :
187     ((∑' g, c.otherPrior g) + (∑' j, childPrior c.parentPrior c.weight j) = 1) ∧
188     (refinedEvidence c.otherPrior c.otherLikelihood c.parentPrior c.weight c.likelihood =
189       originalEvidence c.otherPrior c.otherLikelihood c.parentPrior c.parentLikelihood) ∧
190     ((∑' j, (childPrior c.parentPrior c.weight j * c.likelihood j) /
191         refinedEvidence c.otherPrior c.otherLikelihood c.parentPrior c.weight c.likelihood) =
192       (c.parentPrior * c.parentLikelihood) /
193         originalEvidence c.otherPrior c.otherLikelihood c.parentPrior c.parentLikelihood) ∧
194     (∀ g, (c.otherPrior g * c.otherLikelihood g) /
195         refinedEvidence c.otherPrior c.otherLikelihood c.parentPrior c.weight c.likelihood =
196       (c.otherPrior g * c.otherLikelihood g) /
197         originalEvidence c.otherPrior c.otherLikelihood c.parentPrior c.parentLikelihood) := by
198   exact ⟨refined_prior_normalized c,
199     total_evidence_unchanged _ _ _ _ _ _ c.whole_record_mixture,
200     child_posterior_sum _ _ _ _ _ _ c.whole_record_mixture,
201     other_posterior_unchanged _ _ _ _ _ _ c.whole_record_mixture⟩
202 
203 end
204 
205 end Komorebi.LSM.ProgramRefinement

Back to source controls