StructuredLearning.lean

1 import KomorebiLSM.ObservableMomentConditional
2 import KomorebiLSM.RationalRegressionConfidence
3 import KomorebiLSM.CurvedMomentMarkov
4 
5 /-! P87: the two predictable scalar regressions are derived from the literal
6 declared observation law before their common all-time coverage event is used.
7 The true parameters need not satisfy the sufficient diamond test at early
8 checkpoints. Their actual nonnegative conditional density is an explicit model
9 assumption, rather than a claimed consequence of one observed path. -/
10 set_option autoImplicit false
11 namespace Komorebi.LSM.CurvedMoment
12 open MeasureTheory ProbabilityTheory
13 open scoped ENNReal
14 noncomputable section
15 
16 namespace Reference
17 variable {ν : Measure ℝ} (R : Reference ν)
18 
19 /-- A globally declared true transition law. The sufficient rectangle test is
20 not assumed here: only the actual conditional density and its nonnegativity. -/
21 structure TrueKernel (_R : Reference ν) (a b : ℝ) where
22   kernel : Kernel Signal ℝ
23   markov : IsMarkovKernel kernel
24   density : ∀ s,kernel s=ν.withDensity
25     (fun u => ENNReal.ofReal (1+a*s*u+b*(s:ℝ)^2*legendre u))
26   nonnegative : ∀ s : Signal,∀ᵐ u∂ν,0≤1+a*s*u+b*(s:ℝ)^2*legendre u
27 
28 namespace TrueKernel
29 variable {R} {a b : ℝ} (K : R.TrueKernel a b)
30 
31 theorem integral (s : Signal) (g : ℝ → ℝ) :
32     (∫ u,g u∂K.kernel s)=∫ u,g u*likelihood a b u (curve s)∂ν := by
33   rw [K.density]
34   have hd : Measurable (fun u : ℝ =>
35       ENNReal.ofReal (1+a*(s:ℝ)*u+b*(s:ℝ)^2*legendre u)) := by
36     unfold legendre
37     fun_prop
38   rw [integral_withDensity_eq_integral_toReal_smul hd
39     (Filter.Eventually.of_forall (fun _ => ENNReal.ofReal_lt_top))]
40   apply integral_congr_ae
41   filter_upwards [K.nonnegative s] with u hu
42   rw [ENNReal.toReal_ofReal hu]
43   change (1+a*(s:ℝ)*u+b*(s:ℝ)^2*legendre u)*g u=g u*likelihood a b u (curve s)
44   simp [likelihood,curve]
45   ring
46 
47 theorem signal_mean (s : Signal) : (∫ u,u∂K.kernel s)=a/3*s := by
48   rw [K.integral,R.integral_signal_likelihood]
49   simp [curve]
50   ring
51 
52 theorem legendre_mean (s : Signal) : (∫ u,legendre u∂K.kernel s)=b/5*(s:ℝ)^2 := by
53   rw [K.integral,R.integral_legendre_likelihood]
54   simp [curve]
55   ring
56 
57 end TrueKernel
58 
59 section Process
60 variable {Ω H : Type*} [mΩ : MeasurableSpace Ω] [mH : MeasurableSpace H]
61 variable {μ : Measure Ω} [IsProbabilityMeasure μ] (F : Filtration ℕ mΩ)
62 variable {a b : ℝ} (K : R.TrueKernel a b)
63 
64 /-- The conditional law is recorded as an equality of actual joint measures.
65 Current and next scalar observations are accessible from the recorded history.
66 The filtration is exactly its declared history sigma algebra. -/
67 structure ObservableProcess where
68   history : ℕ → Ω → H
69   history_measurable : ∀ n,Measurable[F n] (history n)
70   history_sigma : ∀ n,F n=mH.comap (history n)
71   signal : ℕ → H → Signal
72   signal_measurable : ∀ n,Measurable (signal n)
73   observation : ℕ → Ω → Signal
74   observation_measurable : ∀ n,Measurable[F (n+1)] (observation n)
75   next_signal : ∀ n ω,signal (n+1) (history (n+1) ω)=observation n ω
76   joint : ∀ n,μ.map (fun ω => (history n ω,(observation n ω : ℝ)))=
77     (μ.map (history n)) ⊗ₘ (K.kernel.comap (signal n) (signal_measurable n))
78 
79 namespace ObservableProcess
80 variable {R F K} (P : R.ObservableProcess (H := H) (μ := μ) F K)
81 
82 def current (n : ℕ) (ω : Ω) : ℝ := P.signal n (P.history n ω)
83 def designA (n : ℕ) (ω : Ω) : ℝ := P.current n ω/3
84 def designB (n : ℕ) (ω : Ω) : ℝ := (P.current n ω)^2/5
85 def responseA (n : ℕ) (ω : Ω) : ℝ := P.observation n ω
86 def responseB (n : ℕ) (ω : Ω) : ℝ := legendre (P.responseA n ω)
87 
88 omit [IsProbabilityMeasure μ] in
89 theorem current_measurable (n : ℕ) : Measurable[F n] (P.current n) :=
90   measurable_subtype_coe.comp ((P.signal_measurable n).comp (P.history_measurable n))
91 
92 omit [IsProbabilityMeasure μ] in
93 theorem designA_measurable (n : ℕ) : Measurable[F n] (P.designA n) :=
94   (P.current_measurable n).div_const 3
95 
96 omit [IsProbabilityMeasure μ] in
97 theorem designB_measurable (n : ℕ) : Measurable[F n] (P.designB n) :=
98   ((P.current_measurable n).pow_const 2).div_const 5
99 
100 omit [IsProbabilityMeasure μ] in
101 theorem responseA_measurable (n : ℕ) : Measurable[F (n+1)] (P.responseA n) :=
102   measurable_subtype_coe.comp (P.observation_measurable n)
103 
104 omit [IsProbabilityMeasure μ] in
105 theorem responseB_measurable (n : ℕ) : Measurable[F (n+1)] (P.responseB n) := by
106   have hy := P.responseA_measurable n
107   unfold responseB legendre
108   exact (((hy.pow_const 2).const_mul 3).sub_const 1).div_const 2
109 
110 omit [IsProbabilityMeasure μ] in
111 theorem responseA_bounds (n : ℕ) (ω : Ω) : P.responseA n ω∈Set.Icc (-1:ℝ) 1 :=
112   (P.observation n ω).2
113 
114 omit [IsProbabilityMeasure μ] in
115 theorem responseB_bounds (n : ℕ) (ω : Ω) : P.responseB n ω∈Set.Icc (-(1/2):ℝ) 1 := by
116   have hu := P.responseA_bounds n ω
117   have hs : (P.responseA n ω)^2≤1 := (sq_le_one_iff_abs_le_one _).mpr (abs_le.mpr hu)
118   unfold responseB legendre
119   constructor <;> nlinarith [sq_nonneg (P.responseA n ω)]
120 
121 /-- Conditional means are consequences of the joint law, not input fields. -/
122 theorem responseA_condExp (n : ℕ) :
123     (μ[P.responseA n|F n])=ᵐ[μ] (fun ω => a*P.designA n ω) := by
124   let := K.markov
125   let κ := K.kernel.comap (P.signal n) (P.signal_measurable n)
126   have hh := (P.history_measurable n).mono (F.le n) le_rfl
127   have hy := (P.responseA_measurable n).mono (F.le (n+1)) le_rfl
128   have hi : Integrable (P.responseA n) μ :=
129     Integrable.of_mem_Icc (-1:ℝ) 1 hy.aemeasurable
130       (Filter.Eventually.of_forall (P.responseA_bounds n))
131   have hc := ObservableMoments.history_condExp (P.history n) (P.responseA n)
132     hh hy κ (P.joint n) (fun p : H × ℝ => p.2) measurable_snd hi
133   rw [← P.history_sigma n] at hc
134   filter_upwards [hc] with ω hω
135   rw [hω]
136   change (∫ u,u∂K.kernel (P.signal n (P.history n ω)))=a*P.designA n ω
137   rw [K.signal_mean]
138   unfold designA current
139   ring
140 
141 theorem responseB_condExp (n : ℕ) :
142     (μ[P.responseB n|F n])=ᵐ[μ] (fun ω => b*P.designB n ω) := by
143   let := K.markov
144   let κ := K.kernel.comap (P.signal n) (P.signal_measurable n)
145   have hh := (P.history_measurable n).mono (F.le n) le_rfl
146   have hy := (P.responseA_measurable n).mono (F.le (n+1)) le_rfl
147   have hm := (P.responseB_measurable n).mono (F.le (n+1)) le_rfl
148   have hi : Integrable (P.responseB n) μ :=
149     Integrable.of_mem_Icc (-(1/2):ℝ) 1 hm.aemeasurable
150       (Filter.Eventually.of_forall (P.responseB_bounds n))
151   have hg : Measurable (fun p : H × ℝ => legendre p.2) := by unfold legendre;fun_prop
152   have hc := ObservableMoments.history_condExp (P.history n) (P.responseA n)
153     hh hy κ (P.joint n) (fun p : H × ℝ => legendre p.2) hg hi
154   rw [← P.history_sigma n] at hc
155   filter_upwards [hc] with ω hω
156   change (μ[fun ω => legendre (P.responseA n ω)|F n]) ω=_
157   rw [hω]
158   change (∫ u,legendre u∂K.kernel (P.signal n (P.history n ω)))=b*P.designB n ω
159   rw [K.legendre_mean]
160   unfold designB current
161   ring
162 
163 /-- The actual prescribed regressions and rational outward arithmetic provide
164 one measurable event of probability at least 19/20 covering every finite time.
165 This endpoint assumes neither a confidence event nor a conditional mean. -/
166 theorem simultaneous_rational_coverage (endpointGrid : ℕ) (he : 0<endpointGrid)
167     (ha : |a|≤1) (hb : |b|≤1) :
168     let G := RegressionConfidence.scalarGood 1 (1/40) P.designA P.responseA a∩
169       RegressionConfidence.scalarGood (3/4) (1/40) P.designB P.responseB b
170     MeasurableSet G ∧ (19/20:ℝ)≤μ.real G ∧ ∀ ω∈G,∀ n,
171       a∈Set.Icc
172         (RationalRegressionConfidence.lower (10^12) endpointGrid 1 (1/40) P.designA P.responseA n ω:ℝ)
173         (RationalRegressionConfidence.upper (10^12) endpointGrid 1 (1/40) P.designA P.responseA n ω:ℝ) ∧
174       b∈Set.Icc
175         (RationalRegressionConfidence.lower (10^12) endpointGrid (3/4) (1/40) P.designB P.responseB n ω:ℝ)
176         (RationalRegressionConfidence.upper (10^12) endpointGrid (3/4) (1/40) P.designB P.responseB n ω:ℝ) := by
177   exact RationalRegressionConfidence.two_regression_outer_certificate F endpointGrid he
178     P.designA P.responseA P.designB P.responseB a b
179     P.designA_measurable P.responseA_measurable P.designB_measurable P.responseB_measurable
180     (fun n => Filter.Eventually.of_forall (P.responseA_bounds n))
181     (fun n => Filter.Eventually.of_forall (P.responseB_bounds n))
182     P.responseA_condExp P.responseB_condExp ha hb
183 
184 end ObservableProcess
185 end Process
186 end Reference
187 end
188 end Komorebi.LSM.CurvedMoment

Back to source controls