ObservableMomentProcess.lean

1 import KomorebiLSM.ObservableMomentConditional
2 import Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
3 import Mathlib.LinearAlgebra.Matrix.ToLin
4 import Mathlib.Probability.Process.Filtration
5 
6 /-! Actual observable-history instruments yield predictable moment-regression
7 designs and responses. Accessibility and conditional experiment laws are
8 explicit inputs; no regression mean or confidence event is an input field. -/
9 set_option autoImplicit false
10 namespace Komorebi.LSM.ObservableMoments
11 open MeasureTheory ProbabilityTheory Matrix
12 open scoped ENNReal BigOperators Matrix
13 
14 section Process
15 variable {Ω H E A Y : Type*} [mΩ : MeasurableSpace Ω] [mH : MeasurableSpace H]
16 variable [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
17 variable [MeasurableSpace E] [BorelSpace E] [MeasurableSpace Y]
18 variable [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A]
19 variable {C : BaseNorm.ProbabilityCone E} {ν : Measure Y} [IsProbabilityMeasure ν]
20 variable (D : ContinuousInstrument.DensityInstrument (A := A) C ν)
21 variable {μ : Measure Ω} [IsProbabilityMeasure μ]
22 
23 /-- The information is exactly a recorded history, and both successive states
24 are given by specified measurable maps of those observations. -/
25 structure AccessibleProcess (ℱ : Filtration ℕ mΩ) where
26   history : ℕ → Ω → H
27   history_measurable : ∀ n,Measurable[ℱ n] (history n)
28   history_generates : ∀ n,mH.comap (history n)=ℱ n
29   observation : ℕ → Ω → Y
30   observation_measurable : ∀ n,Measurable[ℱ (n+1)] (observation n)
31   stateMap : ℕ → AccessibleState (H := H) D
32   joint_law : ∀ n,μ.map (fun ω => (history n ω,observation n ω))=
33     (μ.map (history n)) ⊗ₘ historyKernel D (stateMap n)
34   next_state : ∀ n,∀ᵐ ω∂μ,(stateMap n).next (history n ω,observation n ω)=
35     (stateMap (n+1)).state (history (n+1) ω)
36 
37 variable {ℱ : Filtration ℕ mΩ} (P : AccessibleProcess (H := H) (μ := μ) D ℱ)
38 
39 noncomputable def currentState (n : ℕ) (ω : Ω) : E := (P.stateMap n).state (P.history n ω)
40 def currentAction (n : ℕ) (ω : Ω) : A := (P.stateMap n).action (P.history n ω)
41 
42 omit [FiniteDimensional ℝ E] [BorelSpace E] [IsProbabilityMeasure μ] in
43 theorem currentState_measurable (n : ℕ) : Measurable[ℱ n] (currentState D P n) :=
44   measurable_subtype_coe.comp ((P.stateMap n).state_measurable.comp (P.history_measurable n))
45 
46 omit [FiniteDimensional ℝ E] [BorelSpace E] [IsProbabilityMeasure μ] in
47 theorem currentAction_measurable (n : ℕ) : Measurable[ℱ n] (currentAction D P n) :=
48   (P.stateMap n).action_measurable.comp (P.history_measurable n)
49 
50 omit [FiniteDimensional ℝ E] [BorelSpace E] [IsProbabilityMeasure μ] in
51 theorem currentState_mem (n : ℕ) (ω : Ω) : currentState D P n ω∈C.base :=
52   ((P.stateMap n).state (P.history n ω)).2
53 
54 theorem currentState_integrable (n : ℕ) : Integrable (currentState D P n) μ := by
55   obtain ⟨R,_,hR⟩ := C.exists_cone_bound
56   apply (integrable_const R).mono'
57     ((currentState_measurable D P n).mono (ℱ.le n) le_rfl).aestronglyMeasurable
58   exact Filter.Eventually.of_forall (fun ω => by
59     simpa only [(currentState_mem D P n ω).2,mul_one] using
60       hR (currentState D P n ω) (currentState_mem D P n ω).1)
61 
62 /-- The literal next accessible state gives an integrable moment response. -/
63 theorem momentResponse_integrable (g : Y → ℝ) (hg : Measurable g)
64     (hgi : ∀ a,Integrable (fun y => g y • D.op a y) ν) (n : ℕ) :
65     Integrable (fun ω => g (P.observation n ω) • currentState D P (n+1) ω) μ := by
66   have hi := accessible_response_integrable D (P.stateMap n) (P.history n) (P.observation n)
67     ((P.history_measurable n).mono (ℱ.le n) le_rfl)
68     ((P.observation_measurable n).mono (ℱ.le (n+1)) le_rfl) (P.joint_law n) g hg hgi
69   apply hi.congr
70   filter_upwards [P.next_state n] with ω he
71   rw [he]
72   rfl
73 
74 /-- The conditional moment is derived for the actual next state, with respect
75 to the actual observed-history filtration, at each dependent time. -/
76 theorem process_conditional_moment (g : Y → ℝ) (hg : Measurable g)
77     (hgi : ∀ a,Integrable (fun y => g y • D.op a y) ν) (n : ℕ) :
78     μ[fun ω => g (P.observation n ω) • currentState D P (n+1) ω | ℱ n] =ᵐ[μ]
79       (fun ω => momentOperator D g (currentAction D P n ω) (currentState D P n ω)) := by
80   have hc := accessible_conditional_moment D (P.stateMap n) (P.history n) (P.observation n)
81     ((P.history_measurable n).mono (ℱ.le n) le_rfl)
82     ((P.observation_measurable n).mono (ℱ.le (n+1)) le_rfl) (P.joint_law n) g hg hgi
83   rw [P.history_generates n] at hc
84   have heq : (fun ω => g (P.observation n ω) • currentState D P (n+1) ω)=ᵐ[μ]
85       (fun ω => g (P.observation n ω) • ((P.stateMap n).next (P.history n ω,P.observation n ω)).1) := by
86     filter_upwards [P.next_state n] with ω he
87     rw [he]
88     rfl
89   exact (condExp_congr_ae heq).trans hc
90 
91 /-- The action gate is known before the response is observed. -/
92 noncomputable def actionGate (a : A) (n : ℕ) (ω : Ω) : ℝ := by
93   classical
94   exact if currentAction D P n ω=a then 1 else 0
95 
96 omit [FiniteDimensional ℝ E] [BorelSpace E] [IsProbabilityMeasure μ] in
97 theorem actionGate_measurable (a : A) (n : ℕ) : Measurable[ℱ n] (actionGate D P a n) := by
98   classical
99   exact measurable_const.ite
100     ((measurableSet_singleton a).preimage (currentAction_measurable D P n)) measurable_const
101 
102 omit [FiniteDimensional ℝ E] [BorelSpace E] [IsProbabilityMeasure μ] in
103 theorem actionGate_norm_le (a : A) (n : ℕ) (ω : Ω) : ‖actionGate D P a n ω‖≤1 := by
104   classical
105   by_cases h : currentAction D P n ω=a <;> simp [actionGate,h]
106 
107 /-- An exact observable regressor for each target action, with zeros on all
108 other action visits. It is not an estimated hidden state. -/
109 noncomputable def gatedDesign (a : A) (n : ℕ) (ω : Ω) : E :=
110   actionGate D P a n ω • currentState D P n ω
111 
112 omit [FiniteDimensional ℝ E] [IsProbabilityMeasure μ] in
113 theorem gatedDesign_measurable (a : A) (n : ℕ) : Measurable[ℱ n] (gatedDesign D P a n) :=
114   (actionGate_measurable D P a n).smul (currentState_measurable D P n)
115 
116 theorem gatedDesign_integrable (a : A) (n : ℕ) : Integrable (gatedDesign D P a n) μ := by
117   apply ((currentState_integrable D P n).norm).mono'
118     ((gatedDesign_measurable D P a n).mono (ℱ.le n) le_rfl).aestronglyMeasurable
119   exact Filter.Eventually.of_forall (fun ω => by
120     rw [gatedDesign,norm_smul]
121     exact (mul_le_mul_of_nonneg_right (actionGate_norm_le D P a n ω) (norm_nonneg _)).trans_eq (one_mul _))
122 
123 end Process
124 
125 section Rows
126 variable {Ω H A Y : Type*} {r : ℕ} [mΩ : MeasurableSpace Ω] [mH : MeasurableSpace H]
127 variable [MeasurableSpace Y] [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A]
128 variable {C : BaseNorm.ProbabilityCone (Fin r → ℝ)} {ν : Measure Y} [IsProbabilityMeasure ν]
129 variable (D : ContinuousInstrument.DensityInstrument (A := A) C ν)
130 variable {μ : Measure Ω} [IsProbabilityMeasure μ] {ℱ : Filtration ℕ mΩ}
131 variable (P : AccessibleProcess (H := H) (μ := μ) D ℱ)
132 
133 /-- The actual matrix of an integrated operator moment in the fixed observable
134 coordinates, with no additional fit or coordinate identification. -/
135 noncomputable def momentMatrix (g : Y → ℝ) (a : A) : Matrix (Fin r) (Fin r) ℝ :=
136   LinearMap.toMatrix' (momentOperator D g a).toLinearMap
137 
138 omit [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A] [IsProbabilityMeasure ν] in
139 @[simp] theorem momentMatrix_mulVec (g : Y → ℝ) (a : A) (z : Fin r → ℝ) :
140     momentMatrix D g a *ᵥ z=momentOperator D g a z :=
141   LinearMap.toMatrix'_mulVec _ _
142 
143 noncomputable def gatedResponse (a : A) (g : Y → ℝ) (i : Fin r) (n : ℕ) (ω : Ω) : ℝ :=
144   actionGate D P a n ω*(g (P.observation n ω)*currentState D P (n+1) ω i)
145 
146 omit [IsProbabilityMeasure μ] in
147 /-- The response is genuinely recorded at the next filtration level. -/
148 theorem gatedResponse_measurable (a : A) (g : Y → ℝ) (hg : Measurable g)
149     (i : Fin r) (n : ℕ) : Measurable[ℱ (n+1)] (gatedResponse D P a g i n) :=
150   ((actionGate_measurable D P a n).mono (ℱ.mono (by omega)) le_rfl).mul
151     ((hg.comp (P.observation_measurable n)).mul
152       ((measurable_pi_apply i).comp (currentState_measurable D P (n+1))))
153 
154 /-- The action-gated response has the exact fixed row-moment regression mean.
155 This mean equation is a conclusion of the instrument experiment. -/
156 theorem gatedResponse_condExp (a : A) (g : Y → ℝ) (hg : Measurable g)
157     (hgi : ∀ b,Integrable (fun y => g y • D.op b y) ν) (i : Fin r) (n : ℕ) :
158     μ[gatedResponse D P a g i n | ℱ n] =ᵐ[μ]
159       (fun ω => (momentMatrix D g a *ᵥ gatedDesign D P a n ω) i) := by
160   let L : (Fin r → ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj i
161   have hi := momentResponse_integrable D P g hg hgi n
162   have hcoord := L.comp_condExp_comm (m := ℱ n) hi
163   have hcoord' : (fun ω => (μ[fun ω => g (P.observation n ω) • currentState D P (n+1) ω | ℱ n]) ω i)=ᵐ[μ]
164       μ[(fun ω => g (P.observation n ω)*currentState D P (n+1) ω i) | ℱ n] := by
165     simpa only [L,Function.comp_def,ContinuousLinearMap.proj_apply,Pi.smul_apply,smul_eq_mul] using hcoord
166   have hvec := process_conditional_moment D P g hg hgi n
167   have hrow : μ[(fun ω => g (P.observation n ω)*currentState D P (n+1) ω i) | ℱ n]=ᵐ[μ]
168       (fun ω => (momentOperator D g (currentAction D P n ω) (currentState D P n ω)) i) := by
169     filter_upwards [hcoord',hvec] with ω hc hv
170     rw [← hc,hv]
171   have hip : Integrable (fun ω => g (P.observation n ω)*currentState D P (n+1) ω i) μ :=
172     L.integrable_comp hi
173   have hpull := condExp_stronglyMeasurable_mul_of_bound (ℱ.le n)
174     (actionGate_measurable D P a n).stronglyMeasurable hip (1:ℝ)
175     (Filter.Eventually.of_forall (actionGate_norm_le D P a n))
176   filter_upwards [hpull,hrow] with ω hp hr
177   change (μ[(fun ω => actionGate D P a n ω)*
178     (fun ω => g (P.observation n ω)*currentState D P (n+1) ω i) | ℱ n]) ω=_
179   rw [hp]
180   change actionGate D P a n ω*(μ[fun ω => g (P.observation n ω)*currentState D P (n+1) ω i | ℱ n]) ω=_
181   rw [hr,momentMatrix_mulVec,gatedDesign,map_smul]
182   classical
183   by_cases ha : currentAction D P n ω=a
184   · simp [actionGate,ha]
185   · simp [actionGate,ha]
186 
187 end Rows
188 end Komorebi.LSM.ObservableMoments

Back to source controls