ObservableMomentConditional.lean

1 import KomorebiLSM.ContinuousInstrument
2 import KomorebiLSM.BaseNormTopology
3 import Mathlib.Probability.Kernel.Composition.IntegralCompProd
4 import Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
5 import Mathlib.Tactic
6 
7 /-! P82: conditional moments from literal observation kernels and accessible
8 normalized posterior states. No conditional-mean identity is an input field. -/
9 set_option autoImplicit false
10 namespace Komorebi.LSM.ObservableMoments
11 open MeasureTheory ProbabilityTheory
12 open scoped ENNReal BigOperators
13 
14 section HistoryConditional
15 variable {Ω H Y E : Type*} [mΩ : MeasurableSpace Ω] [mH : MeasurableSpace H]
16 variable [MeasurableSpace Y] [NormedAddCommGroup E] [NormedSpace ℝ E]
17 variable [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
18 variable {μ : Measure Ω} [IsProbabilityMeasure μ]
19 
20 /-- Equality of the actual joint history/observation measure identifies the
21 conditional integral relative to exactly the recorded history sigma algebra. -/
22 theorem history_condExp (history : Ω → H) (observation : Ω → Y)
23     (hh : Measurable history) (hy : Measurable observation)
24     (κ : Kernel H Y) [IsMarkovKernel κ]
25     (hlaw : μ.map (fun ω => (history ω,observation ω))=(μ.map history) ⊗ₘ κ)
26     (F : H × Y → E) (hF : Measurable F)
27     (hFi : Integrable (fun ω => F (history ω,observation ω)) μ) :
28     μ[fun ω => F (history ω,observation ω) | mH.comap history] =ᵐ[μ]
29       (fun ω => ∫ y,F (history ω,y)∂κ (history ω)) := by
30   have hj := hh.prodMk hy
31   have hiMap : Integrable F (μ.map (fun ω => (history ω,observation ω))) :=
32     (integrable_map_measure hF.stronglyMeasurable.aestronglyMeasurable hj.aemeasurable).mpr hFi
33   have hi : Integrable F ((μ.map history) ⊗ₘ κ) := by rwa [hlaw] at hiMap
34   have hparts := (Measure.integrable_compProd_iff hi.aestronglyMeasurable).mp hi
35   have hg : Measurable (fun h => ∫ y,F (h,y)∂κ h) :=
36     hF.stronglyMeasurable.integral_kernel_prod_right'.measurable
37   have hgi : Integrable (fun h => ∫ y,F (h,y)∂κ h) (μ.map history) := by
38     apply hparts.2.mono' hg.aestronglyMeasurable
39     exact Filter.Eventually.of_forall (fun h => norm_integral_le_integral_norm _)
40   have hgc : @Measurable Ω E (mH.comap history) _
41       (fun ω => ∫ y,F (history ω,y)∂κ (history ω)) := hg.comp (comap_measurable history)
42   apply (ae_eq_condExp_of_forall_setIntegral_eq hh.comap_le hFi
43     (fun _ _ _ => (hgi.comp_measurable hh).integrableOn) ?_
44     hgc.stronglyMeasurable.aestronglyMeasurable).symm
45   intro s hs _
46   obtain ⟨S,hS,rfl⟩ := MeasurableSpace.measurableSet_comap.mp hs
47   calc
48     (∫ ω in history ⁻¹' S,(∫ y,F (history ω,y)∂κ (history ω))∂μ)=
49       ∫ h in S,(∫ y,F (h,y)∂κ h)∂μ.map history :=
50         (setIntegral_map hS hg.aestronglyMeasurable hh.aemeasurable).symm
51     _ = ∫ p in S ×ˢ Set.univ,F p∂(μ.map history) ⊗ₘ κ := by
52       rw [Measure.setIntegral_compProd hS MeasurableSet.univ hi.integrableOn]
53       simp only [Measure.restrict_univ]
54     _ = ∫ ω in history ⁻¹' S,F (history ω,observation ω)∂μ := by
55       rw [← hlaw,setIntegral_map (hS.prod MeasurableSet.univ)
56         hF.stronglyMeasurable.aestronglyMeasurable hj.aemeasurable]
57       have hp : (fun ω => (history ω,observation ω)) ⁻¹' (S ×ˢ Set.univ)=history ⁻¹' S := by
58         ext ω
59         simp
60       rw [hp]
61 
62 end HistoryConditional
63 
64 section Instrument
65 variable {E A Y : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
66 variable [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
67 variable [MeasurableSpace Y] {C : BaseNorm.ProbabilityCone E} {ν : Measure Y}
68 variable [IsProbabilityMeasure ν]
69 variable (D : ContinuousInstrument.DensityInstrument (A := A) C ν)
70 open ContinuousInstrument.DensityInstrument
71 
72 /-- The literal weighted integral of the submitted operator density. -/
73 noncomputable def momentOperator (g : Y → ℝ) (a : A) : E →L[ℝ] E :=
74   ∫ y,g y • D.op a y∂ν
75 
76 /-- The observation density cancels the actual normalized posterior,
77 including zero-density branches through their zero measure contribution. -/
78 theorem kernel_weighted_posterior (fallback : State C) (a : A) (z : State C)
79     (g : Y → ℝ)
80     (hgi : Integrable (fun y => g y • D.op a y) ν) :
81     (∫ y,g y • (D.update fallback a z y).1∂D.kernel a z)=momentOperator D g a z.1 := by
82   have hd : Measurable (fun y => ENNReal.ofReal (D.density a y z.1)) :=
83     (((D.density_measurable a).comp (measurable_const.prodMk measurable_id)).ennreal_ofReal)
84   rw [D.kernel_apply,integral_withDensity_eq_integral_toReal_smul hd
85     (Filter.Eventually.of_forall (fun _ => ENNReal.ofReal_lt_top))]
86   rw [momentOperator,ContinuousLinearMap.integral_apply hgi]
87   apply integral_congr_ae
88   filter_upwards [D.density_smul_update_ae fallback a z,D.density_nonneg_ae a z.2.1] with y he hn
89   rw [ENNReal.toReal_ofReal hn,smul_smul,mul_comm,← smul_smul,he]
90   rfl
91 
92 variable [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A]
93 
94 /-- The literal instrument kernel with its observed chosen action included. -/
95 noncomputable def controlledKernel : Kernel (A × State C) Y where
96   toFun p := D.kernel p.1 p.2
97   measurable' := measurable_from_prod_countable_right (fun a => (D.kernel a).measurable)
98 
99 instance controlledKernel_markov : IsMarkovKernel (controlledKernel D) := by
100   constructor
101   intro p
102   change IsProbabilityMeasure (D.kernel p.1 p.2)
103   infer_instance
104 
105 omit [IsProbabilityMeasure ν] in
106 theorem controlled_update_measurable (fallback : State C) :
107     Measurable (fun p : A × (State C × Y) => (D.update fallback p.1 p.2.1 p.2.2).1) := by
108   apply measurable_from_prod_countable_right
109   intro a
110   exact measurable_subtype_coe.comp (D.update_measurable fallback a)
111 
112 variable {H : Type*} [MeasurableSpace H]
113 
114 /-- Every state in this experiment is a specified measurable function of the
115 recorded context. The next state is also accessible from that context and the
116 new observation. Its positive-density branch formula is a separate assumption. -/
117 structure AccessibleState where
118   action : H → A
119   state : H → State C
120   next : H × Y → State C
121   action_measurable : Measurable action
122   state_measurable : Measurable state
123   next_measurable : Measurable next
124   posterior : ∀ h,∀ᵐ y∂ν,0<D.density (action h) y (state h).1 →
125     (next (h,y)).1=(D.density (action h) y (state h).1)⁻¹ • D.op (action h) y (state h).1
126 
127 variable (X : AccessibleState (H := H) D)
128 
129 /-- The actual chosen-action observation kernel along the accessible state. -/
130 noncomputable def historyKernel : Kernel H Y :=
131   (controlledKernel D).comap (fun h => (X.action h,X.state h))
132     (X.action_measurable.prodMk X.state_measurable)
133 
134 instance historyKernel_markov : IsMarkovKernel (historyKernel D X) := by
135   unfold historyKernel
136   infer_instance
137 
138 omit [FiniteDimensional ℝ E] [BorelSpace E] [IsProbabilityMeasure ν] [Fintype A]
139   [MeasurableSingletonClass A] in
140 /-- The normalized posterior cancels on positive branches. At zero mass the
141 true positive branch is zero, so the identity extends almost everywhere. -/
142 theorem density_smul_accessible (h : H) :
143     ∀ᵐ y∂ν,D.density (X.action h) y (X.state h).1 • (X.next (h,y)).1=
144       D.op (X.action h) y (X.state h).1 := by
145   filter_upwards [X.posterior h,D.positive (X.action h)] with y hp hy
146   have hcone := hy _ (X.state h).2.1
147   have hn : 0≤D.density (X.action h) y (X.state h).1 := C.mass_nonneg hcone
148   by_cases hpos : 0<D.density (X.action h) y (X.state h).1
149   · rw [hp hpos,smul_smul,mul_inv_cancel₀ hpos.ne',one_smul]
150   · have hz : D.density (X.action h) y (X.state h).1=0 := le_antisymm (le_of_not_gt hpos) hn
151     have ho : D.op (X.action h) y (X.state h).1=0 := (C.mass_zero_iff hcone).mp hz
152     rw [hz,zero_smul,ho]
153 
154 /-- Literal integration of the accessible response gives the unnormalized
155 operator moment; no observation density remains in the denominator. -/
156 theorem kernel_weighted_accessible (g : Y → ℝ)
157     (hgi : ∀ a,Integrable (fun y => g y • D.op a y) ν) (h : H) :
158     (∫ y,g y • (X.next (h,y)).1∂historyKernel D X h)=
159       momentOperator D g (X.action h) (X.state h).1 := by
160   change (∫ y,g y • (X.next (h,y)).1∂D.kernel (X.action h) (X.state h))=_
161   have hd : Measurable (fun y => ENNReal.ofReal (D.density (X.action h) y (X.state h).1)) :=
162     (((D.density_measurable (X.action h)).comp
163       (measurable_const.prodMk measurable_id)).ennreal_ofReal)
164   rw [D.kernel_apply,integral_withDensity_eq_integral_toReal_smul hd
165     (Filter.Eventually.of_forall (fun _ => ENNReal.ofReal_lt_top)),momentOperator,
166     ContinuousLinearMap.integral_apply (hgi (X.action h))]
167   apply integral_congr_ae
168   filter_upwards [density_smul_accessible D X h,
169     D.density_nonneg_ae (X.action h) (X.state h).2.1] with y he hn
170   rw [ENNReal.toReal_ofReal hn,smul_smul,mul_comm,← smul_smul,he]
171   rfl
172 
173 /-- Weighted operator integrability supplies the genuine conditional
174 response integrability after density/posterior cancellation. -/
175 theorem accessible_response_integrable_kernel (g : Y → ℝ)
176     (hgi : ∀ a,Integrable (fun y => g y • D.op a y) ν) (h : H) :
177     Integrable (fun y => g y • (X.next (h,y)).1) (historyKernel D X h) := by
178   change Integrable _ (D.kernel (X.action h) (X.state h))
179   have hd : Measurable (fun y => ENNReal.ofReal (D.density (X.action h) y (X.state h).1)) :=
180     (((D.density_measurable (X.action h)).comp
181       (measurable_const.prodMk measurable_id)).ennreal_ofReal)
182   rw [D.kernel_apply,integrable_withDensity_iff_integrable_smul' hd
183     (Filter.Eventually.of_forall (fun _ => ENNReal.ofReal_lt_top))]
184   apply ((ContinuousLinearMap.apply ℝ E (X.state h).1).integrable_comp (hgi (X.action h))).congr
185   filter_upwards [density_smul_accessible D X h,
186     D.density_nonneg_ae (X.action h) (X.state h).2.1] with y he hn
187   rw [ENNReal.toReal_ofReal hn,smul_smul,mul_comm,← smul_smul,he]
188   rfl
189 
190 /-- The conditional absolute response integral has a uniform finite bound
191 from the compact normalized base and the actual weighted operator norms. -/
192 theorem exists_response_norm_bound (g : Y → ℝ)
193     (hgi : ∀ a,Integrable (fun y => g y • D.op a y) ν) :
194     ∃ K : ℝ,∀ h,(∫ y,‖g y • (X.next (h,y)).1‖∂historyKernel D X h)≤K := by
195   obtain ⟨R,hRpos,hR⟩ := C.exists_cone_bound
196   refine ⟨R*∑ a,∫ y,‖g y • D.op a y‖∂ν,?_⟩
197   intro h
198   have hzR : ‖(X.state h).1‖≤R := by
199     simpa only [(X.state h).2.2,mul_one] using hR (X.state h).1 (X.state h).2.1
200   have heq : (∫ y,‖g y • (X.next (h,y)).1‖∂historyKernel D X h)=
201       ∫ y,‖(g y • D.op (X.action h) y) (X.state h).1‖∂ν := by
202     change (∫ y,‖g y • (X.next (h,y)).1‖∂D.kernel (X.action h) (X.state h))=_
203     have hd : Measurable (fun y => ENNReal.ofReal (D.density (X.action h) y (X.state h).1)) :=
204       (((D.density_measurable (X.action h)).comp
205         (measurable_const.prodMk measurable_id)).ennreal_ofReal)
206     rw [D.kernel_apply,integral_withDensity_eq_integral_toReal_smul hd
207       (Filter.Eventually.of_forall (fun _ => ENNReal.ofReal_lt_top))]
208     apply integral_congr_ae
209     filter_upwards [density_smul_accessible D X h,
210       D.density_nonneg_ae (X.action h) (X.state h).2.1] with y he hn
211     rw [ENNReal.toReal_ofReal hn]
212     have hv : D.density (X.action h) y (X.state h).1 • (g y • (X.next (h,y)).1)=
213         (g y • D.op (X.action h) y) (X.state h).1 := by
214       rw [smul_smul,mul_comm,← smul_smul,he]
215       rfl
216     have hvnorm := congrArg norm hv
217     rw [norm_smul,Real.norm_eq_abs,abs_of_nonneg hn] at hvnorm
218     exact hvnorm
219   rw [heq]
220   calc
221     _ ≤ ∫ y,R*‖g y • D.op (X.action h) y‖∂ν := by
222       apply integral_mono_ae
223         (((ContinuousLinearMap.apply ℝ E (X.state h).1).integrable_comp (hgi (X.action h))).norm)
224         ((hgi (X.action h)).norm.const_mul R)
225       exact Filter.Eventually.of_forall (fun y =>
226         ((g y • D.op (X.action h) y).le_opNorm (X.state h).1).trans
227           (by nlinarith [norm_nonneg (g y • D.op (X.action h) y)]))
228     _ = R*(∫ y,‖g y • D.op (X.action h) y‖∂ν) := integral_const_mul _ _
229     _ ≤ _ := by
230       have hs : (∫ y,‖g y • D.op (X.action h) y‖∂ν)≤
231           ∑ a : A,∫ y,‖g y • D.op a y‖∂ν :=
232         Finset.single_le_sum (f := fun a : A => ∫ y,‖g y • D.op a y‖∂ν)
233           (fun (a : A) _ => integral_nonneg (fun _ => norm_nonneg _))
234           (Finset.mem_univ (X.action h))
235       exact mul_le_mul_of_nonneg_left hs hRpos.le
236 
237 variable {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
238 
239 /-- The actual observable-history experiment proves the conditional moment
240 identity. Integrability is the ordinary analytic hypothesis for this vector
241 conditional expectation, not an assumed conditional-mean certificate. -/
242 theorem accessible_conditional_moment_of_integrable (history : Ω → H) (observation : Ω → Y)
243     (hh : Measurable history) (hy : Measurable observation)
244     (hlaw : μ.map (fun ω => (history ω,observation ω))=(μ.map history) ⊗ₘ historyKernel D X)
245     (g : Y → ℝ) (hg : Measurable g)
246     (hgi : ∀ a,Integrable (fun y => g y • D.op a y) ν)
247     (hi : Integrable (fun ω => g (observation ω) • (X.next (history ω,observation ω)).1) μ) :
248     μ[fun ω => g (observation ω) • (X.next (history ω,observation ω)).1 |
249       (inferInstance : MeasurableSpace H).comap history] =ᵐ[μ]
250       (fun ω => momentOperator D g (X.action (history ω)) (X.state (history ω)).1) := by
251   have hF : Measurable (fun p : H × Y => g p.2 • (X.next p).1) :=
252     (hg.comp measurable_snd).smul (measurable_subtype_coe.comp X.next_measurable)
253   have hc := history_condExp history observation hh hy (historyKernel D X) hlaw _ hF hi
254   apply hc.trans
255   exact Filter.Eventually.of_forall (fun ω => kernel_weighted_accessible D X g hgi (history ω))
256 
257 /-- Actual response integrability follows from weighted operator
258 integrability and normalized accessible states, without a bounded-test proxy. -/
259 theorem accessible_response_integrable (history : Ω → H) (observation : Ω → Y)
260     (hh : Measurable history) (hy : Measurable observation)
261     (hlaw : μ.map (fun ω => (history ω,observation ω))=(μ.map history) ⊗ₘ historyKernel D X)
262     (g : Y → ℝ) (hg : Measurable g)
263     (hgi : ∀ a,Integrable (fun y => g y • D.op a y) ν) :
264     Integrable (fun ω => g (observation ω) • (X.next (history ω,observation ω)).1) μ := by
265   have hF : Measurable (fun p : H × Y => g p.2 • (X.next p).1) :=
266     (hg.comp measurable_snd).smul (measurable_subtype_coe.comp X.next_measurable)
267   have hn : Measurable (fun h => ∫ y,‖g y • (X.next (h,y)).1‖∂historyKernel D X h) :=
268     hF.norm.stronglyMeasurable.integral_kernel_prod_right'.measurable
269   obtain ⟨K,hK⟩ := exists_response_norm_bound D X g hgi
270   have hni : Integrable (fun h => ∫ y,‖g y • (X.next (h,y)).1‖∂historyKernel D X h)
271       (μ.map history) := by
272     apply (integrable_const K).mono' hn.aestronglyMeasurable
273     exact Filter.Eventually.of_forall (fun h => by
274       rw [Real.norm_eq_abs,abs_of_nonneg (integral_nonneg (fun _ => norm_nonneg _))]
275       exact hK h)
276   have hFi : Integrable (fun p : H × Y => g p.2 • (X.next p).1)
277       ((μ.map history) ⊗ₘ historyKernel D X) :=
278     (Measure.integrable_compProd_iff hF.stronglyMeasurable.aestronglyMeasurable).mpr
279       ⟨Filter.Eventually.of_forall (accessible_response_integrable_kernel D X g hgi),hni⟩
280   rw [← hlaw] at hFi
281   exact hFi.comp_measurable (hh.prodMk hy)
282 
283 /-- P82's actual conditional moment identity with its analytic integrability
284 derived from the instrument and weighted basis products. -/
285 theorem accessible_conditional_moment (history : Ω → H) (observation : Ω → Y)
286     (hh : Measurable history) (hy : Measurable observation)
287     (hlaw : μ.map (fun ω => (history ω,observation ω))=(μ.map history) ⊗ₘ historyKernel D X)
288     (g : Y → ℝ) (hg : Measurable g)
289     (hgi : ∀ a,Integrable (fun y => g y • D.op a y) ν) :
290     μ[fun ω => g (observation ω) • (X.next (history ω,observation ω)).1 |
291       (inferInstance : MeasurableSpace H).comap history] =ᵐ[μ]
292       (fun ω => momentOperator D g (X.action (history ω)) (X.state (history ω)).1) :=
293   accessible_conditional_moment_of_integrable D X history observation hh hy hlaw g hg hgi
294     (accessible_response_integrable D X history observation hh hy hlaw g hg hgi)
295 
296 end Instrument
297 end Komorebi.LSM.ObservableMoments

Back to source controls