ContinuousBinnedRecords.lean

1 import KomorebiLSM.ContinuousBins
2 import KomorebiLSM.ContinuousRecords
3 import Mathlib.MeasureTheory.Integral.Prod
4 import KomorebiLSM.UniformIntervalMoments
5 import KomorebiLSM.BaseNormModels
6 
7 /-! Actual pushforwards of continuous record laws under a finite observation
8 bin map. Binned policies depend on the full observed action/bin history. -/
9 set_option autoImplicit false
10 open MeasureTheory
11 open scoped ENNReal BigOperators
12 
13 namespace Komorebi.LSM.ContinuousBins
14 
15 open ContinuousRecords
16 
17 noncomputable section
18 
19 universe u v
20 
21 
22 def historyMap {X : Type u} {Z : Type v} (f : X → Z) : (n : ℕ) → History X n → History Z n
23   | 0, _ => PUnit.unit
24   | n+1, h => (historyMap f n h.1, f h.2)
25 
26 def historyList {X : Type u} : (n : ℕ) → History X n → List X
27   | 0, _ => []
28   | n+1, h => historyList n h.1 ++ [h.2]
29 
30 theorem historyMap_measurable {X Z : Type*} [MeasurableSpace X] [MeasurableSpace Z]
31     (f : X → Z) (hf : Measurable f) : (n : ℕ) → Measurable (historyMap f n)
32   | 0 => measurable_const
33   | n+1 => ((historyMap_measurable f hf n).comp measurable_fst).prodMk (hf.comp measurable_snd)
34 
35 instance historyFintype {X : Type*} [Fintype X] : (n : ℕ) → Fintype (History X n)
36   | 0 => inferInstanceAs (Fintype PUnit)
37   | n+1 => by
38     let := historyFintype (X := X) n
39     exact inferInstanceAs (Fintype (History X n × X))
40 
41 instance historySingleton {X : Type*} [MeasurableSpace X] [MeasurableSingletonClass X] :
42     (n : ℕ) → MeasurableSingletonClass (History X n)
43   | 0 => inferInstanceAs (MeasurableSingletonClass PUnit)
44   | n+1 => by
45     let := historySingleton (X := X) n
46     exact inferInstanceAs (MeasurableSingletonClass (History X n × X))
47 
48 variable {E A Y I : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
49 variable [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
50 variable [MeasurableSpace Y] [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A]
51 variable [MeasurableSpace I] [Fintype I] [MeasurableSingletonClass I]
52 variable {C : BaseNorm.ProbabilityCone E} {μ : Measure Y} [IsProbabilityMeasure μ]
53 variable (D : ContinuousInstrument.DensityInstrument (A := A) C μ)
54 
55 /-- The bin map records the action without losing it. -/
56 def binStep (bin : Y → I) (r : A × Y) : A × I := (r.1, bin r.2)
57 
58 omit [Fintype A] [MeasurableSingletonClass A] [Fintype I] [MeasurableSingletonClass I] in
59 theorem binStep_measurable (bin : Y → I) (hbin : Measurable bin) :
60     Measurable (binStep (A := A) bin) := measurable_fst.prodMk (hbin.comp measurable_snd)
61 
62 omit [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] in
63 /-- Joint action/observation operators are integrable under counting actions. -/
64 theorem jointOperator_integrable :
65     Integrable (fun r : A × Y => D.op r.1 r.2) (stepReference (A := A) μ) := by
66   apply (integrable_prod_iff (ContinuousRecords.op_measurable D).aestronglyMeasurable).mpr
67   constructor
68   · exact ae_of_all _ fun a => D.integrable_op a
69   · exact Integrable.of_finite
70 
71 omit [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] in
72 /-- Literal chronological operator products have genuine Bochner integrals. -/
73 theorem run_integrable (z : E) : (n : ℕ) →
74     Integrable (ContinuousRecords.run D z n) (reference (stepReference (A := A) μ) n)
75   | 0 => by
76     change Integrable (fun _ : PUnit => z) (Measure.dirac PUnit.unit)
77     exact integrable_const _
78   | n+1 => by
79     exact (run_integrable z n).op_fst_snd (by fun_prop)
80       ⟨‖ContinuousLinearMap.apply ℝ E‖, (ContinuousLinearMap.apply ℝ E).le_opNorm₂⟩
81       (jointOperator_integrable D)
82 
83 /-- The complete fine-record fiber of one action/bin record. -/
84 def binFiber (bin : Y → I) (n : ℕ) (b : History (A × I) n) : Set (History (A × Y) n) :=
85   historyMap (binStep bin) n ⁻¹' {b}
86 
87 omit [Fintype A] [Fintype I] in
88 theorem binFiber_measurable (bin : Y → I) (hbin : Measurable bin)
89     (n : ℕ) (b : History (A × I) n) : MeasurableSet (binFiber bin n b) :=
90   (historyMap_measurable _ (binStep_measurable bin hbin) n) (measurableSet_singleton b)
91 
92 omit [MeasurableSpace Y] [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A]
93   [MeasurableSpace I] [Fintype I] [MeasurableSingletonClass I] in
94 theorem binFiber_succ (bin : Y → I) (n : ℕ) (b : History (A × I) (n+1)) :
95     binFiber bin (n+1) b = binFiber bin n b.1 ×ˢ ({b.2.1} ×ˢ (bin ⁻¹' {b.2.2})) := by
96   rcases b with ⟨b, a, i⟩
97   ext h
98   simp only [binFiber, historyMap, binStep, Set.mem_preimage, Set.mem_singleton_iff,
99     Set.mem_prod, Prod.mk.injEq]
100 
101 /-- Unweighted cell operators follow the same chronological product. -/
102 def binnedRun (bin : Y → I) (z : E) : (n : ℕ) → History (A × I) n → E
103   | 0, _ => z
104   | n+1, b => cellOperator μ (D.op b.2.1) (bin ⁻¹' {b.2.2}) (binnedRun bin z n b.1)
105 
106 omit [MeasurableSpace E] [BorelSpace E] [MeasurableSpace I] [Fintype I] [MeasurableSingletonClass I] in
107 theorem step_cell_integral (bin : Y → I) (a : A) (i : I) (z : E) :
108     (∫ r in ({a} ×ˢ (bin ⁻¹' {i})), D.op r.1 r.2 z ∂stepReference (A := A) μ) =
109       cellOperator μ (D.op a) (bin ⁻¹' {i}) z := by
110   have hint : IntegrableOn (fun r : A × Y => D.op r.1 r.2 z)
111       ({a} ×ˢ (bin ⁻¹' {i})) (stepReference (A := A) μ) :=
112     ((ContinuousLinearMap.apply ℝ E z).integrable_comp (jointOperator_integrable D)).integrableOn
113   rw [stepReference, setIntegral_prod _ hint]
114   simp only [integral_singleton, Measure.real, Measure.count_singleton, ENNReal.toReal_one, one_smul]
115   exact (cellOperator_apply μ (D.op a) (D.integrable_op a) _ z).symm
116 
117 set_option backward.isDefEq.respectTransparency false in
118 omit [MeasurableSpace E] [BorelSpace E] [Fintype I] [MeasurableSingletonClass I] in
119 /-- Integrating the actual fine operator product over the complete bin fiber
120 produces the literal chronological product of integrated cell operators. -/
121 theorem run_binFiber_integral (bin : Y → I) (hbin : Measurable bin) (z : E) :
122     (n : ℕ) → ∀ b : History (A × I) n,
123       (∫ h in binFiber bin n b, ContinuousRecords.run D z n h ∂reference (stepReference (A := A) μ) n) =
124         binnedRun D bin z n b
125   | 0, b => by
126     have hb : b = PUnit.unit := Subsingleton.elim _ _
127     subst b
128     simp [binFiber, historyMap, reference, ContinuousRecords.run, binnedRun]
129   | n+1, b => by
130     rw [binFiber_succ, reference, setIntegral_prod _ (run_integrable D z (n+1)).integrableOn]
131     change (∫ h in binFiber bin n b.1, ∫ r in ({b.2.1} ×ˢ (bin ⁻¹' {b.2.2})),
132       D.op r.1 r.2 (ContinuousRecords.run D z n h) ∂stepReference (A := A) μ
133       ∂reference (stepReference (A := A) μ) n) = _
134     simp_rw [step_cell_integral D bin]
135     rw [(cellOperator μ (D.op b.2.1) (bin ⁻¹' {b.2.2})).integral_comp_comm
136       (run_integrable D z n).integrableOn, run_binFiber_integral bin hbin z n b.1]
137     rfl
138 
139 /-- A real finite-action policy on exactly the observed bin history. -/
140 def binWeight (π : List (A × I) → A → ℝ) : (n : ℕ) → History (A × I) n → ℝ
141   | 0, _ => 1
142   | n+1, b => binWeight π n b.1 * π (historyList n b.1) b.2.1
143 
144 omit [MeasurableSpace A] [MeasurableSingletonClass A] [MeasurableSpace I] [Fintype I]
145   [MeasurableSingletonClass I] in
146 theorem binWeight_nonneg (π : List (A × I) → A → ℝ) (hπ : ∀ h, FiniteBayes.IsPrior (π h)) :
147     (n : ℕ) → ∀ b : History (A × I) n, 0 ≤ binWeight π n b
148   | 0, _ => by norm_num [binWeight]
149   | n+1, b => mul_nonneg (binWeight_nonneg π hπ n b.1) ((hπ _).1 _)
150 
151 /-- The fine policy reads only the measurable bin record. -/
152 def liftedBinPolicy (bin : Y → I) (hbin : Measurable bin)
153     (π : List (A × I) → A → ℝ) (hπ : ∀ h, FiniteBayes.IsPrior (π h)) :
154     ContinuousRecords.Policy (A := A) (Y := Y) where
155   probability n h a := ENNReal.ofReal (π (historyList n (historyMap (binStep bin) n h)) a)
156   measurable_probability n a := by
157     have hm : Measurable (fun b : History (A × I) n => ENNReal.ofReal (π (historyList n b) a)) :=
158       Measurable.of_discrete
159     exact hm.comp (historyMap_measurable _ (binStep_measurable bin hbin) n)
160   sum_one n h := by
161     rw [← ENNReal.ofReal_sum_of_nonneg (fun a _ => (hπ _).1 a), (hπ _).2, ENNReal.ofReal_one]
162 
163 theorem liftedBinPolicy_weight (bin : Y → I) (hbin : Measurable bin)
164     (π : List (A × I) → A → ℝ) (hπ : ∀ h, FiniteBayes.IsPrior (π h)) :
165     (n : ℕ) → ∀ h : History (A × Y) n,
166       (liftedBinPolicy bin hbin π hπ).weight n h = ENNReal.ofReal (binWeight π n (historyMap (binStep bin) n h))
167   | 0, _ => by simp [ContinuousRecords.Policy.weight, binWeight]
168   | n+1, h => by
169     change (liftedBinPolicy bin hbin π hπ).weight n h.1 *
170       ENNReal.ofReal (π (historyList n (historyMap (binStep bin) n h.1)) h.2.1) =
171       ENNReal.ofReal (binWeight π n (historyMap (binStep bin) n h.1) *
172         π (historyList n (historyMap (binStep bin) n h.1)) h.2.1)
173     rw [liftedBinPolicy_weight bin hbin π hπ n h.1,
174       ENNReal.ofReal_mul (binWeight_nonneg π hπ n _)]
175 
176 /-- The actual finite model uses integrated cell operators with the same policy. -/
177 def binnedBranches (bin : Y → I) (π : List (A × I) → A → ℝ)
178     (h : List (A × I)) (s : A × I) : E →ₗ[ℝ] E :=
179   π h s.1 • (cellOperator μ (D.op s.1) (bin ⁻¹' {s.2})).toLinearMap
180 
181 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace A]
182   [Fintype A] [MeasurableSingletonClass A] in
183 theorem bin_cell_instrument (bin : Y → I) (hbin : Measurable bin) (a : A) :
184     C.Instrument (fun i => (cellOperator μ (D.op a) (bin ⁻¹' {i})).toLinearMap) := by
185   apply cellInstrument C μ (D.op a) (D.integrable_op a) (D.positive a) (D.mass_preserving a)
186     (fun i => bin ⁻¹' {i}) (fun i => hbin (measurableSet_singleton i))
187   · intro i j hij
188     apply Set.disjoint_left.mpr
189     intro y hi hj
190     apply hij
191     exact hi.symm.trans hj
192   · ext y
193     simp
194 
195 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace A]
196   [MeasurableSingletonClass A] in
197 theorem binnedBranches_instrument (bin : Y → I) (hbin : Measurable bin)
198     (π : List (A × I) → A → ℝ) (hπ : ∀ h, FiniteBayes.IsPrior (π h)) (h : List (A × I)) :
199     C.Instrument (binnedBranches D bin π h) := by
200   exact ObservationTree.policy_instrument C π hπ
201     (fun _ s => (cellOperator μ (D.op s.1) (bin ⁻¹' {s.2})).toLinearMap)
202     (fun _ a => bin_cell_instrument D bin hbin a) h
203 
204 def weightedBinnedRun (bin : Y → I) (π : List (A × I) → A → ℝ) (z : E) :
205     (n : ℕ) → History (A × I) n → E
206   | 0, _ => z
207   | n+1, b => binnedBranches D bin π (historyList n b.1) b.2 (weightedBinnedRun bin π z n b.1)
208 
209 omit [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
210   [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A] [MeasurableSpace I] [Fintype I]
211   [MeasurableSingletonClass I] [IsProbabilityMeasure μ] in
212 theorem weightedBinnedRun_factor (bin : Y → I) (π : List (A × I) → A → ℝ) (z : E) :
213     (n : ℕ) → ∀ b : History (A × I) n,
214       weightedBinnedRun D bin π z n b = binWeight π n b • binnedRun D bin z n b
215   | 0, _ => by simp [weightedBinnedRun, binWeight, binnedRun]
216   | n+1, b => by
217     simp only [weightedBinnedRun, binnedBranches, weightedBinnedRun_factor bin π z n b.1,
218       LinearMap.smul_apply, ContinuousLinearMap.coe_coe, map_smul, smul_smul, binWeight, binnedRun]
219 
220 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace A]
221   [MeasurableSingletonClass A] in
222 theorem weightedBinnedRun_mem (bin : Y → I) (hbin : Measurable bin)
223     (π : List (A × I) → A → ℝ) (hπ : ∀ h, FiniteBayes.IsPrior (π h))
224     (z : E) (hz : z ∈ C.carrier) : (n : ℕ) → ∀ b : History (A × I) n,
225       weightedBinnedRun D bin π z n b ∈ C.carrier
226   | 0, _ => hz
227   | n+1, b => (binnedBranches_instrument D bin hbin π hπ _).1 b.2 _
228       (weightedBinnedRun_mem bin hbin π hπ z hz n b.1)
229 
230 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace A]
231   [MeasurableSingletonClass A] in
232 theorem weightedBinnedRun_mass (bin : Y → I) (hbin : Measurable bin)
233     (π : List (A × I) → A → ℝ) (hπ : ∀ h, FiniteBayes.IsPrior (π h)) (z : E) :
234     (n : ℕ) → (∑ b : History (A × I) n, C.mass (weightedBinnedRun D bin π z n b)) = C.mass z
235   | 0 => by change (∑ _ : PUnit, C.mass z) = _; simp
236   | n+1 => by
237     change (∑ b : History (A × I) n × (A × I), C.mass
238       (binnedBranches D bin π (historyList n b.1) b.2 (weightedBinnedRun D bin π z n b.1))) = _
239     rw [Fintype.sum_prod_type]
240     simp_rw [(binnedBranches_instrument D bin hbin π hπ _).2]
241     exact weightedBinnedRun_mass bin hbin π hπ z n
242 
243 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace A]
244   [MeasurableSingletonClass A] in
245 /-- The finite cell-model record distribution is a prior at every horizon. -/
246 theorem binned_record_prior (bin : Y → I) (hbin : Measurable bin)
247     (π : List (A × I) → A → ℝ) (hπ : ∀ h, FiniteBayes.IsPrior (π h))
248     (z : E) (hz : z ∈ C.base) (n : ℕ) :
249     FiniteBayes.IsPrior (fun b : History (A × I) n => C.mass (weightedBinnedRun D bin π z n b)) :=
250   ⟨fun b => C.mass_nonneg (weightedBinnedRun_mem D bin hbin π hπ z hz.1 n b),
251     (weightedBinnedRun_mass D bin hbin π hπ z n).trans hz.2⟩
252 
253 /-- An actual measure associated to that finite instrument's prior. -/
254 def finiteBinnedLaw (bin : Y → I) (π : List (A × I) → A → ℝ) (z : E) (n : ℕ) :
255     Measure (History (A × I) n) :=
256   Measure.count.withDensity (fun b => ENNReal.ofReal (C.mass (weightedBinnedRun D bin π z n b)))
257 
258 omit [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
259   [Fintype A] [Fintype I] [IsProbabilityMeasure μ] in
260 theorem finiteBinnedLaw_singleton (bin : Y → I) (π : List (A × I) → A → ℝ) (z : E)
261     (n : ℕ) (b : History (A × I) n) :
262     finiteBinnedLaw D bin π z n {b} = ENNReal.ofReal (C.mass (weightedBinnedRun D bin π z n b)) := by
263   rw [finiteBinnedLaw, withDensity_apply _ (measurableSet_singleton b), lintegral_singleton]
264   simp
265 
266 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] in
267 theorem finiteBinnedLaw_probability (bin : Y → I) (hbin : Measurable bin)
268     (π : List (A × I) → A → ℝ) (hπ : ∀ h, FiniteBayes.IsPrior (π h))
269     (z : E) (hz : z ∈ C.base) (n : ℕ) : IsProbabilityMeasure (finiteBinnedLaw D bin π z n) := by
270   constructor
271   rw [finiteBinnedLaw, withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ,
272     lintegral_count, tsum_fintype, ← ENNReal.ofReal_sum_of_nonneg
273       (fun b _ => (binned_record_prior D bin hbin π hπ z hz n).1 b),
274     (binned_record_prior D bin hbin π hπ z hz n).2, ENNReal.ofReal_one]
275 
276 omit [Fintype I] [MeasurableSingletonClass I] in
277 /-- The actual nonnegative record density integrated over one bin fiber. -/
278 theorem mass_run_binFiber_lintegral (bin : Y → I) (hbin : Measurable bin)
279     (z : E) (hz : z ∈ C.carrier) (n : ℕ) (b : History (A × I) n) :
280     (∫⁻ h in binFiber bin n b, ENNReal.ofReal (C.mass (ContinuousRecords.run D z n h))
281       ∂reference (stepReference (A := A) μ) n) = ENNReal.ofReal (C.mass (binnedRun D bin z n b)) := by
282   have hint : Integrable (fun h => C.mass (ContinuousRecords.run D z n h))
283       (reference (stepReference (A := A) μ) n) :=
284     (ContinuousInstrument.massCLM C).integrable_comp (run_integrable D z n)
285   rw [← ofReal_integral_eq_lintegral_ofReal hint.integrableOn
286     (ae_restrict_of_ae ((ContinuousRecords.run_mem_ae D hz n).mono fun _ hh => C.mass_nonneg hh))]
287   congr 1
288   exact ((ContinuousInstrument.massCLM C).integral_comp_comm (run_integrable D z n).integrableOn).trans
289     (congrArg (ContinuousInstrument.massCLM C) (run_binFiber_integral D bin hbin z n b))
290 
291 /-- The probability of every complete binned record is exactly the finite
292 integrated-cell model's probability, including the action-policy factors. -/
293 theorem binned_recordLaw_singleton (bin : Y → I) (hbin : Measurable bin)
294     (π : List (A × I) → A → ℝ) (hπ : ∀ h, FiniteBayes.IsPrior (π h))
295     (z : E) (hz : z ∈ C.carrier) (n : ℕ) (b : History (A × I) n) :
296     ((ContinuousRecords.recordLaw D (liftedBinPolicy bin hbin π hπ) z n).map
297       (historyMap (binStep bin) n)) {b} = finiteBinnedLaw D bin π z n {b} := by
298   rw [Measure.map_apply (historyMap_measurable _ (binStep_measurable bin hbin) n)
299     (measurableSet_singleton b), finiteBinnedLaw_singleton]
300   change ContinuousRecords.recordLaw D (liftedBinPolicy bin hbin π hπ) z n (binFiber bin n b) = _
301   rw [ContinuousRecords.recordLaw_event _ _ _ _ _ (binFiber_measurable bin hbin n b)]
302   have hweight : ∀ᵐ h ∂(reference (stepReference (A := A) μ) n).restrict (binFiber bin n b),
303       (liftedBinPolicy bin hbin π hπ).weight n h = ENNReal.ofReal (binWeight π n b) := by
304     filter_upwards [ae_restrict_mem (binFiber_measurable bin hbin n b)] with h hh
305     rw [liftedBinPolicy_weight]
306     exact congrArg (fun q => ENNReal.ofReal (binWeight π n q)) hh
307   calc
308     _ = ∫⁻ h in binFiber bin n b, ENNReal.ofReal (binWeight π n b) *
309         ENNReal.ofReal (C.mass (ContinuousRecords.run D z n h))
310         ∂reference (stepReference (A := A) μ) n := by
311       apply lintegral_congr_ae
312       filter_upwards [hweight] with h hh
313       exact congrArg (fun w => w * ENNReal.ofReal (C.mass (ContinuousRecords.run D z n h))) hh
314     _ = ENNReal.ofReal (binWeight π n b) *
315         ∫⁻ h in binFiber bin n b, ENNReal.ofReal (C.mass (ContinuousRecords.run D z n h))
316           ∂reference (stepReference (A := A) μ) n := by
317       apply lintegral_const_mul
318       exact ((ContinuousInstrument.massCLM C).continuous.measurable.comp
319         (ContinuousRecords.run_measurable D z n)).ennreal_ofReal
320     _ = ENNReal.ofReal (binWeight π n b) * ENNReal.ofReal (C.mass (binnedRun D bin z n b)) := by
321       rw [mass_run_binFiber_lintegral D bin hbin z hz n b]
322     _ = _ := by
323       rw [weightedBinnedRun_factor, map_smul, smul_eq_mul,
324         ENNReal.ofReal_mul (binWeight_nonneg π hπ n b)]
325 
326 /-- P56's equality of actual measures at every horizon. The continuous policy
327 is allowed to depend on the entire action/bin history and only that history. -/
328 theorem actual_binned_recordLaw (bin : Y → I) (hbin : Measurable bin)
329     (π : List (A × I) → A → ℝ) (hπ : ∀ h, FiniteBayes.IsPrior (π h))
330     (z : E) (hz : z ∈ C.carrier) (n : ℕ) :
331     (ContinuousRecords.recordLaw D (liftedBinPolicy bin hbin π hπ) z n).map
332       (historyMap (binStep bin) n) = finiteBinnedLaw D bin π z n := by
333   apply Measure.ext_of_singleton
334   intro b
335   exact binned_recordLaw_singleton D bin hbin π hπ z hz n b
336 
337 /-- A covering partition supplies a literal bin map, without assuming one. -/
338 def partitionBin (S : I → Set Y) (hcover : ⋃ i, S i = Set.univ) (y : Y) : I :=
339   Classical.choose (show ∃ i, y ∈ S i from Set.mem_iUnion.mp (hcover.symm ▸ Set.mem_univ y))
340 
341 omit [MeasurableSpace Y] [MeasurableSpace I] [Fintype I] [MeasurableSingletonClass I] in
342 theorem partitionBin_mem (S : I → Set Y) (hcover : ⋃ i, S i = Set.univ) (y : Y) :
343     y ∈ S (partitionBin S hcover y) :=
344   Classical.choose_spec (show ∃ i, y ∈ S i from Set.mem_iUnion.mp (hcover.symm ▸ Set.mem_univ y))
345 
346 omit [MeasurableSpace Y] [MeasurableSpace I] [Fintype I] [MeasurableSingletonClass I] in
347 theorem partitionBin_fiber (S : I → Set Y) (hcover : ⋃ i, S i = Set.univ)
348     (hdis : Pairwise (fun i j => Disjoint (S i) (S j))) (i : I) :
349     partitionBin S hcover ⁻¹' {i} = S i := by
350   ext y
351   constructor
352   · intro hy
353     exact hy ▸ partitionBin_mem S hcover y
354   · intro hy
355     change partitionBin S hcover y = i
356     by_contra hne
357     exact Set.disjoint_left.mp (hdis hne) (partitionBin_mem S hcover y) hy
358 
359 omit [MeasurableSingletonClass I] in
360 theorem partitionBin_measurable (S : I → Set Y) (hcover : ⋃ i, S i = Set.univ)
361     (hdis : Pairwise (fun i j => Disjoint (S i) (S j))) (hS : ∀ i, MeasurableSet (S i)) :
362     Measurable (partitionBin S hcover) := by
363   apply measurable_to_countable
364   intro y
365   rw [partitionBin_fiber S hcover hdis]
366   exact hS _
367 
368 /-- P56 for any finite measurable partition: the constructed measurable map has
369 exactly those cells and pushes the actual law to the finite integrated model. -/
370 theorem exact_partition_coarsening (S : I → Set Y) (hcover : ⋃ i, S i = Set.univ)
371     (hdis : Pairwise (fun i j => Disjoint (S i) (S j))) (hS : ∀ i, MeasurableSet (S i))
372     (π : List (A × I) → A → ℝ) (hπ : ∀ h, FiniteBayes.IsPrior (π h))
373     (z : E) (hz : z ∈ C.base) (n : ℕ) :
374     (∀ i, partitionBin S hcover ⁻¹' {i} = S i) ∧
375     (∀ h, C.Instrument (binnedBranches D (partitionBin S hcover) π h)) ∧
376     FiniteBayes.IsPrior (fun b : History (A × I) n =>
377       C.mass (weightedBinnedRun D (partitionBin S hcover) π z n b)) ∧
378     (ContinuousRecords.recordLaw D
379       (liftedBinPolicy (partitionBin S hcover) (partitionBin_measurable S hcover hdis hS) π hπ) z n).map
380         (historyMap (binStep (partitionBin S hcover)) n) =
381           finiteBinnedLaw D (partitionBin S hcover) π z n := by
382   refine ⟨partitionBin_fiber S hcover hdis, ?_, ?_, ?_⟩
383   · exact binnedBranches_instrument D _ (partitionBin_measurable S hcover hdis hS) π hπ
384   · exact binned_record_prior D _ (partitionBin_measurable S hcover hdis hS) π hπ z hz n
385   · exact actual_binned_recordLaw D _ (partitionBin_measurable S hcover hdis hS) π hπ z hz.1 n
386 
387 omit [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
388   [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A] [MeasurableSpace I] [Fintype I]
389   [MeasurableSingletonClass I] [IsProbabilityMeasure μ] in
390 /-- A bin-history policy factor commutes with exact cell integration. -/
391 theorem policy_density_cell (π : List (A × I) → A → ℝ) (h : List (A × I)) (a : A)
392     (S : Set Y) :
393     cellOperator μ (fun y => π h a • D.op a y) S = π h a • cellOperator μ (D.op a) S := by
394   exact integral_smul _ _
395 
396 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace A]
397   [Fintype A] [MeasurableSingletonClass A] [MeasurableSpace I] [Fintype I]
398   [MeasurableSingletonClass I] [IsProbabilityMeasure μ] in
399 /-- The earlier chronological repeated-integral theorem instantiated with the
400 literal policy-weighted density is the actual finite cell branch model. -/
401 theorem policy_iterated_record_probability (bin : Y → I)
402     (π : List (A × I) → A → ℝ) (n : ℕ) (h : List (A × I)) (z : E)
403     (w : ObservationTree.Record (A × I) n) :
404     C.mass (iteratedCellVector μ (fun h a y => π h a • D.op a y)
405       (fun i => bin ⁻¹' {i}) h (ObservationTree.recordList w) z) =
406         ObservationTree.recordLaw C (binnedBranches D bin π) n h z w := by
407   have hB : ∀ h a, Integrable (fun y => π h a • D.op a y) μ :=
408     fun h a => Integrable.smul (π h a) (D.integrable_op a)
409   have heq : (fun h (s : A × I) =>
410       (cellOperator μ (fun y => π h s.1 • D.op s.1 y) (bin ⁻¹' {s.2})).toLinearMap) =
411         binnedBranches D bin π := by
412     funext h s
413     rw [policy_density_cell]
414     rfl
415   rw [iterated_cell_record_probability C μ _ hB, heq]
416 
417 namespace QuadraticExample
418 
419 def op (u : ℝ) : ℝ →L[ℝ] ℝ := (3 * u^2) • ContinuousLinearMap.id ℝ ℝ
420 
421 theorem op_integrable : Integrable op UniformIntervalMoments.measure :=
422   (UniformIntervalMoments.continuous_integrable (by fun_prop : Continuous (fun u : ℝ => 3 * u^2))).smul_const _
423 
424 /-- A valid normalized scalar density that vanishes at the bin midpoint. -/
425 def instrument : ContinuousInstrument.DensityInstrument (A := Unit)
426     BaseNorm.scalarCone UniformIntervalMoments.measure where
427   op _ := op
428   measurable_op _ := by unfold op; fun_prop
429   integrable_op _ := op_integrable
430   positive _ := ae_of_all _ fun u z hz => mul_nonneg (by positivity : 0 ≤ 3 * u^2) hz
431   mass_preserving _ z := by
432     rw [ContinuousLinearMap.integral_apply op_integrable z]
433     change (∫ u, (3 * u^2) * z ∂UniformIntervalMoments.measure) = z
434     rw [integral_mul_const, integral_const_mul]
435     change 3 * UniformIntervalMoments.moment 2 * z = z
436     rw [UniformIntervalMoments.moment_two]
437     ring
438 
439 theorem full_cell : cellOperator UniformIntervalMoments.measure (instrument.op ()) Set.univ 1 = 1 := by
440   rw [cellOperator, Measure.restrict_univ]
441   exact instrument.mass_preserving () 1
442 
443 theorem midpoint : instrument.op () 0 1 = 0 := by norm_num [instrument, op]
444 
445 theorem integrated_cell_ne_point_sample :
446     cellOperator UniformIntervalMoments.measure (instrument.op ()) Set.univ 1 ≠ instrument.op () 0 1 := by
447   rw [full_cell, midpoint]
448   norm_num
449 
450 end QuadraticExample
451 
452 end
453 end Komorebi.LSM.ContinuousBins

Back to source controls