BoundedResponseNoise.lean

1 import KomorebiLSM.ConditionalHoeffding
2 import KomorebiLSM.PredictableResidualAffine
3 import KomorebiLSM.ConditionalRandomMultiplier
4 
5 /-! Conditional regression noise scales are derived from actual bounded
6 responses and their actual conditional means on arbitrary probability spaces. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.BoundedResponseNoise
9 open MeasureTheory ProbabilityTheory
10 open Komorebi.LSM.RegressionConfidence
11 
12 variable {Ω : Type*} [mΩ : MeasurableSpace Ω]
13 variable {μ : Measure Ω} [IsProbabilityMeasure μ]
14 
15 omit [IsProbabilityMeasure μ] in
16 /-- An actual a.e. identity transports the conditional exponential structure;
17 ambient measurability of the chosen version is retained explicitly. -/
18 theorem conditionalSubgaussian_congr {m : MeasurableSpace Ω} {hm : m≤mΩ}
19     {X Z : Ω → ℝ} {σ : ℝ} (H : ConditionalSubgaussian (mΩ := mΩ) hm X σ μ)
20     (hZ : @Measurable Ω ℝ mΩ _ Z) (hXZ : X=ᵐ[μ] Z) :
21     ConditionalSubgaussian (mΩ := mΩ) hm Z σ μ := by
22   let : MeasurableSpace Ω := mΩ
23   have he (h : ℝ) : (fun ω => Real.exp (h*X ω))=ᵐ[μ] (fun ω => Real.exp (h*Z ω)) := by
24     filter_upwards [hXZ] with ω hω
25     rw [hω]
26   refine ⟨hZ,fun h => (H.integrable_exp h).congr (he h),?_⟩
27   intro h
28   filter_upwards [H.condExp_le h,condExp_congr_ae (he h)] with ω hb hc
29   exact hc.symm.trans_le hb
30 
31 /-- Actual affine normalization and the sharp conditional unit Hoeffding
32 bound give the interval-width noise scale (b-a)/2. -/
33 theorem centered_interval {m : MeasurableSpace Ω} (hm : m≤mΩ)
34     (Y : Ω → ℝ) (hY : @Measurable Ω ℝ mΩ _ Y)
35     (a b : ℝ) (hab : a<b) (hb : ∀ᵐ ω∂μ,Y ω∈Set.Icc a b) :
36     ConditionalSubgaussian (mΩ := mΩ) hm (fun ω => Y ω-(μ[Y|m]) ω) ((b-a)/2) μ := by
37   let : MeasurableSpace Ω := mΩ
38   let c := b-a
39   have hc : 0<c := sub_pos.mpr hab
40   let U : Ω → ℝ := fun ω => (Y ω-a)/c
41   have hU : @Measurable Ω ℝ mΩ _ U := (hY.sub_const a).div_const c
42   have hunit : ∀ᵐ ω∂μ,U ω∈Set.Icc (0:ℝ) 1 := by
43     filter_upwards [hb] with ω hω
44     refine ⟨div_nonneg (sub_nonneg.mpr hω.1) hc.le,?_⟩
45     apply (div_le_iff₀ hc).2
46     dsimp [c]
47     linarith [hω.2]
48   have hi : Integrable U μ := Integrable.of_mem_Icc (0:ℝ) 1 hU.aemeasurable hunit
49   have hrep (ω : Ω) : a+c*U ω=Y ω := by
50     dsimp [U]
51     field_simp [ne_of_gt hc]
52     ring
53   have hce := PredictableResidualAffine.condExp_affine_ae hm U hi a c
54   rw [show (fun ω => a+c*U ω)=Y from funext hrep] at hce
55   have hcenter : (fun ω => Y ω-(μ[Y|m]) ω)=ᵐ[μ]
56       (fun ω => c*(U ω-(μ[U|m]) ω)) := by
57     filter_upwards [hce] with ω hω
58     rw [hω,← hrep ω]
59     ring
60   have hexp (h : ℝ) : (fun ω => Real.exp (h*(Y ω-(μ[Y|m]) ω)))=ᵐ[μ]
61       (fun ω => Real.exp ((h*c)*(U ω-(μ[U|m]) ω))) := by
62     filter_upwards [hcenter] with ω hω
63     rw [hω]
64     congr 1
65     ring
66   refine ⟨hY.sub (stronglyMeasurable_condExp.measurable.mono hm le_rfl),?_,?_⟩
67   · intro h
68     exact (ConditionalHoeffding.centered_exp_integrable hm U hU hunit (h*c)).congr (hexp h).symm
69   · intro h
70     have hbound := ConditionalHoeffding.centered_condExp_le hm U hU hunit (h*c)
71     have he := condExp_congr_ae (m := m) (hexp h)
72     have hscale : (h*c)^2/8=h^2*((b-a)/2)^2/2 := by dsimp [c]; ring
73     filter_upwards [hbound,he] with ω hω heω
74     rw [heω]
75     simpa only [hscale] using hω
76 
77 /-- A declared regression mean is used only after its actual conditional
78 expectation identity has been proved. No noise certificate is an input. -/
79 theorem regression_interval {m : MeasurableSpace Ω} (hm : m≤mΩ)
80     (Y : Ω → ℝ) (hY : @Measurable Ω ℝ mΩ _ Y)
81     (a b : ℝ) (hab : a<b) (hb : ∀ᵐ ω∂μ,Y ω∈Set.Icc a b)
82     (θ : ℝ) (φ : Ω → ℝ) (hφ : @Measurable Ω ℝ m _ φ)
83     (hmean : (μ[Y|m])=ᵐ[μ] (fun ω => θ*φ ω)) :
84     ConditionalSubgaussian (mΩ := mΩ) hm (fun ω => Y ω-θ*φ ω) ((b-a)/2) μ := by
85   let : MeasurableSpace Ω := mΩ
86   apply conditionalSubgaussian_congr (centered_interval hm Y hY a b hab hb)
87     (hY.sub ((hφ.mono hm le_rfl).const_mul θ))
88   filter_upwards [hmean] with ω hω
89   change Y ω-(μ[Y|m]) ω=Y ω-θ*φ ω
90   rw [hω]
91 
92 /-- A response in [-1,1] has the derived conditional noise scale one. -/
93 theorem regression_neg_one_one {m : MeasurableSpace Ω} (hm : m≤mΩ)
94     (Y : Ω → ℝ) (hY : @Measurable Ω ℝ mΩ _ Y)
95     (hb : ∀ᵐ ω∂μ,Y ω∈Set.Icc (-1:ℝ) 1)
96     (θ : ℝ) (φ : Ω → ℝ) (hφ : @Measurable Ω ℝ m _ φ)
97     (hmean : (μ[Y|m])=ᵐ[μ] (fun ω => θ*φ ω)) :
98     ConditionalSubgaussian (mΩ := mΩ) hm (fun ω => Y ω-θ*φ ω) 1 μ := by
99   let : MeasurableSpace Ω := mΩ
100   convert regression_interval hm Y hY (-1) 1 (by norm_num) hb θ φ hφ hmean using 1; norm_num
101 
102 /-- A response in [-1/2,1] has the derived conditional noise scale three quarters. -/
103 theorem regression_neg_half_one {m : MeasurableSpace Ω} (hm : m≤mΩ)
104     (Y : Ω → ℝ) (hY : @Measurable Ω ℝ mΩ _ Y)
105     (hb : ∀ᵐ ω∂μ,Y ω∈Set.Icc (-(1/2):ℝ) 1)
106     (θ : ℝ) (φ : Ω → ℝ) (hφ : @Measurable Ω ℝ m _ φ)
107     (hmean : (μ[Y|m])=ᵐ[μ] (fun ω => θ*φ ω)) :
108     ConditionalSubgaussian (mΩ := mΩ) hm (fun ω => Y ω-θ*φ ω) (3/4) μ := by
109   let : MeasurableSpace Ω := mΩ
110   convert regression_interval hm Y hY (-(1/2)) 1 (by norm_num) hb θ φ hφ hmean using 1; norm_num
111 
112 /-- Predictable scalar regressors and next-level recorded [-1,1] responses
113 supply P81's actual noise input with sigma=1 at every time. -/
114 theorem process_neg_one_one (ℱ : Filtration ℕ mΩ) (θ : ℝ)
115     (φ Y : ℕ → Ω → ℝ) (hφ : ∀ n,Measurable[ℱ n] (φ n))
116     (hY : ∀ n,Measurable[ℱ (n+1)] (Y n))
117     (hb : ∀ n,∀ᵐ ω∂μ,Y n ω∈Set.Icc (-1:ℝ) 1)
118     (hmean : ∀ n,(μ[Y n|ℱ n])=ᵐ[μ] (fun ω => θ*φ n ω)) :
119     ∀ n,ConditionalSubgaussian (mΩ := mΩ) (ℱ.le n) (fun ω => Y n ω-θ*φ n ω) 1 μ :=
120   fun n => regression_neg_one_one (ℱ.le n) (Y n) ((hY n).mono (ℱ.le (n+1)) le_rfl)
121     (hb n) θ (φ n) (hφ n) (hmean n)
122 
123 /-- The [-1/2,1] predictable regression analog supplies sigma=3/4. -/
124 theorem process_neg_half_one (ℱ : Filtration ℕ mΩ) (θ : ℝ)
125     (φ Y : ℕ → Ω → ℝ) (hφ : ∀ n,Measurable[ℱ n] (φ n))
126     (hY : ∀ n,Measurable[ℱ (n+1)] (Y n))
127     (hb : ∀ n,∀ᵐ ω∂μ,Y n ω∈Set.Icc (-(1/2):ℝ) 1)
128     (hmean : ∀ n,(μ[Y n|ℱ n])=ᵐ[μ] (fun ω => θ*φ n ω)) :
129     ∀ n,ConditionalSubgaussian (mΩ := mΩ) (ℱ.le n) (fun ω => Y n ω-θ*φ n ω) (3/4) μ :=
130   fun n => regression_neg_half_one (ℱ.le n) (Y n) ((hY n).mono (ℱ.le (n+1)) le_rfl)
131     (hb n) θ (φ n) (hφ n) (hmean n)
132 
133 end Komorebi.LSM.BoundedResponseNoise

Back to source controls