RegressionExponential.lean

1 import KomorebiLSM.ConditionalRandomMultiplier
2 import KomorebiLSM.RegressionGeometry
3 import Mathlib.Probability.Martingale.Basic
4 import Mathlib.MeasureTheory.Integral.Prod
5 
6 /-! The literal exponential product generated by predictable regression designs
7 is a nonnegative supermartingale. A fixed probability mixture is derived by
8 joint measurability and actual product-measure integration. -/
9 set_option autoImplicit false
10 namespace Komorebi.LSM.RegressionConfidence
11 open MeasureTheory ProbabilityTheory Matrix Real
12 open scoped BigOperators ENNReal
13 variable {Ω : Type*} [mΩ : MeasurableSpace Ω]
14 variable {μ : Measure Ω} [IsProbabilityMeasure μ]
15 variable {I : Type*} [Fintype I] [DecidableEq I]
16 
17 /-- The predictable scalar projection used for one fixed exponential direction. -/
18 noncomputable def projection (σ : ℝ) (φ : ℕ → Ω → I → ℝ) (q : I → ℝ) (n : ℕ) (ω : Ω) : ℝ :=
19   (q ⬝ᵥ φ n ω)/σ
20 
21 /-- The actual finite product, starting before observation zero. -/
22 noncomputable def exponentialProcess (σ : ℝ) (φ : ℕ → Ω → I → ℝ) (ξ : ℕ → Ω → ℝ)
23     (q : I → ℝ) (n : ℕ) (ω : Ω) : ℝ :=
24   ∏ i∈Finset.range n,factor (ξ i) σ (projection σ φ q i) ω
25 
26 omit [MeasurableSpace Ω] [DecidableEq I] in
27 @[simp] theorem exponentialProcess_zero (σ : ℝ) (φ : ℕ → Ω → I → ℝ)
28     (ξ : ℕ → Ω → ℝ) (q : I → ℝ) (ω : Ω) : exponentialProcess σ φ ξ q 0 ω=1 := by
29   simp [exponentialProcess]
30 
31 omit [MeasurableSpace Ω] [DecidableEq I] in
32 theorem exponentialProcess_succ (σ : ℝ) (φ : ℕ → Ω → I → ℝ)
33     (ξ : ℕ → Ω → ℝ) (q : I → ℝ) (n : ℕ) (ω : Ω) :
34     exponentialProcess σ φ ξ q (n+1) ω=
35       exponentialProcess σ φ ξ q n ω*factor (ξ n) σ (projection σ φ q n) ω := by
36   simp only [exponentialProcess,Finset.prod_range_succ]
37 
38 omit [MeasurableSpace Ω] [DecidableEq I] in
39 theorem exponentialProcess_pos (σ : ℝ) (φ : ℕ → Ω → I → ℝ)
40     (ξ : ℕ → Ω → ℝ) (q : I → ℝ) (n : ℕ) (ω : Ω) :
41     0<exponentialProcess σ φ ξ q n ω :=
42   Finset.prod_pos (fun _ _ => factor_pos _ _)
43 
44 omit [MeasurableSpace Ω] [DecidableEq I] in
45 /-- The product equals the exact source score/Gram exponential, rather than
46 being supplied as a process with an assumed logarithmic formula. -/
47 theorem exponentialProcess_eq (σ : ℝ) (hσ : σ≠0) (φ : ℕ → Ω → I → ℝ)
48     (ξ : ℕ → Ω → ℝ) (q : I → ℝ) (n : ℕ) (ω : Ω) :
49     exponentialProcess σ φ ξ q n ω=
50       exp ((q ⬝ᵥ responseVector (fun i => φ i ω) (fun i => ξ i ω) n)/σ-
51         (q ⬝ᵥ (designGram (fun i => φ i ω) n *ᵥ q))/2) := by
52   have he (i : ℕ) : factor (ξ i) σ (projection σ φ q i) ω=
53       exp ((q ⬝ᵥ φ i ω)*ξ i ω/σ-(q ⬝ᵥ φ i ω)^2/2) := by
54     unfold factor projection
55     congr 1
56     field_simp
57   unfold exponentialProcess
58   simp only [he]
59   rw [← Real.exp_sum]
60   congr 1
61   rw [designGram_quadratic]
62   simp only [responseVector,dotProduct_sum,dotProduct_smul,smul_eq_mul,
63     Finset.sum_sub_distrib,Finset.sum_div]
64   congr 1
65   apply Finset.sum_congr rfl
66   intro i _
67   ring
68 
69 section Predictable
70 variable (ℱ : Filtration ℕ mΩ) (σ : ℝ) (φ : ℕ → Ω → I → ℝ) (ξ : ℕ → Ω → ℝ)
71 variable (hφ : ∀ n i,Measurable[ℱ n] (fun ω => φ n ω i))
72 variable (hξ : ∀ n,Measurable[ℱ (n+1)] (ξ n))
73 variable (H : ∀ n,ConditionalSubgaussian (ℱ.le n) (ξ n) σ μ)
74 
75 include hφ in
76 omit [DecidableEq I] in
77 theorem projection_measurable (q : I → ℝ) (n : ℕ) :
78     Measurable[ℱ n] (projection σ φ q n) := by
79   unfold projection dotProduct
80   exact (Finset.measurable_sum _ (fun i _ => measurable_const.mul (hφ n i))).div_const σ
81 
82 include hφ hξ in
83 omit [DecidableEq I] in
84 theorem exponentialProcess_measurable (q : I → ℝ) :
85     ∀ n,Measurable[ℱ n] (exponentialProcess σ φ ξ q n)
86   | 0 => by
87     have he : exponentialProcess σ φ ξ q 0=(fun _ : Ω => (1:ℝ)) :=
88       funext (exponentialProcess_zero σ φ ξ q)
89     rw [he]
90     exact measurable_const
91   | n+1 => by
92     have hp : Measurable[ℱ (n+1)] (exponentialProcess σ φ ξ q n) :=
93       (exponentialProcess_measurable q n).mono (ℱ.mono (Nat.le_succ n)) le_rfl
94     have hf : Measurable[ℱ (n+1)] (factor (ξ n) σ (projection σ φ q n)) := by
95       let : MeasurableSpace Ω := ℱ (n+1)
96       exact factor_measurable (mΩ := ℱ (n+1)) (hξ n)
97         ((projection_measurable (mΩ := mΩ) ℱ σ φ hφ q n).mono (ℱ.mono (Nat.le_succ n)) le_rfl)
98     have he : exponentialProcess σ φ ξ q (n+1)=
99         (fun ω => exponentialProcess σ φ ξ q n ω*factor (ξ n) σ (projection σ φ q n) ω) :=
100       funext (exponentialProcess_succ σ φ ξ q n)
101     rw [he]
102     exact hp.mul hf
103 
104 include hφ hξ H in
105 omit [DecidableEq I] in
106 theorem exponentialProcess_integrable (q : I → ℝ) :
107     ∀ n,Integrable (exponentialProcess σ φ ξ q n) μ
108   | 0 => by
109     have he : exponentialProcess σ φ ξ q 0=(fun _ : Ω => (1:ℝ)) :=
110       funext (exponentialProcess_zero σ φ ξ q)
111     rw [he]
112     exact integrable_const _
113   | n+1 => by
114     have hi := (H n).weighted_factor_integrable (projection σ φ q n)
115       (projection_measurable ℱ σ φ hφ q n) (exponentialProcess σ φ ξ q n)
116       (exponentialProcess_measurable ℱ σ φ ξ hφ hξ q n)
117       (exponentialProcess_integrable q n) (fun ω => (exponentialProcess_pos σ φ ξ q n ω).le)
118     have he : exponentialProcess σ φ ξ q (n+1)=
119         (fun ω => exponentialProcess σ φ ξ q n ω*factor (ξ n) σ (projection σ φ q n) ω) :=
120       funext (exponentialProcess_succ σ φ ξ q n)
121     rw [he]
122     exact hi
123 
124 include hφ hξ H in
125 omit [DecidableEq I] in
126 theorem exponentialProcess_setIntegral_succ_le (q : I → ℝ) (n : ℕ)
127     {s : Set Ω} (hs : MeasurableSet[ℱ n] s) :
128     (∫ ω in s,exponentialProcess σ φ ξ q (n+1) ω∂μ)≤
129       ∫ ω in s,exponentialProcess σ φ ξ q n ω∂μ := by
130   simpa only [exponentialProcess_succ] using (H n).setIntegral_weighted_factor_le
131     (projection σ φ q n) (projection_measurable ℱ σ φ hφ q n)
132     (exponentialProcess σ φ ξ q n) (exponentialProcess_measurable ℱ σ φ ξ hφ hξ q n)
133     (exponentialProcess_integrable ℱ σ φ ξ hφ hξ H q n)
134     (fun ω => (exponentialProcess_pos σ φ ξ q n ω).le) hs
135 
136 include hφ hξ H in
137 omit [DecidableEq I] in
138 /-- Fixed-q supermartingale status follows from the actual conditional noise
139 bounds, predictable designs and the literal product recurrence. -/
140 theorem exponentialProcess_supermartingale (q : I → ℝ) :
141     Supermartingale (exponentialProcess σ φ ξ q) ℱ μ :=
142   supermartingale_of_setIntegral_succ_le
143     (fun n => (exponentialProcess_measurable ℱ σ φ ξ hφ hξ q n).stronglyMeasurable)
144     (exponentialProcess_integrable ℱ σ φ ξ hφ hξ H q)
145     (fun n _ hs => exponentialProcess_setIntegral_succ_le ℱ σ φ ξ hφ hξ H q n hs)
146 
147 end Predictable
148 /-- A fixed probability mixture of the literal processes. -/
149 noncomputable def probabilityMixture {Q : Type*} [MeasurableSpace Q] (ν : Measure Q)
150     (F : Q → ℕ → Ω → ℝ) (n : ℕ) (ω : Ω) : ℝ := ∫ q,F q n ω∂ν
151 
152 section GeneralMixture
153 variable {Q : Type*} [mQ : MeasurableSpace Q] (ν : Measure Q) [IsProbabilityMeasure ν]
154 variable (ℱ : Filtration ℕ mΩ) (F : Q → ℕ → Ω → ℝ)
155 variable (hF : ∀ q,Supermartingale (F q) ℱ μ)
156 variable (hjoint : ∀ n,Measurable[mQ.prod (ℱ n)] (fun p : Q × Ω => F p.1 n p.2))
157 variable (hnonneg : ∀ q n ω,0≤F q n ω) (hinit : ∀ q ω,F q 0 ω=1)
158 
159 include hF hjoint hnonneg hinit in
160 /-- Joint integrability is derived from Tonelli's norm criterion and the
161 individual supermartingale expectation budgets. It is not a mixture premise. -/
162 theorem mixture_joint_integrable (n : ℕ) :
163     Integrable (fun p : Q × Ω => F p.1 n p.2) (ν.prod μ) := by
164   have hprod : mQ.prod (ℱ n)≤mQ.prod mΩ :=
165     sup_le_sup le_rfl (MeasurableSpace.comap_mono (g := Prod.snd) (ℱ.le n))
166   have hm : Measurable (fun p : Q × Ω => F p.1 n p.2) :=
167     (hjoint n).mono hprod le_rfl
168   have hb (q : Q) : (∫ ω,F q n ω∂μ)≤1 := by
169     have hs := (hF q).setIntegral_le (i := 0) (j := n) (Nat.zero_le n) MeasurableSet.univ
170     simpa only [Measure.restrict_univ,hinit,integral_const,measureReal_def,
171       measure_univ,ENNReal.toReal_one,one_smul] using hs
172   apply (integrable_prod_iff hm.aestronglyMeasurable).2
173   refine ⟨ae_of_all _ (fun q => (hF q).integrable n),?_⟩
174   apply Integrable.of_bound hm.norm.stronglyMeasurable.integral_prod_right'.aestronglyMeasurable 1
175   filter_upwards [] with q
176   have he : (∫ ω,‖F q n ω‖∂μ)=∫ ω,F q n ω∂μ :=
177     integral_congr_ae (ae_of_all _ (fun ω => Real.norm_of_nonneg (hnonneg q n ω)))
178   rw [Real.norm_eq_abs,abs_of_nonneg (integral_nonneg (fun ω => norm_nonneg (F q n ω))),he]
179   exact hb q
180 
181 include hF hjoint hnonneg hinit in
182 /-- A probability mixture of nonnegative supermartingales starting at one is
183 an actual supermartingale. Joint measurability and Tonelli/Fubini derive the
184 conditional event inequalities. -/
185 theorem probabilityMixture_supermartingale : Supermartingale (probabilityMixture ν F) ℱ μ := by
186   have hi := mixture_joint_integrable ν ℱ F hF hjoint hnonneg hinit
187   apply supermartingale_of_setIntegral_succ_le
188   · intro n
189     let : MeasurableSpace Ω := ℱ n
190     exact (hjoint n).stronglyMeasurable.integral_prod_left'
191   · intro n
192     exact (hi n).integral_prod_right
193   · intro n s hs
194     have hin : Integrable (fun p : Q × Ω => F p.1 n p.2) (ν.prod (μ.restrict s)) :=
195       (hi n).mono_measure (Measure.prod_mono le_rfl Measure.restrict_le_self)
196     have his : Integrable (fun p : Q × Ω => F p.1 (n+1) p.2) (ν.prod (μ.restrict s)) :=
197       (hi (n+1)).mono_measure (Measure.prod_mono le_rfl Measure.restrict_le_self)
198     calc (∫ ω in s,probabilityMixture ν F (n+1) ω∂μ)=
199         ∫ q,∫ ω in s,F q (n+1) ω∂μ∂ν := (integral_integral_swap his).symm
200       _ ≤ ∫ q,∫ ω in s,F q n ω∂μ∂ν :=
201         integral_mono his.integral_prod_left hin.integral_prod_left
202           (fun q => (hF q).setIntegral_le (Nat.le_succ n) hs)
203       _ = ∫ ω in s,probabilityMixture ν F n ω∂μ := integral_integral_swap hin
204 end GeneralMixture
205 
206 section RegressionMixture
207 variable (ℱ : Filtration ℕ mΩ) (σ : ℝ) (φ : ℕ → Ω → I → ℝ) (ξ : ℕ → Ω → ℝ)
208 variable (hφ : ∀ n i,Measurable[ℱ n] (fun ω => φ n ω i))
209 variable (hξ : ∀ n,Measurable[ℱ (n+1)] (ξ n))
210 variable (H : ∀ n,ConditionalSubgaussian (ℱ.le n) (ξ n) σ μ)
211 
212 include hφ hξ in
213 omit [DecidableEq I] in
214 /-- The literal regression family is jointly measurable in the mixing direction
215 and recorded history, already at the current filtration level. -/
216 theorem exponentialProcess_joint_measurable (n : ℕ) :
217     Measurable[(inferInstance : MeasurableSpace (I → ℝ)).prod (ℱ n)]
218       (fun p : (I → ℝ) × Ω => exponentialProcess σ φ ξ p.1 n p.2) := by
219   let : MeasurableSpace Ω := ℱ n
220   unfold exponentialProcess
221   apply Finset.measurable_prod
222   intro i hi
223   have hlt : i<n := Finset.mem_range.mp hi
224   have ha : Measurable (fun p : (I → ℝ) × Ω => projection σ φ p.1 i p.2) := by
225     unfold projection dotProduct
226     apply Measurable.div_const
227     apply Finset.measurable_sum
228     intro j _
229     exact ((measurable_pi_apply j).comp measurable_fst).mul
230       (((hφ i j).mono (ℱ.mono (Nat.le_of_lt hlt)) le_rfl).comp measurable_snd)
231   have hx : Measurable (fun p : (I → ℝ) × Ω => ξ i p.2) :=
232     ((hξ i).mono (ℱ.mono (Nat.succ_le_of_lt hlt)) le_rfl).comp measurable_snd
233   exact factor_measurable hx ha
234 
235 /-- The literal probability mixture of fixed-direction regression products. -/
236 noncomputable def exponentialMixture (ν : Measure (I → ℝ)) (n : ℕ) (ω : Ω) : ℝ :=
237   probabilityMixture ν (fun q => exponentialProcess σ φ ξ q) n ω
238 
239 omit [MeasurableSpace Ω] [DecidableEq I] in
240 @[simp] theorem exponentialMixture_zero (ν : Measure (I → ℝ)) [IsProbabilityMeasure ν]
241     (ω : Ω) : exponentialMixture σ φ ξ ν 0 ω=1 := by
242   simp [exponentialMixture,probabilityMixture]
243 
244 omit [MeasurableSpace Ω] [DecidableEq I] in
245 theorem exponentialMixture_nonneg (ν : Measure (I → ℝ)) (n : ℕ) (ω : Ω) :
246     0≤exponentialMixture σ φ ξ ν n ω :=
247   integral_nonneg (fun q => (exponentialProcess_pos σ φ ξ q n ω).le)
248 
249 omit [MeasurableSpace Ω] [DecidableEq I] in
250 /-- The mixture integrand is exactly the score/Gram exponential used by the
251 Gaussian completing-square calculation. -/
252 theorem exponentialMixture_eq (hσ : σ≠0) (ν : Measure (I → ℝ)) (n : ℕ) (ω : Ω) :
253     exponentialMixture σ φ ξ ν n ω=
254       ∫ q,exp ((q ⬝ᵥ responseVector (fun i => φ i ω) (fun i => ξ i ω) n)/σ-
255         (q ⬝ᵥ (designGram (fun i => φ i ω) n *ᵥ q))/2)∂ν :=
256   integral_congr_ae (ae_of_all _ (fun q => exponentialProcess_eq σ hσ φ ξ q n ω))
257 
258 include hφ hξ H in
259 omit [DecidableEq I] in
260 /-- Every fixed probability law on directions gives an actual nonnegative
261 regression-mixture supermartingale, without a design bound or density margin. -/
262 theorem exponentialMixture_supermartingale (ν : Measure (I → ℝ)) [IsProbabilityMeasure ν] :
263     Supermartingale (exponentialMixture σ φ ξ ν) ℱ μ :=
264   probabilityMixture_supermartingale ν ℱ (fun q => exponentialProcess σ φ ξ q)
265     (fun q => exponentialProcess_supermartingale ℱ σ φ ξ hφ hξ H q)
266     (exponentialProcess_joint_measurable ℱ σ φ ξ hφ hξ)
267     (fun q n ω => (exponentialProcess_pos σ φ ξ q n ω).le)
268     (fun q ω => exponentialProcess_zero σ φ ξ q ω)
269 
270 include hφ hξ H in
271 omit [DecidableEq I] in
272 /-- Tonelli also supplies actual almost-everywhere integrability of the mixing
273 fiber; it is derived rather than silently presumed. -/
274 theorem exponentialMixture_fiber_integrable_ae (ν : Measure (I → ℝ)) [IsProbabilityMeasure ν]
275     (n : ℕ) : ∀ᵐ ω∂μ,Integrable (fun q => exponentialProcess σ φ ξ q n ω) ν := by
276   have hi := mixture_joint_integrable ν ℱ (fun q => exponentialProcess σ φ ξ q)
277     (fun q => exponentialProcess_supermartingale ℱ σ φ ξ hφ hξ H q)
278     (exponentialProcess_joint_measurable ℱ σ φ ξ hφ hξ)
279     (fun q n ω => (exponentialProcess_pos σ φ ξ q n ω).le)
280     (fun q ω => exponentialProcess_zero σ φ ξ q ω) n
281   exact hi.prod_left_ae
282 end RegressionMixture
283 
284 end Komorebi.LSM.RegressionConfidence

Back to source controls