Large Signal Model · Lean source
ContinuousRecords.lean
Declared contract recorded Coverage and evidence
The cited release explicitly reports completion of its registered formal contract, under its exact hypotheses.
This viewer reads the retained source; it does not run Lean or assign new claim mappings.
Local imports (1)
KomorebiLSM/ContinuousRecords.lean536 lines
Original source path
Lean/KomorebiLSM/ContinuousRecords.leanSkip declarations and read code
1 import KomorebiLSM.ContinuousInstrument
2 import Mathlib.MeasureTheory.Measure.Prod
3 import Mathlib.MeasureTheory.Integral.Lebesgue.Countable
4 import Mathlib.Probability.Kernel.Composition.WithDensity
5
6 /-! Finite continuous record laws are literal densities of operator products.
7 Policy factors are measurable and normalized at each history. Normalization and
8 prefix consistency are derived by integration, rather than supplied as fields. -/
9 set_option autoImplicit false
10 namespace Komorebi.LSM.ContinuousRecords
11 open MeasureTheory ProbabilityTheory
12 open scoped ENNReal BigOperators
13
14 universe u
15 /-- A finite ordered record, extended on the right. -/
16 def History (X : Type u) : ℕ → Type u
17 | 0 => PUnit.{u+1}
18 | n+1 => History X n × X
19
20 instance historyMeasurable {X : Type*} [MeasurableSpace X] :
21 (n : ℕ) → MeasurableSpace (History X n)
22 | 0 => inferInstanceAs (MeasurableSpace PUnit)
23 | n+1 => by
24 letI := historyMeasurable (X := X) n
25 exact inferInstanceAs (MeasurableSpace (History X n × X))
26
27 attribute [reducible] History
28
29 /-- The actual iterated product reference measure, including the empty record. -/
30 noncomputable def reference {X : Type*} [MeasurableSpace X] (ν : Measure X) :
31 (n : ℕ) → Measure (History X n)
32 | 0 => Measure.dirac PUnit.unit
33 | n+1 => (reference ν n).prod ν
34
35 instance reference_finite {X : Type*} [MeasurableSpace X] (ν : Measure X)
36 [IsFiniteMeasure ν] : (n : ℕ) → IsFiniteMeasure (reference ν n)
37 | 0 => inferInstanceAs (IsFiniteMeasure (Measure.dirac PUnit.unit))
38 | n+1 => by
39 let := reference_finite ν n
40 exact inferInstanceAs (IsFiniteMeasure ((reference ν n).prod ν))
41
42 /-- Remove a specified number of terminal records. -/
43 def truncate {X : Type*} (n : ℕ) : (k : ℕ) → History X (n+k) → History X n
44 | 0,h => h
45 | k+1,h => truncate n k h.1
46
47 theorem truncate_measurable {X : Type*} [MeasurableSpace X] (n : ℕ) :
48 (k : ℕ) → Measurable (truncate (X := X) n k)
49 | 0 => measurable_id
50 | k+1 => (truncate_measurable n k).comp measurable_fst
51
52 /-- Apply a measurable observation or record map coordinate by coordinate. -/
53 def mapHistory {X Z : Type*} (f : X → Z) : (n : ℕ) → History X n → History Z n
54 | 0,_ => PUnit.unit
55 | n+1,h => (mapHistory f n h.1,f h.2)
56
57 theorem mapHistory_measurable {X Z : Type*} [MeasurableSpace X] [MeasurableSpace Z]
58 {f : X → Z} (hf : Measurable f) : (n : ℕ) → Measurable (mapHistory f n)
59 | 0 => measurable_const
60 | n+1 => ((mapHistory_measurable hf n).comp measurable_fst).prodMk (hf.comp measurable_snd)
61
62 theorem mapHistory_first_marginal {X Z : Type*} [MeasurableSpace X] [MeasurableSpace Z]
63 {f : X → Z} (hf : Measurable f) (n : ℕ) (ν : Measure (History X (n+1))) :
64 (ν.map (mapHistory f (n+1))).fst=ν.fst.map (mapHistory f n) := by
65 exact (Measure.map_map (μ := ν) measurable_fst (mapHistory_measurable hf (n+1))).trans
66 (Measure.map_map (μ := ν) (mapHistory_measurable hf n) measurable_fst).symm
67
68 /-- Integrating the last coordinate gives the actual first marginal. -/
69 theorem density_first_marginal {X Z : Type*} [MeasurableSpace X] [MeasurableSpace Z]
70 (ν : Measure X) (η : Measure Z) [SFinite ν] [SFinite η]
71 (f : X × Z → ℝ≥0∞) (g : X → ℝ≥0∞) (hf : Measurable f)
72 (h : ∀ᵐ x∂ν,(∫⁻ y,f (x,y)∂η)=g x) :
73 ((ν.prod η).withDensity f).fst=ν.withDensity g := by
74 ext S hS
75 rw [Measure.fst_apply hS,withDensity_apply _ (measurable_fst hS),
76 withDensity_apply _ hS]
77 have he : Prod.fst ⁻¹' S=S ×ˢ (Set.univ : Set Z) := Set.ext (by simp)
78 rw [he,setLIntegral_prod _ hf.aemeasurable]
79 simp only [Measure.restrict_univ]
80 exact lintegral_congr_ae (h.filter_mono (ae_mono Measure.restrict_le_self))
81
82 variable {E A Y : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
83 variable [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
84 variable [MeasurableSpace Y] [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A]
85 variable {C : BaseNorm.ProbabilityCone E} {μ : Measure Y}
86 variable (D : ContinuousInstrument.DensityInstrument (A := A) C μ)
87
88 /-- The genuine unnormalized operator product on a recorded action/observation history. -/
89 noncomputable def run (z : E) : (n : ℕ) → History (A × Y) n → E
90 | 0, _ => z
91 | n+1, h => D.op h.2.1 h.2.2 (run z n h.1)
92
93 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] in
94 theorem op_measurable : Measurable (Function.uncurry D.op) :=
95 measurable_from_prod_countable_right D.measurable_op
96
97 theorem run_measurable (z : E) : (n : ℕ) → Measurable (run D z n)
98 | 0 => measurable_const
99 | n+1 => by
100 exact (isBoundedBilinearMap_apply (𝕜 := ℝ) (E := E) (F := E)).continuous.measurable.comp
101 (((op_measurable D).comp measurable_snd).prodMk ((run_measurable z n).comp measurable_fst))
102
103 /-- Any measurable randomized finite-action policy, with explicit pointwise normalization. -/
104 structure Policy where
105 probability : (n : ℕ) → History (A × Y) n → A → ℝ≥0∞
106 measurable_probability : ∀ n a,Measurable (fun h => probability n h a)
107 sum_one : ∀ n h,∑ a,probability n h a=1
108
109 namespace Policy
110 variable (π : Policy (A := A) (Y := Y))
111
112 noncomputable def weight : (n : ℕ) → History (A × Y) n → ℝ≥0∞
113 | 0, _ => 1
114 | n+1, h => weight n h.1 * π.probability n h.1 h.2.1
115
116 theorem weight_measurable : (n : ℕ) → Measurable (π.weight n)
117 | 0 => measurable_const
118 | n+1 => by
119 have hp : Measurable (fun p : History (A × Y) n × A => π.probability n p.1 p.2) :=
120 measurable_from_prod_countable_left (π.measurable_probability n)
121 exact ((weight_measurable n).comp measurable_fst).mul
122 (hp.comp (measurable_fst.prodMk (measurable_fst.comp measurable_snd)))
123
124 end Policy
125
126 /-- The counting-action and observation reference for one recorded step. -/
127 noncomputable def stepReference (μ : Measure Y) : Measure (A × Y) := Measure.count.prod μ
128
129 instance stepReference_finite [IsFiniteMeasure μ] :
130 IsFiniteMeasure (stepReference (A := A) μ) :=
131 inferInstanceAs (IsFiniteMeasure (Measure.count.prod μ))
132
133 /-- Policy factors multiply the mass of the actual operator product. -/
134 noncomputable def recordDensity (π : Policy (A := A) (Y := Y)) (z : E) (n : ℕ)
135 (h : History (A × Y) n) : ℝ≥0∞ := π.weight n h * ENNReal.ofReal (C.mass (run D z n h))
136
137 theorem recordDensity_measurable (π : Policy (A := A) (Y := Y)) (z : E) (n : ℕ) :
138 Measurable (recordDensity D π z n) :=
139 (Policy.weight_measurable π n).mul (((ContinuousInstrument.massCLM C).continuous.measurable.comp
140 (run_measurable D z n)).ennreal_ofReal)
141
142 /-- An actual measure on finite action/observation records. -/
143 noncomputable def recordLaw (π : Policy (A := A) (Y := Y)) (z : E) (n : ℕ) :
144 Measure (History (A × Y) n) :=
145 (reference (stepReference (A := A) μ) n).withDensity (recordDensity D π z n)
146
147
148 variable [IsProbabilityMeasure μ]
149
150 theorem run_mem_ae {z : E} (hz : z∈C.carrier) : (n : ℕ) →
151 ∀ᵐ h∂reference (stepReference (A := A) μ) n,run D z n h∈C.carrier
152 | 0 => by simpa [run] using Filter.Eventually.of_forall (fun _ => hz)
153 | n+1 => by
154 apply (Measure.ae_prod_iff_ae_ae (C.closed.measurableSet.preimage (run_measurable D z (n+1)))).mpr
155 filter_upwards [run_mem_ae hz n] with h hh
156 apply (Measure.ae_prod_iff_ae_ae (C.closed.measurableSet.preimage
157 ((run_measurable D z (n+1)).comp (measurable_const.prodMk measurable_id)))).mpr
158 rw [Measure.ae_count_iff]
159 intro a
160 filter_upwards [D.positive a] with y hy
161 exact hy _ hh
162
163 omit [MeasurableSpace E] [BorelSpace E] [MeasurableSpace A] [Fintype A]
164 [MeasurableSingletonClass A] [IsProbabilityMeasure μ] in
165 theorem integrated_density_mass (a : A) {z : E} (hz : z∈C.carrier) :
166 (∫⁻ y,ENNReal.ofReal (D.density a y z)∂μ)=ENNReal.ofReal (C.mass z) := by
167 rw [← ofReal_integral_eq_lintegral_ofReal (D.density_integrable a z)
168 (D.density_nonneg_ae a hz),D.integral_density a z]
169
170 theorem recordDensity_integrate_last (π : Policy (A := A) (Y := Y))
171 (z : E) (n : ℕ) (h : History (A × Y) n) (hh : run D z n h∈C.carrier) :
172 (∫⁻ r,recordDensity D π z (n+1) (h,r)∂stepReference (A := A) μ)=
173 recordDensity D π z n h := by
174 have hm : Measurable (fun r : A × Y => recordDensity D π z (n+1) (h,r)) :=
175 (recordDensity_measurable D π z (n+1)).comp (measurable_const.prodMk measurable_id)
176 rw [stepReference,lintegral_prod _ hm.aemeasurable]
177 change (∫⁻ a,∫⁻ y,(π.weight n h * π.probability n h a) *
178 ENNReal.ofReal (D.density a y (run D z n h))∂μ∂Measure.count)=recordDensity D π z n h
179 have hi (a : A) : (∫⁻ y,(π.weight n h * π.probability n h a) *
180 ENNReal.ofReal (D.density a y (run D z n h))∂μ)=
181 (π.weight n h * π.probability n h a)*ENNReal.ofReal (C.mass (run D z n h)) := by
182 have hd : Measurable (fun y : Y => ENNReal.ofReal (D.density a y (run D z n h))) :=
183 ((D.density_measurable a).comp (measurable_const.prodMk measurable_id)).ennreal_ofReal
184 rw [lintegral_const_mul _ hd,integrated_density_mass D a hh]
185 simp_rw [hi,lintegral_count,tsum_fintype]
186 rw [← Finset.sum_mul,← Finset.mul_sum,π.sum_one,mul_one]
187 rfl
188
189
190
191 /-- Consistency is the equality of literal prefix marginals. -/
192 theorem recordLaw_consistent (π : Policy (A := A) (Y := Y)) {z : E}
193 (hz : z∈C.carrier) (n : ℕ) :
194 (recordLaw D π z (n+1)).fst=recordLaw D π z n := by
195 apply density_first_marginal _ _ _ _ (recordDensity_measurable D π z (n+1))
196 filter_upwards [run_mem_ae D hz n] with h hh
197 exact recordDensity_integrate_last D π z n h hh
198
199 /-- Every finite record law has total probability one. -/
200 theorem recordLaw_univ (π : Policy (A := A) (Y := Y))
201 (z : ContinuousInstrument.DensityInstrument.State C) :
202 (n : ℕ) → recordLaw D π z.1 n Set.univ=1
203 | 0 => by simp [recordLaw,reference,recordDensity,Policy.weight,run,z.2.2]
204 | n+1 => by
205 have hm := congrArg (fun ν : Measure (History (A × Y) n) => ν Set.univ)
206 (recordLaw_consistent D π z.2.1 n)
207 exact (Measure.fst_univ (ρ := recordLaw D π z.1 (n+1))).symm.trans (hm.trans (recordLaw_univ π z n))
208
209 instance recordLaw_probability (π : Policy (A := A) (Y := Y))
210 (z : ContinuousInstrument.DensityInstrument.State C) (n : ℕ) :
211 IsProbabilityMeasure (recordLaw D π z.1 n) := ⟨recordLaw_univ D π z n⟩
212
213 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
214 [MeasurableSingletonClass A] [IsProbabilityMeasure μ] in
215 theorem recordLaw_event (π : Policy (A := A) (Y := Y)) (z : E) (n : ℕ)
216 (S : Set (History (A × Y) n)) (hS : MeasurableSet S) :
217 recordLaw D π z n S=∫⁻ h in S,recordDensity D π z n h∂reference (stepReference (A := A) μ) n :=
218 withDensity_apply _ hS
219
220
221 /-- Prescribed actions retain the genuine, unnormalized chronological product. -/
222 noncomputable def observationRun (actions : ℕ → A) (z : E) :
223 (n : ℕ) → History Y n → E
224 | 0, _ => z
225 | n+1,h => D.op (actions n) h.2 (observationRun actions z n h.1)
226
227 omit [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A] [IsProbabilityMeasure μ] in
228 theorem observationRun_measurable (actions : ℕ → A) (z : E) :
229 (n : ℕ) → Measurable (observationRun D actions z n)
230 | 0 => measurable_const
231 | n+1 => by
232 exact (isBoundedBilinearMap_apply (𝕜 := ℝ) (E := E) (F := E)).continuous.measurable.comp
233 (((D.measurable_op (actions n)).comp measurable_snd).prodMk
234 ((observationRun_measurable actions z n).comp measurable_fst))
235
236 omit [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A] in
237 theorem observationRun_mem_ae (actions : ℕ → A) {z : E} (hz : z∈C.carrier) :
238 (n : ℕ) → ∀ᵐ h∂reference μ n,observationRun D actions z n h∈C.carrier
239 | 0 => by simpa [observationRun] using Filter.Eventually.of_forall (fun _ => hz)
240 | n+1 => by
241 apply (Measure.ae_prod_iff_ae_ae (C.closed.measurableSet.preimage
242 (observationRun_measurable D actions z (n+1)))).mpr
243 filter_upwards [observationRun_mem_ae actions hz n] with h hh
244 filter_upwards [D.positive (actions n)] with y hy
245 exact hy _ hh
246
247 /-- Exact operator-product density with respect to the nested product reference μ^n. -/
248 noncomputable def observationDensity (actions : ℕ → A) (z : E) (n : ℕ)
249 (h : History Y n) : ℝ≥0∞ := ENNReal.ofReal (C.mass (observationRun D actions z n h))
250
251 omit [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A] [IsProbabilityMeasure μ] in
252 theorem observationDensity_measurable (actions : ℕ → A) (z : E) (n : ℕ) :
253 Measurable (observationDensity D actions z n) :=
254 ((ContinuousInstrument.massCLM C).continuous.measurable.comp
255 (observationRun_measurable D actions z n)).ennreal_ofReal
256
257 noncomputable def observationLaw (actions : ℕ → A) (z : E) (n : ℕ) :
258 Measure (History Y n) := (reference μ n).withDensity (observationDensity D actions z n)
259
260 omit [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A] in
261 theorem observationLaw_consistent (actions : ℕ → A) {z : E}
262 (hz : z∈C.carrier) (n : ℕ) :
263 (observationLaw D actions z (n+1)).fst=observationLaw D actions z n := by
264 apply density_first_marginal _ _ _ _ (observationDensity_measurable D actions z (n+1))
265 filter_upwards [observationRun_mem_ae D actions hz n] with h hh
266 exact integrated_density_mass D (actions n) hh
267
268 omit [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A] in
269 theorem observationLaw_univ (actions : ℕ → A)
270 (z : ContinuousInstrument.DensityInstrument.State C) :
271 (n : ℕ) → observationLaw D actions z.1 n Set.univ=1
272 | 0 => by simp [observationLaw,reference,observationDensity,observationRun,z.2.2]
273 | n+1 => by
274 have hm := congrArg (fun ν : Measure (History Y n) => ν Set.univ)
275 (observationLaw_consistent D actions z.2.1 n)
276 exact (Measure.fst_univ (ρ := observationLaw D actions z.1 (n+1))).symm.trans
277 (hm.trans (observationLaw_univ actions z n))
278
279 instance observationLaw_probability (actions : ℕ → A)
280 (z : ContinuousInstrument.DensityInstrument.State C) (n : ℕ) :
281 IsProbabilityMeasure (observationLaw D actions z.1 n) := ⟨observationLaw_univ D actions z n⟩
282
283 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
284 [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A] [IsProbabilityMeasure μ] in
285 theorem observationLaw_product_density (actions : ℕ → A) (z : E) (n : ℕ)
286 (S : Set (History Y n)) (hS : MeasurableSet S) :
287 observationLaw D actions z n S=
288 ∫⁻ h in S,ENNReal.ofReal (C.mass (observationRun D actions z n h))∂reference μ n :=
289 withDensity_apply _ hS
290
291
292 /-- A measurable normalized version, with an explicit valid fallback on null prefixes. -/
293 noncomputable def normalizeValue (fallback : ContinuousInstrument.DensityInstrument.State C)
294 (z : E) : E := by
295 classical
296 exact if z∈C.carrier ∧ 0<C.mass z then (C.mass z)⁻¹ • z else fallback.1
297
298 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] in
299 theorem normalizeValue_mem (fallback : ContinuousInstrument.DensityInstrument.State C) (z : E) :
300 normalizeValue fallback z∈C.base := by
301 classical
302 unfold normalizeValue
303 split_ifs with h
304 · refine ⟨C.smul_mem (inv_nonneg.mpr h.2.le) h.1,?_⟩
305 rw [map_smul,smul_eq_mul,inv_mul_cancel₀ h.2.ne']
306 · exact fallback.2
307
308 noncomputable def normalize (fallback : ContinuousInstrument.DensityInstrument.State C) (z : E) :
309 ContinuousInstrument.DensityInstrument.State C :=
310 ⟨normalizeValue fallback z,normalizeValue_mem fallback z⟩
311
312 theorem normalize_measurable (fallback : ContinuousInstrument.DensityInstrument.State C) :
313 Measurable (normalize fallback) := by
314 have hm : Measurable (fun z : E => C.mass z) := (ContinuousInstrument.massCLM C).continuous.measurable
315 have hc : MeasurableSet {z : E | z∈C.carrier ∧ 0<C.mass z} :=
316 C.closed.measurableSet.inter (measurableSet_lt measurable_const hm)
317 exact ((hm.inv.smul measurable_id).ite hc measurable_const).subtype_mk
318
319 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] in
320 /-- Zero-mass cone prefixes are zero; consequently the fallback cancels exactly. -/
321 theorem mass_smul_normalize (fallback : ContinuousInstrument.DensityInstrument.State C)
322 {z : E} (hz : z∈C.carrier) : C.mass z • (normalize fallback z).1=z := by
323 classical
324 by_cases hm : C.mass z=0
325 · have hz0 := (C.mass_zero_iff hz).mp hm
326 simp [hz0]
327 · have hp : 0<C.mass z := lt_of_le_of_ne (C.mass_nonneg hz) (Ne.symm hm)
328 simp [normalize,normalizeValue,hz,hp,smul_smul,hm]
329
330 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
331 [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A] [IsProbabilityMeasure μ] in
332 theorem density_normalize_factor (fallback : ContinuousInstrument.DensityInstrument.State C)
333 (a : A) (y : Y) {z : E} (hz : z∈C.carrier) :
334 C.mass z * D.density a y (normalize fallback z).1=D.density a y z := by
335 change C.mass z * C.mass (D.op a y (normalize fallback z).1)=C.mass (D.op a y z)
336 rw [← smul_eq_mul,← map_smul,← map_smul,mass_smul_normalize fallback hz]
337
338
339 /-- The conditional action/observation density from the actual normalized prefix. -/
340 noncomputable def nextDensity (π : Policy (A := A) (Y := Y))
341 (fallback : ContinuousInstrument.DensityInstrument.State C) (z : E) (n : ℕ)
342 (h : History (A × Y) n) (r : A × Y) : ℝ≥0∞ :=
343 π.probability n h r.1 * ENNReal.ofReal
344 (D.density r.1 r.2 (normalize fallback (run D z n h)).1)
345
346 omit [IsProbabilityMeasure μ] in
347 theorem nextDensity_measurable (π : Policy (A := A) (Y := Y))
348 (fallback : ContinuousInstrument.DensityInstrument.State C) (z : E) (n : ℕ) :
349 Measurable (Function.uncurry (nextDensity D π fallback z n)) := by
350 have hp : Measurable (fun p : History (A × Y) n × A => π.probability n p.1 p.2) :=
351 measurable_from_prod_countable_left (π.measurable_probability n)
352 have hd : Measurable (fun p : A × (ContinuousInstrument.DensityInstrument.State C × Y) =>
353 ENNReal.ofReal (D.density p.1 p.2.2 p.2.1.1)) :=
354 measurable_from_prod_countable_right D.kernel_density_measurable
355 exact (hp.comp (measurable_fst.prodMk (measurable_fst.comp measurable_snd))).mul
356 (hd.comp ((measurable_fst.comp measurable_snd).prodMk
357 (((normalize_measurable fallback).comp ((run_measurable D z n).comp measurable_fst)).prodMk
358 (measurable_snd.comp measurable_snd))))
359
360 theorem nextDensity_integral (π : Policy (A := A) (Y := Y))
361 (fallback : ContinuousInstrument.DensityInstrument.State C) (z : E) (n : ℕ)
362 (h : History (A × Y) n) :
363 (∫⁻ r,nextDensity D π fallback z n h r∂stepReference (A := A) μ)=1 := by
364 have hm : Measurable (nextDensity D π fallback z n h) :=
365 (nextDensity_measurable D π fallback z n).comp (measurable_const.prodMk measurable_id)
366 rw [stepReference,lintegral_prod _ hm.aemeasurable]
367 have hi (a : A) : (∫⁻ y,nextDensity D π fallback z n h (a,y)∂μ)=π.probability n h a := by
368 have hd : Measurable (fun y : Y => ENNReal.ofReal
369 (D.density a y (normalize fallback (run D z n h)).1)) :=
370 (D.kernel_density_measurable a).comp (measurable_const.prodMk measurable_id)
371 change (∫⁻ y,π.probability n h a * ENNReal.ofReal
372 (D.density a y (normalize fallback (run D z n h)).1)∂μ)=_
373 rw [lintegral_const_mul _ hd,integrated_density_mass D a
374 (normalize fallback (run D z n h)).2.1,(normalize fallback (run D z n h)).2.2,
375 ENNReal.ofReal_one,mul_one]
376 simp_rw [hi,lintegral_count,tsum_fintype]
377 exact π.sum_one n h
378
379 noncomputable def nextKernel (π : Policy (A := A) (Y := Y))
380 (fallback : ContinuousInstrument.DensityInstrument.State C) (z : E) (n : ℕ) :
381 Kernel (History (A × Y) n) (A × Y) :=
382 (Kernel.const _ (stepReference (A := A) μ)).withDensity (nextDensity D π fallback z n)
383
384 instance nextKernel_markov (π : Policy (A := A) (Y := Y))
385 (fallback : ContinuousInstrument.DensityInstrument.State C) (z : E) (n : ℕ) :
386 IsMarkovKernel (nextKernel D π fallback z n) := by
387 constructor
388 intro h
389 constructor
390 rw [nextKernel,Kernel.withDensity_apply _ (nextDensity_measurable D π fallback z n),
391 Kernel.const_apply,withDensity_apply _ MeasurableSet.univ,Measure.restrict_univ,
392 nextDensity_integral D π fallback z n h]
393
394 /-- The product-density law is generated one step at a time by the probability
395 instrument kernel and the randomized policy. Null-prefix fallback choices cancel. -/
396 theorem recordLaw_compProd (π : Policy (A := A) (Y := Y))
397 (fallback : ContinuousInstrument.DensityInstrument.State C) {z : E}
398 (hz : z∈C.carrier) (n : ℕ) :
399 recordLaw D π z (n+1)=recordLaw D π z n ⊗ₘ nextKernel D π fallback z n := by
400 have : IsMarkovKernel ((Kernel.const (History (A × Y) n) (stepReference (A := A) μ)).withDensity
401 (nextDensity D π fallback z n)) := nextKernel_markov D π fallback z n
402 rw [recordLaw,recordLaw,nextKernel,Measure.withDensity_compProd_withDensity
403 (recordDensity_measurable D π z n) (nextDensity_measurable D π fallback z n),
404 Measure.compProd_const]
405 apply withDensity_congr_ae
406 apply (Measure.ae_prod_iff_ae_ae (measurableSet_eq_fun
407 (recordDensity_measurable D π z (n+1))
408 (((recordDensity_measurable D π z n).comp measurable_fst).mul
409 (nextDensity_measurable D π fallback z n)))).mpr
410 filter_upwards [run_mem_ae D hz n] with h hh
411 apply Filter.Eventually.of_forall
412 intro r
413 change π.weight n h * π.probability n h r.1 *
414 ENNReal.ofReal (D.density r.1 r.2 (run D z n h))=
415 (π.weight n h * ENNReal.ofReal (C.mass (run D z n h))) *
416 (π.probability n h r.1 * ENNReal.ofReal
417 (D.density r.1 r.2 (normalize fallback (run D z n h)).1))
418 rw [← density_normalize_factor D fallback r.1 r.2 hh,ENNReal.ofReal_mul (C.mass_nonneg hh)]
419 ac_rfl
420
421
422 /-- Consistency holds for every earlier finite horizon. -/
423 theorem recordLaw_prefix (π : Policy (A := A) (Y := Y)) {z : E}
424 (hz : z∈C.carrier) (n : ℕ) : (k : ℕ) →
425 (recordLaw D π z (n+k)).map (truncate n k)=recordLaw D π z n
426 | 0 => by simp [truncate]
427 | k+1 => by
428 change (recordLaw D π z (n+k+1)).map ((truncate n k) ∘ Prod.fst)=_
429 exact (Measure.map_map (μ := recordLaw D π z (n+k+1))
430 (truncate_measurable (X := A × Y) n k) measurable_fst).symm.trans
431 ((congrArg (fun ν : Measure (History (A × Y) (n+k)) => ν.map (truncate n k))
432 (recordLaw_consistent D π hz (n+k))).trans (recordLaw_prefix π hz n k))
433
434 omit [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A] in
435 theorem observationLaw_prefix (actions : ℕ → A) {z : E}
436 (hz : z∈C.carrier) (n : ℕ) : (k : ℕ) →
437 (observationLaw D actions z (n+k)).map (truncate n k)=observationLaw D actions z n
438 | 0 => by simp [truncate]
439 | k+1 => by
440 change (observationLaw D actions z (n+k+1)).map ((truncate n k) ∘ Prod.fst)=_
441 exact (Measure.map_map (μ := observationLaw D actions z (n+k+1))
442 (truncate_measurable (X := Y) n k) measurable_fst).symm.trans
443 ((congrArg (fun ν : Measure (History Y (n+k)) => ν.map (truncate n k))
444 (observationLaw_consistent D actions hz (n+k))).trans (observationLaw_prefix actions hz n k))
445
446
447 /-- The conditional law chooses the policy action and then uses the actual
448 ContinuousInstrument kernel at the normalized prefix state. -/
449 theorem nextKernel_action_event (π : Policy (A := A) (Y := Y))
450 (fallback : ContinuousInstrument.DensityInstrument.State C) (z : E) (n : ℕ)
451 (h : History (A × Y) n) (a : A) (S : Set Y) (hS : MeasurableSet S) :
452 nextKernel D π fallback z n h ({a} ×ˢ S)=
453 π.probability n h a * D.kernel a (normalize fallback (run D z n h)) S := by
454 have hm : Measurable (nextDensity D π fallback z n h) :=
455 (nextDensity_measurable D π fallback z n).comp (measurable_const.prodMk measurable_id)
456 rw [nextKernel,Kernel.withDensity_apply _ (nextDensity_measurable D π fallback z n),
457 Kernel.const_apply,withDensity_apply _ ((measurableSet_singleton a).prod hS),
458 stepReference,setLIntegral_prod _ hm.aemeasurable,lintegral_singleton,
459 Measure.count_singleton,mul_one]
460 change (∫⁻ y in S,π.probability n h a * ENNReal.ofReal
461 (D.density a y (normalize fallback (run D z n h)).1)∂μ)=_
462 have hd : Measurable (fun y : Y => ENNReal.ofReal
463 (D.density a y (normalize fallback (run D z n h)).1)) :=
464 (D.kernel_density_measurable a).comp (measurable_const.prodMk measurable_id)
465 rw [lintegral_const_mul _ hd,D.kernel_apply,withDensity_apply _ hS]
466
467
468 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] in
469 theorem normalize_smul_pos (fallback : ContinuousInstrument.DensityInstrument.State C)
470 {z : E} (hz : z∈C.carrier) {c : ℝ} (hc : 0<c) :
471 normalize fallback (c • z)=normalize fallback z := by
472 classical
473 by_cases hm : C.mass z=0
474 · have hz0 := (C.mass_zero_iff hz).mp hm
475 simp [hz0]
476 · have hp : 0<C.mass z := lt_of_le_of_ne (C.mass_nonneg hz) (Ne.symm hm)
477 apply Subtype.ext
478 have hcz : c • z∈C.carrier := C.smul_mem hc.le hz
479 have hcm : 0<C.mass (c • z) := by simpa only [map_smul,smul_eq_mul] using mul_pos hc hp
480 dsimp only [normalize,normalizeValue]
481 rw [ite_eq_left (show c • z∈C.carrier ∧ 0<C.mass (c • z) from ⟨hcz,hcm⟩),
482 ite_eq_left (show z∈C.carrier ∧ 0<C.mass z from ⟨hz,hp⟩),map_smul,smul_eq_mul,smul_smul]
483 congr 1
484 field_simp [hm,hc.ne']
485
486 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace A] [Fintype A]
487 [MeasurableSingletonClass A] [IsProbabilityMeasure μ] in
488 /-- The normalized product update agrees with the instrument's measurable update
489 on every positive-density branch outside its common null set. -/
490 theorem update_eq_normalize_ae (fallback : ContinuousInstrument.DensityInstrument.State C)
491 (a : A) (z : ContinuousInstrument.DensityInstrument.State C) :
492 ∀ᵐ y∂μ,0<D.density a y z.1 →
493 D.update fallback a z y=normalize fallback (D.op a y z.1) := by
494 filter_upwards [D.positive a,D.update_eq_ae fallback a z] with y hy hu
495 intro hp
496 apply Subtype.ext
497 rw [hu hp]
498 dsimp only [normalize,normalizeValue]
499 rw [ite_eq_left (show D.op a y z.1∈C.carrier ∧ 0<C.mass (D.op a y z.1) from
500 ⟨hy z.1 z.2.1,hp⟩)]
501 rfl
502
503
504 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace A]
505 [Fintype A] [MeasurableSingletonClass A] [IsProbabilityMeasure μ] in
506 theorem normalized_run_update_ae (fallback : ContinuousInstrument.DensityInstrument.State C)
507 (a : A) {z : E} (hz : z∈C.carrier) (hp : 0<C.mass z) :
508 ∀ᵐ y∂μ,0<D.density a y (normalize fallback z).1 →
509 normalize fallback (D.op a y z)=D.update fallback a (normalize fallback z) y := by
510 filter_upwards [D.positive a,update_eq_normalize_ae D fallback a (normalize fallback z)] with y hy hu
511 intro hd
512 have hs : C.mass z • D.op a y (normalize fallback z).1=D.op a y z := by
513 rw [← map_smul,mass_smul_normalize fallback hz]
514 rw [← hs,normalize_smul_pos fallback (hy _ (normalize fallback z).2.1) hp]
515 exact (hu hd).symm
516
517
518 /-- The observation-only law under an arbitrary history-dependent policy is an
519 actual pushforward of the joint action/observation record law. -/
520 noncomputable def policyObservationLaw (π : Policy (A := A) (Y := Y)) (z : E) (n : ℕ) :
521 Measure (History Y n) := (recordLaw D π z n).map (mapHistory Prod.snd n)
522
523 instance policyObservationLaw_probability (π : Policy (A := A) (Y := Y))
524 (z : ContinuousInstrument.DensityInstrument.State C) (n : ℕ) :
525 IsProbabilityMeasure (policyObservationLaw D π z.1 n) := by
526 have := recordLaw_probability D π z n
527 exact inferInstanceAs (IsProbabilityMeasure ((recordLaw D π z.1 n).map (mapHistory Prod.snd n)))
528
529 theorem policyObservationLaw_consistent (π : Policy (A := A) (Y := Y)) {z : E}
530 (hz : z∈C.carrier) (n : ℕ) :
531 (policyObservationLaw D π z (n+1)).fst=policyObservationLaw D π z n := by
532 exact (mapHistory_first_marginal measurable_snd n (recordLaw D π z (n+1))).trans
533 (congrArg (fun ν : Measure (History (A × Y) n) => ν.map (mapHistory Prod.snd n))
534 (recordLaw_consistent D π hz n))
535
536 end Komorebi.LSM.ContinuousRecords
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: e70cf7cb905531ff8ee9ea250f4dff426126685ef7ed71e08a5c0e58e66c6419