TimeRecords.lean

1 import KomorebiLSM.ContinuousRecords
2 
3 /-! Time-dependent instruments on the established continuous history and policy
4 spaces. Actual finite laws, normalization and all prefix marginals are derived. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.TimeRecords
7 open MeasureTheory ProbabilityTheory ContinuousRecords
8 open scoped ENNReal BigOperators
9 
10 section PolicyBounds
11 variable {A Y : Type*} [MeasurableSpace A] [MeasurableSpace Y] [Fintype A]
12 
13 /-- Pointwise normalization bounds each finite-action policy probability. -/
14 theorem policy_probability_le_one (π : Policy (A := A) (Y := Y))
15     (n : ℕ) (h : History (A × Y) n) (a : A) : π.probability n h a ≤ 1 := by
16   calc
17     _ ≤ ∑ b, π.probability n h b := Finset.single_le_sum (fun _ _ => by positivity) (Finset.mem_univ a)
18     _ = 1 := π.sum_one n h
19 
20 theorem policy_weight_le_one (π : Policy (A := A) (Y := Y)) :
21     (n : ℕ) → ∀ h : History (A × Y) n, π.weight n h ≤ 1
22   | 0, _ => le_rfl
23   | n+1, h => by
24     exact (mul_le_mul' (policy_weight_le_one π n h.1)
25       (policy_probability_le_one π n h.1 h.2.1)).trans_eq (one_mul 1)
26 
27 theorem policy_probability_ne_top (π : Policy (A := A) (Y := Y))
28     (n : ℕ) (h : History (A × Y) n) (a : A) : π.probability n h a ≠ ⊤ :=
29   ne_top_of_le_ne_top ENNReal.one_ne_top (policy_probability_le_one π n h a)
30 
31 theorem policy_weight_ne_top (π : Policy (A := A) (Y := Y))
32     (n : ℕ) (h : History (A × Y) n) : π.weight n h ≠ ⊤ :=
33   ne_top_of_le_ne_top ENNReal.one_ne_top (policy_weight_le_one π n h)
34 end PolicyBounds
35 
36 variable {E A Y : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
37 variable [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
38 variable [MeasurableSpace Y] [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A]
39 variable {C : BaseNorm.ProbabilityCone E} {μ : Measure Y}
40 variable (D : ℕ → ContinuousInstrument.DensityInstrument (A := A) C μ)
41 
42 /-- The genuine unnormalized operator product on a recorded action/observation history. -/
43 noncomputable def run (z : E) : (n : ℕ) → History (A × Y) n → E
44   | 0, _ => z
45   | n+1, h => (D n).op h.2.1 h.2.2 (run z n h.1)
46 
47 theorem run_measurable (z : E) : (n : ℕ) → Measurable (run D z n)
48   | 0 => measurable_const
49   | n+1 => by
50     exact (isBoundedBilinearMap_apply (𝕜 := ℝ) (E := E) (F := E)).continuous.measurable.comp
51       (((ContinuousRecords.op_measurable (D n)).comp measurable_snd).prodMk ((run_measurable z n).comp measurable_fst))
52 
53 /-- Policy factors multiply the mass of the actual operator product. -/
54 noncomputable def recordDensity (π : Policy (A := A) (Y := Y)) (z : E) (n : ℕ)
55     (h : History (A × Y) n) : ℝ≥0∞ := π.weight n h * ENNReal.ofReal (C.mass (run D z n h))
56 
57 theorem recordDensity_measurable (π : Policy (A := A) (Y := Y)) (z : E) (n : ℕ) :
58     Measurable (recordDensity D π z n) :=
59   (Policy.weight_measurable π n).mul (((ContinuousInstrument.massCLM C).continuous.measurable.comp
60     (run_measurable D z n)).ennreal_ofReal)
61 
62 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [MeasurableSingletonClass A] in
63 /-- Policy weighting is an exact real scalar representation of the actual
64 nonnegative record density, because normalized policy weights are finite. -/
65 theorem recordDensity_eq_ofReal_weightedRun (π : Policy (A := A) (Y := Y)) (z : E) (n : ℕ)
66     (h : History (A × Y) n) :
67     recordDensity D π z n h = ENNReal.ofReal (C.mass ((π.weight n h).toReal • run D z n h)) := by
68   rw [map_smul, smul_eq_mul, ENNReal.ofReal_mul ENNReal.toReal_nonneg,
69     ENNReal.ofReal_toReal (policy_weight_ne_top π n h)]
70   rfl
71 
72 /-- An actual measure on finite action/observation records. -/
73 noncomputable def recordLaw (π : Policy (A := A) (Y := Y)) (z : E) (n : ℕ) :
74     Measure (History (A × Y) n) :=
75   (reference (stepReference (A := A) μ) n).withDensity (recordDensity D π z n)
76 
77 
78 variable [IsProbabilityMeasure μ]
79 
80 theorem run_mem_ae {z : E} (hz : z∈C.carrier) : (n : ℕ) →
81     ∀ᵐ h∂reference (stepReference (A := A) μ) n,run D z n h∈C.carrier
82   | 0 => by simpa [run] using Filter.Eventually.of_forall (fun _ => hz)
83   | n+1 => by
84     apply (Measure.ae_prod_iff_ae_ae (C.closed.measurableSet.preimage (run_measurable D z (n+1)))).mpr
85     filter_upwards [run_mem_ae hz n] with h hh
86     apply (Measure.ae_prod_iff_ae_ae (C.closed.measurableSet.preimage
87       ((run_measurable D z (n+1)).comp (measurable_const.prodMk measurable_id)))).mpr
88     rw [Measure.ae_count_iff]
89     intro a
90     filter_upwards [(D n).positive a] with y hy
91     exact hy _ hh
92 
93 theorem recordDensity_integrate_last (π : Policy (A := A) (Y := Y))
94     (z : E) (n : ℕ) (h : History (A × Y) n) (hh : run D z n h∈C.carrier) :
95     (∫⁻ r,recordDensity D π z (n+1) (h,r)∂stepReference (A := A) μ)=
96       recordDensity D π z n h := by
97   have hm : Measurable (fun r : A × Y => recordDensity D π z (n+1) (h,r)) :=
98     (recordDensity_measurable D π z (n+1)).comp (measurable_const.prodMk measurable_id)
99   rw [stepReference,lintegral_prod _ hm.aemeasurable]
100   change (∫⁻ a,∫⁻ y,(π.weight n h * π.probability n h a) *
101     ENNReal.ofReal ((D n).density a y (run D z n h))∂μ∂Measure.count)=recordDensity D π z n h
102   have hi (a : A) : (∫⁻ y,(π.weight n h * π.probability n h a) *
103       ENNReal.ofReal ((D n).density a y (run D z n h))∂μ)=
104       (π.weight n h * π.probability n h a)*ENNReal.ofReal (C.mass (run D z n h)) := by
105     have hd : Measurable (fun y : Y => ENNReal.ofReal ((D n).density a y (run D z n h))) :=
106       (((D n).density_measurable a).comp (measurable_const.prodMk measurable_id)).ennreal_ofReal
107     rw [lintegral_const_mul _ hd,ContinuousRecords.integrated_density_mass (D n) a hh]
108   simp_rw [hi,lintegral_count,tsum_fintype]
109   rw [← Finset.sum_mul,← Finset.mul_sum,π.sum_one,mul_one]
110   rfl
111 
112 
113 
114 /-- Consistency is the equality of literal prefix marginals. -/
115 theorem recordLaw_consistent (π : Policy (A := A) (Y := Y)) {z : E}
116     (hz : z∈C.carrier) (n : ℕ) :
117     (recordLaw D π z (n+1)).fst=recordLaw D π z n := by
118   apply density_first_marginal _ _ _ _ (recordDensity_measurable D π z (n+1))
119   filter_upwards [run_mem_ae D hz n] with h hh
120   exact recordDensity_integrate_last D π z n h hh
121 
122 /-- Every finite record law has total probability one. -/
123 theorem recordLaw_univ (π : Policy (A := A) (Y := Y))
124     (z : ContinuousInstrument.DensityInstrument.State C) :
125     (n : ℕ) → recordLaw D π z.1 n Set.univ=1
126   | 0 => by simp [recordLaw,reference,recordDensity,Policy.weight,run,z.2.2]
127   | n+1 => by
128     have hm := congrArg (fun ν : Measure (History (A × Y) n) => ν Set.univ)
129       (recordLaw_consistent D π z.2.1 n)
130     exact (Measure.fst_univ (ρ := recordLaw D π z.1 (n+1))).symm.trans (hm.trans (recordLaw_univ π z n))
131 
132 instance recordLaw_probability (π : Policy (A := A) (Y := Y))
133     (z : ContinuousInstrument.DensityInstrument.State C) (n : ℕ) :
134     IsProbabilityMeasure (recordLaw D π z.1 n) := ⟨recordLaw_univ D π z n⟩
135 
136 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
137   [MeasurableSingletonClass A] [IsProbabilityMeasure μ] in
138 theorem recordLaw_event (π : Policy (A := A) (Y := Y)) (z : E) (n : ℕ)
139     (S : Set (History (A × Y) n)) (hS : MeasurableSet S) :
140     recordLaw D π z n S=∫⁻ h in S,recordDensity D π z n h∂reference (stepReference (A := A) μ) n :=
141   withDensity_apply _ hS
142 
143 
144 /-- Prescribed actions retain the genuine, unnormalized chronological product. -/
145 noncomputable def observationRun (actions : ℕ → A) (z : E) :
146     (n : ℕ) → History Y n → E
147   | 0, _ => z
148   | n+1,h => (D n).op (actions n) h.2 (observationRun actions z n h.1)
149 
150 omit [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A] [IsProbabilityMeasure μ] in
151 theorem observationRun_measurable (actions : ℕ → A) (z : E) :
152     (n : ℕ) → Measurable (observationRun D actions z n)
153   | 0 => measurable_const
154   | n+1 => by
155     exact (isBoundedBilinearMap_apply (𝕜 := ℝ) (E := E) (F := E)).continuous.measurable.comp
156       ((((D n).measurable_op (actions n)).comp measurable_snd).prodMk
157         ((observationRun_measurable actions z n).comp measurable_fst))
158 
159 omit [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A] in
160 theorem observationRun_mem_ae (actions : ℕ → A) {z : E} (hz : z∈C.carrier) :
161     (n : ℕ) → ∀ᵐ h∂reference μ n,observationRun D actions z n h∈C.carrier
162   | 0 => by simpa [observationRun] using Filter.Eventually.of_forall (fun _ => hz)
163   | n+1 => by
164     apply (Measure.ae_prod_iff_ae_ae (C.closed.measurableSet.preimage
165       (observationRun_measurable D actions z (n+1)))).mpr
166     filter_upwards [observationRun_mem_ae actions hz n] with h hh
167     filter_upwards [(D n).positive (actions n)] with y hy
168     exact hy _ hh
169 
170 /-- Exact operator-product density with respect to the nested product reference μ^n. -/
171 noncomputable def observationDensity (actions : ℕ → A) (z : E) (n : ℕ)
172     (h : History Y n) : ℝ≥0∞ := ENNReal.ofReal (C.mass (observationRun D actions z n h))
173 
174 omit [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A] [IsProbabilityMeasure μ] in
175 theorem observationDensity_measurable (actions : ℕ → A) (z : E) (n : ℕ) :
176     Measurable (observationDensity D actions z n) :=
177   ((ContinuousInstrument.massCLM C).continuous.measurable.comp
178     (observationRun_measurable D actions z n)).ennreal_ofReal
179 
180 noncomputable def observationLaw (actions : ℕ → A) (z : E) (n : ℕ) :
181     Measure (History Y n) := (reference μ n).withDensity (observationDensity D actions z n)
182 
183 omit [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A] in
184 theorem observationLaw_consistent (actions : ℕ → A) {z : E}
185     (hz : z∈C.carrier) (n : ℕ) :
186     (observationLaw D actions z (n+1)).fst=observationLaw D actions z n := by
187   apply density_first_marginal _ _ _ _ (observationDensity_measurable D actions z (n+1))
188   filter_upwards [observationRun_mem_ae D actions hz n] with h hh
189   exact ContinuousRecords.integrated_density_mass (D n) (actions n) hh
190 
191 omit [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A] in
192 theorem observationLaw_univ (actions : ℕ → A)
193     (z : ContinuousInstrument.DensityInstrument.State C) :
194     (n : ℕ) → observationLaw D actions z.1 n Set.univ=1
195   | 0 => by simp [observationLaw,reference,observationDensity,observationRun,z.2.2]
196   | n+1 => by
197     have hm := congrArg (fun ν : Measure (History Y n) => ν Set.univ)
198       (observationLaw_consistent D actions z.2.1 n)
199     exact (Measure.fst_univ (ρ := observationLaw D actions z.1 (n+1))).symm.trans
200       (hm.trans (observationLaw_univ actions z n))
201 
202 instance observationLaw_probability (actions : ℕ → A)
203     (z : ContinuousInstrument.DensityInstrument.State C) (n : ℕ) :
204     IsProbabilityMeasure (observationLaw D actions z.1 n) := ⟨observationLaw_univ D actions z n⟩
205 
206 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
207   [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A] [IsProbabilityMeasure μ] in
208 theorem observationLaw_product_density (actions : ℕ → A) (z : E) (n : ℕ)
209     (S : Set (History Y n)) (hS : MeasurableSet S) :
210     observationLaw D actions z n S=
211       ∫⁻ h in S,ENNReal.ofReal (C.mass (observationRun D actions z n h))∂reference μ n :=
212   withDensity_apply _ hS
213 
214 
215 /-- Consistency holds for every earlier finite horizon. -/
216 theorem recordLaw_prefix (π : Policy (A := A) (Y := Y)) {z : E}
217     (hz : z∈C.carrier) (n : ℕ) : (k : ℕ) →
218     (recordLaw D π z (n+k)).map (truncate n k)=recordLaw D π z n
219   | 0 => by simp [truncate]
220   | k+1 => by
221     change (recordLaw D π z (n+k+1)).map ((truncate n k) ∘ Prod.fst)=_
222     exact (Measure.map_map (μ := recordLaw D π z (n+k+1))
223       (truncate_measurable (X := A × Y) n k) measurable_fst).symm.trans
224       ((congrArg (fun ν : Measure (History (A × Y) (n+k)) => ν.map (truncate n k))
225         (recordLaw_consistent D π hz (n+k))).trans (recordLaw_prefix π hz n k))
226 
227 omit [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A] in
228 theorem observationLaw_prefix (actions : ℕ → A) {z : E}
229     (hz : z∈C.carrier) (n : ℕ) : (k : ℕ) →
230     (observationLaw D actions z (n+k)).map (truncate n k)=observationLaw D actions z n
231   | 0 => by simp [truncate]
232   | k+1 => by
233     change (observationLaw D actions z (n+k+1)).map ((truncate n k) ∘ Prod.fst)=_
234     exact (Measure.map_map (μ := observationLaw D actions z (n+k+1))
235       (truncate_measurable (X := Y) n k) measurable_fst).symm.trans
236       ((congrArg (fun ν : Measure (History Y (n+k)) => ν.map (truncate n k))
237         (observationLaw_consistent D actions hz (n+k))).trans (observationLaw_prefix actions hz n k))
238 
239 
240 
241 end Komorebi.LSM.TimeRecords

Back to source controls