ConditionalRandomMultiplier.lean

1 import Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
2 import Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
3 import Mathlib.MeasureTheory.Function.SimpleFuncDense
4 import Mathlib.MeasureTheory.Integral.Bochner.Set
5 import Mathlib.MeasureTheory.Integral.Lebesgue.Add
6 import Mathlib.Analysis.SpecialFunctions.Exp
7 import Mathlib.Tactic
8 
9 /-! Deterministic conditional exponential bounds transfer to a predictable
10 random multiplier on an arbitrary probability space. Finite simple-function
11 approximation and nonnegative Fatou limits avoid a uniform all-parameter null
12 set and avoid any regular-conditional-distribution assumption on the sample
13 space. -/
14 set_option autoImplicit false
15 namespace Komorebi.LSM.RegressionConfidence
16 open MeasureTheory ProbabilityTheory Real Filter
17 open scoped ENNReal Topology
18 variable {Ω : Type*} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω]
19 variable {μ : Measure Ω}
20 /-- The normalized one-step exponential factor. -/
21 noncomputable def factor (X : Ω → ℝ) (σ : ℝ) (a : Ω → ℝ) (ω : Ω) : ℝ :=
22   exp (a ω*X ω-(a ω)^2*σ^2/2)
23 
24 variable {X : Ω → ℝ} {σ : ℝ}
25 
26 variable (hm : m ≤ mΩ)
27 
28 /-- The real coefficient is chosen before the almost-everywhere conclusion.
29 This field does not assert a uniform event for all coefficients. -/
30 structure ConditionalSubgaussian (hm : m ≤ mΩ) (X : Ω → ℝ) (σ : ℝ) (μ : @Measure Ω mΩ) : Prop where
31   measurable : @Measurable Ω ℝ mΩ _ X
32   integrable_exp : ∀ h : ℝ, Integrable (fun ω => exp (h*X ω)) μ
33   condExp_le : ∀ h : ℝ, (μ[fun ω => exp (h*X ω)|m])≤ᵐ[μ]
34     fun _ => exp (h^2*σ^2/2)
35 
36 variable {hm}
37 
38 omit [MeasurableSpace Ω] in
39 theorem factor_pos (a : Ω → ℝ) (ω : Ω) : 0<factor X σ a ω := exp_pos _
40 
41 theorem factor_measurable (hX : @Measurable Ω ℝ mΩ _ X) {a : Ω → ℝ}
42     (ha : @Measurable Ω ℝ mΩ _ a) : @Measurable Ω ℝ mΩ _ (factor X σ a) :=
43   (ha.mul hX |>.sub (((ha.pow_const 2).mul_const (σ^2)).div_const 2)).exp
44 
45 /-- A nonnegative pointwise Fatou limit inherits both integrability and an
46 integral budget. This is valid on any measurable sample space. -/
47 theorem nonnegative_limit_budget (ν : @Measure Ω mΩ) (f : Ω → ℝ) (fn : ℕ → Ω → ℝ)
48     (hf : Measurable f) (h0 : ∀ ω,0≤f ω) (hfn0 : ∀ n ω,0≤fn n ω)
49     (hfn : ∀ n,Integrable (fn n) ν) (C : ℝ) (hC : 0≤C)
50     (hbudget : ∀ n,(∫ ω,fn n ω∂ν)≤C)
51     (hlim : ∀ ω,Tendsto (fun n => fn n ω) atTop (𝓝 (f ω))) :
52     Integrable f ν ∧ (∫ ω,f ω∂ν)≤C := by
53   have hfatou : (∫⁻ ω,ENNReal.ofReal (f ω)∂ν)≤ENNReal.ofReal C := by
54     calc (∫⁻ ω,ENNReal.ofReal (f ω)∂ν)=
55         ∫⁻ ω,liminf (fun n => ENNReal.ofReal (fn n ω)) atTop∂ν := by
56           apply lintegral_congr
57           intro ω
58           exact ((ENNReal.continuous_ofReal.tendsto _).comp (hlim ω)).liminf_eq.symm
59       _ ≤ liminf (fun n => ∫⁻ ω,ENNReal.ofReal (fn n ω)∂ν) atTop :=
60         lintegral_liminf_le' (fun n => (hfn n).aemeasurable.ennreal_ofReal)
61       _ ≤ ENNReal.ofReal C := by
62         apply liminf_le_of_frequently_le'
63         apply Filter.Eventually.frequently
64         exact Filter.Eventually.of_forall (fun n => by
65           rw [← ofReal_integral_eq_lintegral_ofReal (hfn n) (ae_of_all _ (hfn0 n))]
66           exact ENNReal.ofReal_le_ofReal (hbudget n))
67   have hfi : Integrable f ν := ⟨hf.aestronglyMeasurable,
68     (hasFiniteIntegral_iff_ofReal (ae_of_all _ h0)).2
69       (lt_of_le_of_lt hfatou ENNReal.ofReal_lt_top)⟩
70   refine ⟨hfi,?_⟩
71   have hreal := ENNReal.toReal_mono ENNReal.ofReal_ne_top hfatou
72   rw [← ofReal_integral_eq_lintegral_ofReal hfi (ae_of_all _ h0),
73     ENNReal.toReal_ofReal (integral_nonneg h0),ENNReal.toReal_ofReal hC] at hreal
74   exact hreal
75 
76 namespace ConditionalSubgaussian
77 variable (H : ConditionalSubgaussian (mΩ := mΩ) hm X σ μ)
78 include H
79 
80 theorem constant_factor_integrable (h : ℝ) : Integrable (factor X σ (fun _ => h)) μ := by
81   have he : factor X σ (fun _ => h) = fun ω => exp (-(h^2*σ^2/2))*exp (h*X ω) := by
82     funext ω
83     dsimp [factor]
84     rw [← exp_add]
85     congr 1
86     ring
87   rw [he]
88   exact (H.integrable_exp h).const_mul _
89 
90 theorem constant_factor_condExp_le (h : ℝ) :
91     (μ[factor X σ (fun _ => h)|m])≤ᵐ[μ] fun _ => 1 := by
92   have he : factor X σ (fun _ => h) = exp (-(h^2*σ^2/2)) • (fun ω => exp (h*X ω)) := by
93     funext ω
94     simp only [factor, Pi.smul_apply, smul_eq_mul, ← exp_add]
95     congr 1
96     ring
97   rw [he]
98   filter_upwards [condExp_smul (μ := μ) (exp (-(h^2*σ^2/2))) (fun ω => exp (h*X ω)) m,
99     H.condExp_le h] with ω hp hb
100   rw [hp]
101   simp only [Pi.smul_apply,smul_eq_mul]
102   calc exp (-(h^2*σ^2/2))*(μ[fun ω => exp (h*X ω)|m]) ω ≤
103       exp (-(h^2*σ^2/2))*exp (h^2*σ^2/2) := mul_le_mul_of_nonneg_left hb (exp_pos _).le
104     _ = 1 := by rw [← exp_add]; simp
105 
106 /-- Each finite-valued predictable multiplier uses only finitely many of the
107 deterministic-coefficient conditional bounds. -/
108 theorem simple_factor (a : @SimpleFunc Ω m ℝ) :
109     Integrable (factor X σ a) μ ∧ (μ[factor X σ a|m])≤ᵐ[μ] fun _ => 1 := by
110   classical
111   induction a using SimpleFunc.induction' with
112   | const c => exact ⟨H.constant_factor_integrable c,H.constant_factor_condExp_le c⟩
113   | @pcw f g s hs hf hg =>
114     change Integrable (factor X σ (s.piecewise f g)) μ ∧
115       (μ[factor X σ (s.piecewise f g)|m])≤ᵐ[μ] fun _ => 1
116     have he : factor X σ (s.piecewise f g) =
117         s.indicator (factor X σ f)+sᶜ.indicator (factor X σ g) := by
118       funext ω
119       by_cases hω : ω∈s <;> simp [factor,hω]
120     rw [he]
121     have hfi := hf.1.indicator (hm _ hs)
122     have hgi := hg.1.indicator (hm _ hs.compl)
123     refine ⟨hfi.add hgi,?_⟩
124     filter_upwards [condExp_add hfi hgi (m := m),condExp_indicator hf.1 hs,
125       condExp_indicator hg.1 hs.compl,hf.2,hg.2] with ω ha hb hc hd he
126     rw [ha]
127     simp only [Pi.add_apply]
128     rw [hb,hc]
129     by_cases hω : ω∈s
130     · simpa [hω] using hd
131     · simpa [hω] using he
132 
133 variable [IsProbabilityMeasure μ]
134 
135 /-- A predictable multiplier is approximated by finite-valued predictable
136 functions. Fatou is applied separately on each conditioning event. -/
137 theorem random_factor_setIntegral (a : Ω → ℝ) (ha : Measurable[m] a)
138     {s : Set Ω} (hs : MeasurableSet[m] s) :
139     IntegrableOn (factor X σ a) s μ ∧ (∫ ω in s,factor X σ a ω∂μ)≤μ.real s := by
140   let an (n : ℕ) : @SimpleFunc Ω m ℝ := by
141     letI := m
142     exact SimpleFunc.approxOn a ha Set.univ 0 (by simp) n
143   have hlim (ω : Ω) : Tendsto (fun n => (an n) ω) atTop (𝓝 (a ω)) := by
144     let : MeasurableSpace Ω := m
145     exact SimpleFunc.tendsto_approxOn ha (by simp) (by simp)
146   have hlimf (ω : Ω) : Tendsto (fun n => factor X σ (an n) ω) atTop (𝓝 (factor X σ a ω)) := by
147     exact Real.continuous_exp.continuousAt.tendsto.comp
148       (((hlim ω).mul_const (X ω)).sub ((((hlim ω).pow 2).mul_const (σ^2)).div_const 2))
149   have hb (n : ℕ) : (∫ ω in s,factor X σ (an n) ω∂μ)≤μ.real s := by
150     calc (∫ ω in s,factor X σ (an n) ω∂μ)=
151         ∫ ω in s,(μ[factor X σ (an n)|m]) ω∂μ :=
152           (setIntegral_condExp hm (H.simple_factor (an n)).1 hs).symm
153       _ ≤ ∫ _ in s,(1:ℝ)∂μ :=
154         integral_mono_ae integrable_condExp.integrableOn (integrable_const _)
155           (ae_restrict_of_ae (H.simple_factor (an n)).2)
156       _ = μ.real s := by simp
157   exact nonnegative_limit_budget (μ.restrict s) (factor X σ a) (fun n => factor X σ (an n))
158     (factor_measurable H.measurable (ha.mono hm le_rfl))
159     (fun ω => (factor_pos a ω).le) (fun n ω => (factor_pos (an n) ω).le)
160     (fun n => (H.simple_factor (an n)).1.integrableOn) (μ.real s) ENNReal.toReal_nonneg hb hlimf
161 
162 /-- Unbounded predictable multipliers give an integrable normalized factor. -/
163 theorem random_factor_integrable (a : Ω → ℝ) (ha : Measurable[m] a) :
164     Integrable (factor X σ a) μ := by
165   simpa only [IntegrableOn,Measure.restrict_univ] using
166     (H.random_factor_setIntegral a ha MeasurableSet.univ).1
167 
168 /-- The deterministic-parameter hypotheses imply the actual conditional bound
169 at a random predictable parameter, with no uniform all-parameter event assumed. -/
170 theorem random_factor_condExp_le (a : Ω → ℝ) (ha : Measurable[m] a) :
171     (μ[factor X σ a|m])≤ᵐ[μ] fun _ => 1 := by
172   apply ae_le_of_ae_le_trim (hm := hm)
173   refine ae_le_of_forall_setIntegral_le
174     (Integrable.trim hm integrable_condExp stronglyMeasurable_condExp) (integrable_const 1) ?_
175   intro s hs _
176   rw [← setIntegral_trim hm stronglyMeasurable_condExp hs,
177     ← setIntegral_trim hm stronglyMeasurable_const hs,
178     setIntegral_condExp hm (H.random_factor_integrable a ha) hs]
179   simpa only [setIntegral_const,smul_eq_mul,mul_one] using (H.random_factor_setIntegral a ha hs).2
180 
181 /-- First pull out a bounded nonnegative conditioning-measurable weight. -/
182 theorem bounded_weight_factor (a : Ω → ℝ) (ha : Measurable[m] a)
183     (W : Ω → ℝ) (hW : Measurable[m] W) (hWi : Integrable W μ)
184     (hW0 : ∀ ω,0≤W ω) (K : ℝ) (hWK : ∀ ω,W ω≤K) :
185     Integrable (fun ω => W ω*factor X σ a ω) μ ∧
186       (∫ ω,W ω*factor X σ a ω∂μ)≤∫ ω,W ω∂μ := by
187   have hF := H.random_factor_integrable a ha
188   have hWF : Integrable (fun ω => W ω*factor X σ a ω) μ :=
189     hF.bdd_mul (hW.mono hm le_rfl).aestronglyMeasurable
190       (ae_of_all _ (fun ω => by simpa only [Real.norm_eq_abs,abs_of_nonneg (hW0 ω)] using hWK ω))
191   have hpull := condExp_mul_of_stronglyMeasurable_left hW.stronglyMeasurable hWF hF
192   refine ⟨hWF,?_⟩
193   calc (∫ ω,W ω*factor X σ a ω∂μ)=∫ ω,(μ[fun ω => W ω*factor X σ a ω|m]) ω∂μ :=
194       (integral_condExp hm).symm
195     _ ≤ ∫ ω,W ω∂μ := by
196       apply integral_mono_ae integrable_condExp hWi
197       filter_upwards [hpull,H.random_factor_condExp_le a ha] with ω hp hb
198       change (μ[W*factor X σ a|m]) ω≤W ω
199       rw [hp]
200       exact mul_le_of_le_one_right (hW0 ω) hb
201 
202 /-- Nonnegative Fatou localization removes the bounded-weight condition.
203 Weighted integrability is derived, rather than assumed. -/
204 theorem weighted_factor (a : Ω → ℝ) (ha : Measurable[m] a)
205     (W : Ω → ℝ) (hW : Measurable[m] W) (hWi : Integrable W μ) (hW0 : ∀ ω,0≤W ω) :
206     Integrable (fun ω => W ω*factor X σ a ω) μ ∧
207       (∫ ω,W ω*factor X σ a ω∂μ)≤∫ ω,W ω∂μ := by
208   let Wn (n : ℕ) (ω : Ω) : ℝ := min (W ω) (n:ℝ)
209   have hWnm (n : ℕ) : Measurable[m] (Wn n) := hW.min measurable_const
210   have hWn0 (n : ℕ) (ω : Ω) : 0≤Wn n ω := le_min (hW0 ω) (Nat.cast_nonneg n)
211   have hWnK (n : ℕ) (ω : Ω) : Wn n ω≤(n:ℝ) := min_le_right _ _
212   have hWni (n : ℕ) : Integrable (Wn n) μ := by
213     apply Integrable.of_bound (hWnm n |>.mono hm le_rfl).aestronglyMeasurable (n:ℝ)
214     exact ae_of_all _ (fun ω => by
215       simpa only [Real.norm_eq_abs,abs_of_nonneg (hWn0 n ω)] using hWnK n ω)
216   have hproduct (n : ℕ) := H.bounded_weight_factor a ha (Wn n) (hWnm n) (hWni n) (hWn0 n) n (hWnK n)
217   have hb (n : ℕ) : (∫ ω,Wn n ω*factor X σ a ω∂μ)≤∫ ω,W ω∂μ :=
218     (hproduct n).2.trans (integral_mono (hWni n) hWi (fun ω => min_le_left _ _))
219   have hlim (ω : Ω) : Tendsto (fun n => Wn n ω) atTop (𝓝 (W ω)) := by
220     obtain ⟨N,hN⟩ := exists_nat_ge (W ω)
221     have he : (fun n => Wn n ω)=ᶠ[atTop] fun _ => W ω := by
222       filter_upwards [eventually_ge_atTop N] with n hn
223       exact min_eq_left (hN.trans (by exact_mod_cast hn))
224     exact tendsto_const_nhds.congr' he.symm
225   exact nonnegative_limit_budget μ (fun ω => W ω*factor X σ a ω)
226     (fun n ω => Wn n ω*factor X σ a ω)
227     ((hW.mono hm le_rfl).mul (factor_measurable H.measurable (ha.mono hm le_rfl)))
228     (fun ω => mul_nonneg (hW0 ω) (factor_pos a ω).le)
229     (fun n ω => mul_nonneg (hWn0 n ω) (factor_pos a ω).le)
230     (fun n => (hproduct n).1) (∫ ω,W ω∂μ) (integral_nonneg hW0) hb
231     (fun ω => (hlim ω).mul_const (factor X σ a ω))
232 
233 theorem weighted_factor_integrable (a : Ω → ℝ) (ha : Measurable[m] a)
234     (W : Ω → ℝ) (hW : Measurable[m] W) (hWi : Integrable W μ) (hW0 : ∀ ω,0≤W ω) :
235     Integrable (fun ω => W ω*factor X σ a ω) μ := (H.weighted_factor a ha W hW hWi hW0).1
236 
237 theorem integral_weighted_factor_le (a : Ω → ℝ) (ha : Measurable[m] a)
238     (W : Ω → ℝ) (hW : Measurable[m] W) (hWi : Integrable W μ) (hW0 : ∀ ω,0≤W ω) :
239     (∫ ω,W ω*factor X σ a ω∂μ)≤∫ ω,W ω∂μ := (H.weighted_factor a ha W hW hWi hW0).2
240 
241 /-- The same weighted inequality holds on every conditioning-measurable event. -/
242 theorem setIntegral_weighted_factor_le (a : Ω → ℝ) (ha : Measurable[m] a)
243     (W : Ω → ℝ) (hW : Measurable[m] W) (hWi : Integrable W μ) (hW0 : ∀ ω,0≤W ω)
244     {s : Set Ω} (hs : MeasurableSet[m] s) :
245     (∫ ω in s,W ω*factor X σ a ω∂μ)≤∫ ω in s,W ω∂μ := by
246   have h0 (ω : Ω) : 0≤s.indicator W ω := by
247     by_cases hω : ω∈s <;> simp [hω,hW0]
248   have hbound := H.integral_weighted_factor_le a ha (s.indicator W)
249     (hW.indicator hs) (hWi.indicator (hm _ hs)) h0
250   have he : (fun ω => s.indicator W ω*factor X σ a ω)=
251       s.indicator (fun ω => W ω*factor X σ a ω) := by
252     funext ω
253     by_cases hω : ω∈s <;> simp [hω]
254   rw [he,integral_indicator (hm _ hs),integral_indicator (hm _ hs)] at hbound
255   exact hbound
256 
257 end ConditionalSubgaussian
258 end Komorebi.LSM.RegressionConfidence

Back to source controls