ContinuousTV.lean

1 import KomorebiLSM.BaseNormIntegration
2 import KomorebiLSM.TimeRecords
3 import KomorebiLSM.ContinuousTVDensity
4 import KomorebiLSM.SequentialLowerCertificate
5 import Mathlib.MeasureTheory.Integral.Prod
6 import Mathlib.MeasureTheory.VectorMeasure.WithDensityVec
7 
8 /-! Continuous full-law comparison on one actual probability cone. The positive
9 base norm is the infimum over positive decompositions, and lawTV is the half
10 variation of the difference of the actual probability measures. -/
11 set_option autoImplicit false
12 namespace Komorebi.LSM.ContinuousTV
13 open MeasureTheory ProbabilityTheory
14 open scoped ENNReal BigOperators
15 variable {E A Y : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
16 variable [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace Y]
17 variable {C : BaseNorm.ProbabilityCone E} {μ : Measure Y}
18 variable (D F : ContinuousInstrument.DensityInstrument (A := A) C μ)
19 
20 omit [MeasurableSpace E] [BorelSpace E] in
21 /-- Integrated contraction follows from actual positive decompositions. -/
22 theorem integrated_contraction (a : A) (z : E) :
23     (∫ y,C.value (D.op a y z)∂μ)≤C.value z := by
24   apply C.le_value
25   intro u hu v hv hz
26   have hfi := C.integrable_value (D.applied_integrable a z)
27   have hgi := (D.density_integrable a u).add (D.density_integrable a v)
28   have hpoint : ∀ᵐ y∂μ,C.value (D.op a y z)≤D.density a y u+D.density a y v := by
29     filter_upwards [D.positive a] with y hy
30     rw [hz,map_sub]
31     exact (C.value_sub_le _ _).trans_eq (by
32       rw [C.value_on_cone (hy u hu),C.value_on_cone (hy v hv)]
33       rfl)
34   calc (∫ y,C.value (D.op a y z)∂μ)≤∫ y,D.density a y u+D.density a y v∂μ :=
35       integral_mono_ae hfi hgi hpoint
36     _ = C.mass u+C.mass v := by
37       rw [integral_add (D.density_integrable a u) (D.density_integrable a v),
38         D.integral_density a u,D.integral_density a v]
39 
40 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] in
41 /-- A bound on normalized inputs extends homogeneously to the whole cone. -/
42 theorem integrated_discrepancy (fallback : ContinuousInstrument.DensityInstrument.State C)
43     (a : A) (ε : ℝ)
44     (hε : ∀ z∈C.base,(∫ y,C.value (D.op a y z-F.op a y z)∂μ)≤ε)
45     {z : E} (hz : z∈C.carrier) :
46     (∫ y,C.value (D.op a y z-F.op a y z)∂μ)≤ε*C.mass z := by
47   have hm := C.mass_nonneg hz
48   have hs (y : Y) : D.op a y z-F.op a y z=
49       C.mass z • (D.op a y (ContinuousRecords.normalize fallback z).1-
50         F.op a y (ContinuousRecords.normalize fallback z).1) := by
51     rw [smul_sub,← map_smul,← map_smul,ContinuousRecords.mass_smul_normalize fallback hz]
52   simp_rw [hs,C.value_smul,abs_of_nonneg hm]
53   rw [integral_const_mul]
54   simpa only [mul_comm ε] using mul_le_mul_of_nonneg_left
55     (hε _ (ContinuousRecords.normalize fallback z).2) hm
56 
57 omit [MeasurableSpace E] [BorelSpace E] in
58 /-- One step separates transported state error and the declared instrument error. -/
59 theorem integrated_step_error (fallback : ContinuousInstrument.DensityInstrument.State C)
60     (a : A) (ε : ℝ)
61     (hε : ∀ z∈C.base,(∫ y,C.value (D.op a y z-F.op a y z)∂μ)≤ε)
62     (u : E) {v : E} (hv : v∈C.carrier) :
63     (∫ y,C.value (D.op a y u-F.op a y v)∂μ)≤C.value (u-v)+ε*C.mass v := by
64   have hi := C.integrable_value ((D.applied_integrable a u).sub (F.applied_integrable a v))
65   have ht := C.integrable_value (D.applied_integrable a (u-v))
66   have hd := C.integrable_value ((D.applied_integrable a v).sub (F.applied_integrable a v))
67   have hp (y : Y) : C.value (D.op a y u-F.op a y v)≤
68       C.value (D.op a y (u-v))+C.value (D.op a y v-F.op a y v) := by
69     have he : D.op a y u-F.op a y v=D.op a y (u-v)+(D.op a y v-F.op a y v) := by
70       rw [map_sub]; abel
71     rw [he]
72     exact C.value_add_le _ _
73   calc (∫ y,C.value (D.op a y u-F.op a y v)∂μ)≤
74       ∫ y,C.value (D.op a y (u-v))+C.value (D.op a y v-F.op a y v)∂μ :=
75         integral_mono_ae hi (ht.add hd) (Filter.Eventually.of_forall hp)
76     _ = (∫ y,C.value (D.op a y (u-v))∂μ)+(∫ y,C.value (D.op a y v-F.op a y v)∂μ) :=
77       integral_add ht hd
78     _ ≤ C.value (u-v)+ε*C.mass v := add_le_add (integrated_contraction D a (u-v))
79       (integrated_discrepancy D F fallback a ε hε hv)
80 
81 
82 omit [MeasurableSpace E] [BorelSpace E] in
83 theorem lintegrated_step_error (fallback : ContinuousInstrument.DensityInstrument.State C)
84     (a : A) (ε : ℝ)
85     (hε : ∀ z∈C.base,(∫ y,C.value (D.op a y z-F.op a y z)∂μ)≤ε)
86     (u : E) {v : E} (hv : v∈C.carrier) :
87     (∫⁻ y,ENNReal.ofReal (C.value (D.op a y u-F.op a y v))∂μ)≤
88       ENNReal.ofReal (C.value (u-v)+ε*C.mass v) := by
89   have hi : Integrable (fun y => C.value (D.op a y u-F.op a y v)) μ :=
90     C.integrable_value ((D.applied_integrable a u).sub (F.applied_integrable a v))
91   rw [← ofReal_integral_eq_lintegral_ofReal hi
92     (Filter.Eventually.of_forall (fun y => C.value_nonneg _))]
93   exact ENNReal.ofReal_le_ofReal (integrated_step_error D F fallback a ε hε u hv)
94 
95 section Records
96 open ContinuousRecords
97 variable [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A] [IsProbabilityMeasure μ]
98 variable (Ds Fs : ℕ → ContinuousInstrument.DensityInstrument (A := A) C μ)
99 
100 /-- Actual chronological states, multiplied by the common randomized policy weight. -/
101 noncomputable def weightedRun (π : Policy (A := A) (Y := Y)) (z : E) (n : ℕ)
102     (h : History (A × Y) n) : E := (π.weight n h).toReal • TimeRecords.run Ds z n h
103 
104 omit [IsProbabilityMeasure μ] in
105 theorem weightedRun_measurable (π : Policy (A := A) (Y := Y)) (z : E) (n : ℕ) :
106     Measurable (weightedRun Ds π z n) :=
107   (Policy.weight_measurable π n).ennreal_toReal.smul (TimeRecords.run_measurable Ds z n)
108 
109 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
110   [MeasurableSingletonClass A] [IsProbabilityMeasure μ] in
111 theorem weightedRun_succ (π : Policy (A := A) (Y := Y)) (z : E) (n : ℕ)
112     (h : History (A × Y) n) (r : A × Y) :
113     weightedRun Ds π z (n+1) (h,r)=
114       (π.probability n h r.1).toReal • (Ds n).op r.1 r.2 (weightedRun Ds π z n h) := by
115   simp only [weightedRun,Policy.weight,TimeRecords.run,ENNReal.toReal_mul,map_smul,smul_smul]
116   rw [mul_comm]
117 
118 theorem weightedRun_mem_ae (π : Policy (A := A) (Y := Y)) {z : E}
119     (hz : z∈C.carrier) (n : ℕ) :
120     ∀ᵐ h∂reference (stepReference (A := A) μ) n,weightedRun Ds π z n h∈C.carrier := by
121   filter_upwards [TimeRecords.run_mem_ae Ds hz n] with h hh
122   exact C.smul_mem ENNReal.toReal_nonneg hh
123 
124 theorem mass_lintegral (π : Policy (A := A) (Y := Y))
125     (z : ContinuousInstrument.DensityInstrument.State C) (n : ℕ) :
126     (∫⁻ h,ENNReal.ofReal (C.mass (weightedRun Ds π z.1 n h))∂
127       reference (stepReference (A := A) μ) n)=1 := by
128   have hm := TimeRecords.recordLaw_univ Ds π z n
129   rw [TimeRecords.recordLaw,withDensity_apply _ MeasurableSet.univ,Measure.restrict_univ] at hm
130   simpa only [TimeRecords.recordDensity_eq_ofReal_weightedRun,weightedRun] using hm
131 
132 
133 /-- Integration over both the randomized action and the next continuous record. -/
134 theorem policy_step_lintegral_error (fallback : ContinuousInstrument.DensityInstrument.State C)
135     (π : Policy (A := A) (Y := Y)) (n : ℕ) (h : History (A × Y) n) (ε : ℝ)
136     (hε : ∀ a z,z∈C.base → (∫ y,C.value (D.op a y z-F.op a y z)∂μ)≤ε)
137     (u : E) {v : E} (hv : v∈C.carrier) :
138     (∫⁻ r,ENNReal.ofReal (C.value ((π.probability n h r.1).toReal •
139       (D.op r.1 r.2 u-F.op r.1 r.2 v)))∂stepReference (A := A) μ)≤
140       ENNReal.ofReal (C.value (u-v)+ε*C.mass v) := by
141   have hd (a : A) : Measurable (fun y : Y => C.value (D.op a y u-F.op a y v)) := by
142     exact C.value_continuous.measurable.comp
143       (((ContinuousLinearMap.apply ℝ E u).continuous.measurable.comp (D.measurable_op a)).sub
144         ((ContinuousLinearMap.apply ℝ E v).continuous.measurable.comp (F.measurable_op a)))
145   have hm : Measurable (fun r : A × Y => ENNReal.ofReal (C.value
146       ((π.probability n h r.1).toReal • (D.op r.1 r.2 u-F.op r.1 r.2 v)))) := by
147     apply measurable_from_prod_countable_right
148     intro a
149     simpa only [C.value_smul,abs_of_nonneg ENNReal.toReal_nonneg,Pi.mul_apply] using
150       (measurable_const.mul (hd a)).ennreal_ofReal
151   rw [stepReference,lintegral_prod _ hm.aemeasurable,lintegral_count,tsum_fintype]
152   have hi (a : A) : (∫⁻ y,ENNReal.ofReal (C.value ((π.probability n h a).toReal •
153       (D.op a y u-F.op a y v)))∂μ)≤
154       π.probability n h a * ENNReal.ofReal (C.value (u-v)+ε*C.mass v) := by
155     simp_rw [C.value_smul,abs_of_nonneg ENNReal.toReal_nonneg,
156       ENNReal.ofReal_mul ENNReal.toReal_nonneg]
157     rw [lintegral_const_mul _ (hd a).ennreal_ofReal,
158       ENNReal.ofReal_toReal (TimeRecords.policy_probability_ne_top π n h a)]
159     exact mul_le_mul' le_rfl (lintegrated_step_error D F fallback a ε (hε a) u hv)
160   calc (∑ a,∫⁻ y,ENNReal.ofReal (C.value ((π.probability n h a).toReal •
161       (D.op a y u-F.op a y v)))∂μ)≤
162       ∑ a,π.probability n h a * ENNReal.ofReal (C.value (u-v)+ε*C.mass v) :=
163         Finset.sum_le_sum (fun a _ => hi a)
164     _ = ENNReal.ofReal (C.value (u-v)+ε*C.mass v) := by
165       rw [← Finset.sum_mul,π.sum_one,one_mul]
166 
167 
168 /-- Integrated signed state error on the genuine continuous product reference. -/
169 noncomputable def stateError (π : Policy (A := A) (Y := Y)) (u v : E) (n : ℕ) : ℝ≥0∞ :=
170   ∫⁻ h,ENNReal.ofReal (C.value (weightedRun Ds π u n h-weightedRun Fs π v n h))∂
171     reference (stepReference (A := A) μ) n
172 
173 omit [IsProbabilityMeasure μ] in
174 theorem error_integrand_measurable (π : Policy (A := A) (Y := Y)) (u v : E) (n : ℕ) :
175     Measurable (fun h => ENNReal.ofReal (C.value
176       (weightedRun Ds π u n h-weightedRun Fs π v n h))) :=
177   (C.value_continuous.measurable.comp
178     ((weightedRun_measurable Ds π u n).sub (weightedRun_measurable Fs π v n))).ennreal_ofReal
179 
180 /-- The common policy preserves the one-step integrated error recurrence. -/
181 theorem stateError_step (fallback : ContinuousInstrument.DensityInstrument.State C)
182     (π : Policy (A := A) (Y := Y)) (u : E)
183     (v : ContinuousInstrument.DensityInstrument.State C) (n : ℕ) (ε : ℝ) (hε0 : 0≤ε)
184     (hε : ∀ a z,z∈C.base → (∫ y,C.value ((Ds n).op a y z-(Fs n).op a y z)∂μ)≤ε) :
185     stateError Ds Fs π u v.1 (n+1)≤stateError Ds Fs π u v.1 n+ENNReal.ofReal ε := by
186   change (∫⁻ p : History (A × Y) n × (A × Y),ENNReal.ofReal (C.value
187     (weightedRun Ds π u (n+1) p-weightedRun Fs π v.1 (n+1) p))∂
188       (reference (stepReference (A := A) μ) n).prod (stepReference (A := A) μ))≤_
189   have hmprod : Measurable (fun p : History (A × Y) n × (A × Y) => ENNReal.ofReal (C.value
190       (weightedRun Ds π u (n+1) p-weightedRun Fs π v.1 (n+1) p))) :=
191     error_integrand_measurable Ds Fs π u v.1 (n+1)
192   rw [lintegral_prod _ hmprod.aemeasurable]
193   calc
194     (∫⁻ h,∫⁻ r,ENNReal.ofReal (C.value
195       (weightedRun Ds π u (n+1) (h,r)-weightedRun Fs π v.1 (n+1) (h,r)))∂
196       stepReference (A := A) μ∂reference (stepReference (A := A) μ) n)≤
197       ∫⁻ h,ENNReal.ofReal (C.value (weightedRun Ds π u n h-weightedRun Fs π v.1 n h)+
198         ε*C.mass (weightedRun Fs π v.1 n h))∂reference (stepReference (A := A) μ) n := by
199       apply lintegral_mono_ae
200       filter_upwards [weightedRun_mem_ae Fs π v.2.1 n] with h hh
201       simpa only [weightedRun_succ,← smul_sub] using
202         policy_step_lintegral_error (Ds n) (Fs n) fallback π n h ε hε
203           (weightedRun Ds π u n h) hh
204     _ = stateError Ds Fs π u v.1 n+ENNReal.ofReal ε := by
205       have he : (fun h => ENNReal.ofReal (C.value
206           (weightedRun Ds π u n h-weightedRun Fs π v.1 n h)+ε*C.mass (weightedRun Fs π v.1 n h)))
207           =ᵐ[reference (stepReference (A := A) μ) n]
208           (fun h => ENNReal.ofReal (C.value (weightedRun Ds π u n h-weightedRun Fs π v.1 n h))+
209             ENNReal.ofReal ε * ENNReal.ofReal (C.mass (weightedRun Fs π v.1 n h))) := by
210         filter_upwards [weightedRun_mem_ae Fs π v.2.1 n] with h hh
211         rw [ENNReal.ofReal_add (C.value_nonneg _) (mul_nonneg hε0 (C.mass_nonneg hh)),
212           ENNReal.ofReal_mul hε0]
213       have hm : Measurable (fun h => ENNReal.ofReal (C.mass (weightedRun Fs π v.1 n h))) :=
214         ((ContinuousInstrument.massCLM C).continuous.measurable.comp
215           (weightedRun_measurable Fs π v.1 n)).ennreal_ofReal
216       rw [lintegral_congr_ae he,lintegral_add_left (error_integrand_measurable Ds Fs π u v.1 n),
217         lintegral_const_mul _ hm,mass_lintegral Fs π v n,mul_one]
218       rfl
219 
220 /-- Iterating the recurrence requires no branch-density lower margin. -/
221 theorem stateError_le (π : Policy (A := A) (Y := Y))
222     (u v : ContinuousInstrument.DensityInstrument.State C) (ε : ℕ → ℝ)
223     (hε0 : ∀ n,0≤ε n)
224     (hε : ∀ n a z,z∈C.base → (∫ y,C.value ((Ds n).op a y z-(Fs n).op a y z)∂μ)≤ε n) :
225     ∀ n,stateError Ds Fs π u.1 v.1 n≤ENNReal.ofReal (C.value (u.1-v.1)+∑ i∈Finset.range n,ε i) := by
226   intro n
227   induction n with
228   | zero => simp [stateError,reference,weightedRun,Policy.weight,TimeRecords.run]
229   | succ n ih =>
230     calc stateError Ds Fs π u.1 v.1 (n+1)≤stateError Ds Fs π u.1 v.1 n+ENNReal.ofReal (ε n) :=
231         stateError_step Ds Fs v π u.1 v n (ε n) (hε0 n) (hε n)
232       _ ≤ ENNReal.ofReal (C.value (u.1-v.1)+∑ i∈Finset.range n,ε i)+ENNReal.ofReal (ε n) :=
233         add_le_add ih le_rfl
234       _ = ENNReal.ofReal (C.value (u.1-v.1)+∑ i∈Finset.range (n+1),ε i) := by
235         rw [Finset.sum_range_succ,← ENNReal.ofReal_add
236           (add_nonneg (C.value_nonneg _) (Finset.sum_nonneg (fun i _ => hε0 i))) (hε0 n)]
237         congr 1
238         ring
239 
240 
241 /-- Reading mass from the two actual positive states cannot increase their
242 base-norm error. This compares the literal record-measure densities. -/
243 theorem density_lintegral_le_stateError (π : Policy (A := A) (Y := Y))
244     (u v : ContinuousInstrument.DensityInstrument.State C) (n : ℕ) :
245     (∫⁻ h,ENNReal.ofReal |(TimeRecords.recordDensity Ds π u.1 n h).toReal-
246       (TimeRecords.recordDensity Fs π v.1 n h).toReal|∂reference (stepReference (A := A) μ) n)≤
247       stateError Ds Fs π u.1 v.1 n := by
248   apply lintegral_mono_ae
249   filter_upwards [weightedRun_mem_ae Ds π u.2.1 n,weightedRun_mem_ae Fs π v.2.1 n] with h hu hv
250   simp only [TimeRecords.recordDensity_eq_ofReal_weightedRun]
251   change ENNReal.ofReal |(ENNReal.ofReal (C.mass (weightedRun Ds π u.1 n h))).toReal-
252     (ENNReal.ofReal (C.mass (weightedRun Fs π v.1 n h))).toReal|≤_
253   rw [ENNReal.toReal_ofReal (C.mass_nonneg hu),ENNReal.toReal_ofReal (C.mass_nonneg hv)]
254   apply ENNReal.ofReal_le_ofReal
255   simpa only [map_sub] using C.abs_mass_le (weightedRun Ds π u.1 n h-weightedRun Fs π v.1 n h)
256 
257 
258 /-- The full time-dependent record-measure bound under one arbitrary common
259 measurable randomized policy. All instruments use the same actual cone and reference. -/
260 theorem record_lawTV_le (π : Policy (A := A) (Y := Y))
261     (u v : ContinuousInstrument.DensityInstrument.State C) (ε : ℕ → ℝ)
262     (hε0 : ∀ n,0≤ε n)
263     (hε : ∀ n a z,z∈C.base → (∫ y,C.value ((Ds n).op a y z-(Fs n).op a y z)∂μ)≤ε n)
264     (e0 : ℝ) (he0 : C.value (u.1-v.1)≤e0) (n : ℕ) :
265     SequentialLowerCertificate.lawTV (TimeRecords.recordLaw Ds π u.1 n)
266       (TimeRecords.recordLaw Fs π v.1 n)≤min 1 ((e0+∑ i∈Finset.range n,ε i)/2) := by
267   have he00 : 0≤e0 := (C.value_nonneg _).trans he0
268   have hB0 : 0≤e0+∑ i∈Finset.range n,ε i :=
269     add_nonneg he00 (Finset.sum_nonneg (fun i _ => hε0 i))
270   have hs : stateError Ds Fs π u.1 v.1 n≤ENNReal.ofReal (e0+∑ i∈Finset.range n,ε i) :=
271     (stateError_le Ds Fs π u v ε hε0 hε n).trans
272       (ENNReal.ofReal_le_ofReal (add_le_add he0 le_rfl))
273   have hp : IsProbabilityMeasure ((reference (stepReference (A := A) μ) n).withDensity
274       (TimeRecords.recordDensity Ds π u.1 n)) := TimeRecords.recordLaw_probability Ds π u n
275   have hq : IsProbabilityMeasure ((reference (stepReference (A := A) μ) n).withDensity
276       (TimeRecords.recordDensity Fs π v.1 n)) := TimeRecords.recordLaw_probability Fs π v n
277   have hn : ENNReal.ofReal (SequentialLowerCertificate.lawTV (TimeRecords.recordLaw Ds π u.1 n)
278       (TimeRecords.recordLaw Fs π v.1 n))≤ENNReal.ofReal ((e0+∑ i∈Finset.range n,ε i)/2) := by
279     change ENNReal.ofReal (SequentialLowerCertificate.lawTV
280       ((reference (stepReference (A := A) μ) n).withDensity (TimeRecords.recordDensity Ds π u.1 n))
281       ((reference (stepReference (A := A) μ) n).withDensity (TimeRecords.recordDensity Fs π v.1 n)))≤_
282     rw [ContinuousTVDensity.ofReal_lawTV_withDensity_lintegral _ _ _
283       (TimeRecords.recordDensity_measurable Ds π u.1 n).aemeasurable
284       (TimeRecords.recordDensity_measurable Fs π v.1 n).aemeasurable]
285     calc (1/2:ℝ≥0∞) * (∫⁻ h,ENNReal.ofReal
286         |(TimeRecords.recordDensity Ds π u.1 n h).toReal-(TimeRecords.recordDensity Fs π v.1 n h).toReal|∂
287           reference (stepReference (A := A) μ) n)≤
288         (1/2:ℝ≥0∞)*ENNReal.ofReal (e0+∑ i∈Finset.range n,ε i) :=
289           mul_le_mul' le_rfl ((density_lintegral_le_stateError Ds Fs π u v n).trans hs)
290       _ = ENNReal.ofReal ((e0+∑ i∈Finset.range n,ε i)/2) := by
291         rw [show (1/2:ℝ≥0∞)=ENNReal.ofReal (1/2:ℝ) by
292           rw [ENNReal.ofReal_div_of_pos (by norm_num : (0:ℝ)<2)]
293           norm_num,← ENNReal.ofReal_mul (by norm_num : (0:ℝ)≤1/2)]
294         congr 1
295         ring
296   have ht := ENNReal.toReal_mono ENNReal.ofReal_ne_top hn
297   have hreal : SequentialLowerCertificate.lawTV (TimeRecords.recordLaw Ds π u.1 n)
298       (TimeRecords.recordLaw Fs π v.1 n)≤(e0+∑ i∈Finset.range n,ε i)/2 := by
299     have hhalf0 : 0≤(e0+∑ i∈Finset.range n,ε i)/2 := div_nonneg hB0 (by norm_num)
300     simpa only [ENNReal.toReal_ofReal (SequentialLowerCertificate.lawTV_nonneg _ _),
301       ENNReal.toReal_ofReal hhalf0] using ht
302   exact le_min (SequentialLowerCertificate.lawTV_le_one _ _) hreal
303 
304 end Records
305 end Komorebi.LSM.ContinuousTV

Back to source controls