CurvedMomentRecordTV.lean

1 import KomorebiLSM.CurvedMomentTV
2 import KomorebiLSM.ObservationLawComparison
3 import KomorebiLSM.MarkovMinorization
4 import Mathlib.Tactic
5 
6 /-! Completed observable history kernels and their exact P52 operator-product
7 law. Completion preserves every interval signal, including model-null histories. -/
8 set_option autoImplicit false
9 namespace Komorebi.LSM.CurvedMoment
10 open MeasureTheory ProbabilityTheory
11 open scoped ENNReal
12 noncomputable section
13 
14 /-- Only observations outside the declared support use a fallback. -/
15 def observedSignal (u : ℝ) : Signal :=
16   ⟨if u∈Set.Icc (-1:ℝ) 1 then u else 0,by
17     split_ifs with hu
18     · exact hu
19     · norm_num⟩
20 
21 theorem observedSignal_eq {u : ℝ} (hu : u∈Set.Icc (-1:ℝ) 1) :
22     (observedSignal u : ℝ)=u := by simp [observedSignal,hu]
23 
24 theorem observedSignal_measurable : Measurable observedSignal := by
25   apply Measurable.subtype_mk
26   exact measurable_id.ite measurableSet_Icc measurable_const
27 
28 def currentSignal (s : Signal) : (n : ℕ) → ContinuousRecords.History ℝ n → Signal
29   | 0,_ => s
30   | _+1,h => observedSignal h.2
31 
32 theorem currentSignal_measurable (s : Signal) :
33     (n : ℕ) → Measurable (currentSignal s n)
34   | 0 => measurable_const
35   | _+1 => observedSignal_measurable.comp measurable_snd
36 
37 namespace Reference
38 variable {μ : Measure ℝ} (R : Reference μ)
39 
40 def completedKernel (a b ρ : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ) : Kernel ℝ ℝ :=
41   (R.signalKernel a b ρ hρ hab).comap observedSignal observedSignal_measurable
42 
43 instance completedKernel_markov (a b ρ : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ) :
44     IsMarkovKernel (R.completedKernel a b ρ hρ hab) := by unfold completedKernel;infer_instance
45 
46 theorem completedKernel_on_interval (a b ρ : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ)
47     (u : ℝ) (hu : u∈Set.Icc (-1:ℝ) 1) :
48     R.completedKernel a b ρ hρ hab u=R.signalKernel a b ρ hρ hab ⟨u,hu⟩ := by
49   change R.signalKernel a b ρ hρ hab (observedSignal u)=_
50   congr 1
51   exact Subtype.ext (observedSignal_eq hu)
52 
53 def futureKernel (a b ρ : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ) (s : Signal) (n : ℕ) :
54     Kernel (ContinuousRecords.History ℝ n) ℝ :=
55   (R.signalKernel a b ρ hρ hab).comap (currentSignal s n) (currentSignal_measurable s n)
56 
57 instance futureKernel_markov (a b ρ : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ) (s : Signal) (n : ℕ) :
58     IsMarkovKernel (R.futureKernel a b ρ hρ hab s n) := by unfold futureKernel;infer_instance
59 
60 /-- The literal chronological law of the globally completed observation kernels. -/
61 def futureLaw (a b ρ : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ) (s : Signal) :
62     (n : ℕ) → Measure (ContinuousRecords.History ℝ n)
63   | 0 => Measure.dirac PUnit.unit
64   | n+1 => futureLaw a b ρ hρ hab s n ⊗ₘ R.futureKernel a b ρ hρ hab s n
65 
66 instance futureLaw_probability (a b ρ : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ) (s : Signal) :
67     (n : ℕ) → IsProbabilityMeasure (R.futureLaw a b ρ hρ hab s n)
68   | 0 => inferInstanceAs (IsProbabilityMeasure (Measure.dirac PUnit.unit))
69   | n+1 => by
70     let := futureLaw_probability a b ρ hρ hab s n
71     exact inferInstanceAs (IsProbabilityMeasure
72       (R.futureLaw a b ρ hρ hab s n ⊗ₘ R.futureKernel a b ρ hρ hab s n))
73 
74 /-- This is exact even on zero-mass and signed histories. No normalized
75 posterior identity on null branches is used. -/
76 theorem observationRun_rank_one (a b ρ : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ)
77     (z : State) (n : ℕ) (h : ContinuousRecords.History ℝ (n+1)) :
78     ContinuousRecords.observationRun (R.instrument a b ρ hρ hab) (fun _ => ()) z (n+1) h=
79       mass (ContinuousRecords.observationRun (R.instrument a b ρ hρ hab) (fun _ => ()) z (n+1) h) • curve h.2 := by
80   change branch a b h.2 _=mass (branch a b h.2 _) • curve h.2
81   rw [branch_mass,branch_apply]
82 
83 theorem observationRun_mass_factor (a b ρ : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ)
84     (s : Signal) : ∀ n,∀ᵐ h∂ContinuousRecords.reference μ n,∀ u,
85       mass (ContinuousRecords.observationRun (R.instrument a b ρ hρ hab) (fun _ => ())
86         (curve s) (n+1) (h,u))=
87       mass (ContinuousRecords.observationRun (R.instrument a b ρ hρ hab) (fun _ => ())
88         (curve s) n h)*likelihood a b u (curve (currentSignal s n h)) := by
89   let := R.probability
90   intro n
91   cases n with
92   | zero =>
93     apply Filter.Eventually.of_forall
94     intro h u
95     change mass (branch a b u (curve s))=mass (curve s)*likelihood a b u (curve s)
96     rw [branch_mass]
97     simp [mass,curve]
98   | succ n =>
99     have hs : ∀ᵐ h∂ContinuousRecords.reference μ (n+1),h.2∈Set.Icc (-1:ℝ) 1 := by
100       apply (Measure.ae_prod_iff_ae_ae (measurableSet_Icc.preimage measurable_snd)).mpr
101       exact Filter.Eventually.of_forall (fun _ => R.support)
102     filter_upwards [hs] with h hv u
103     obtain ⟨h,v⟩ := h
104     change mass (branch a b u _)=_
105     rw [observationRun_rank_one,map_smul,map_smul,branch_mass]
106     simp only [smul_eq_mul]
107     simp [currentSignal,mass_apply,curve,observedSignal_eq hv]
108 
109 /-- The actual P52 operator-density law equals the completed-kernel law.
110 In particular, model-null interval histories keep the observed curve state. -/
111 theorem observationLaw_eq_futureLaw (a b ρ : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ)
112     (s : Signal) : ∀ n,
113     ContinuousRecords.observationLaw (R.instrument a b ρ hρ hab) (fun _ => ()) (curve s) n=
114       R.futureLaw a b ρ hρ hab s n := by
115   let := R.probability
116   let D := R.instrument a b ρ hρ hab
117   intro n
118   induction n with
119   | zero =>
120     change (Measure.dirac PUnit.unit).withDensity (fun _ => ENNReal.ofReal (mass (curve s)))=
121       Measure.dirac PUnit.unit
122     norm_num [mass,curve]
123   | succ n ih =>
124     let k : ContinuousRecords.History ℝ n → ℝ → ℝ≥0∞ := fun h u =>
125       ENNReal.ofReal (likelihood a b u (curve (currentSignal s n h)))
126     have hk : Measurable (Function.uncurry k) := by
127       unfold k likelihood legendre curve
128       have hs : Measurable (fun p : ContinuousRecords.History ℝ n × ℝ =>
129           (currentSignal s n p.1 : ℝ)) :=
130         (measurable_subtype_coe.comp (currentSignal_measurable s n)).comp measurable_fst
131       fun_prop
132     have hkernel : R.futureKernel a b ρ hρ hab s n=
133         (Kernel.const _ μ).withDensity k := by
134       apply Kernel.ext
135       intro h
136       rw [Kernel.withDensity_apply _ hk]
137       change R.signalKernel a b ρ hρ hab (currentSignal s n h)=μ.withDensity (k h)
138       rw [R.signalKernel_apply]
139       congr 1
140       funext u
141       change ENNReal.ofReal (1+a*(currentSignal s n h:ℝ)*u+
142         b*(currentSignal s n h:ℝ)^2*legendre u)=
143           ENNReal.ofReal (1+a*u*(currentSignal s n h:ℝ)+
144             b*legendre u*(currentSignal s n h:ℝ)^2)
145       congr 1
146       ring
147     have : IsMarkovKernel ((Kernel.const (ContinuousRecords.History ℝ n) μ).withDensity k) := by
148       rw [←hkernel]
149       infer_instance
150     rw [futureLaw,← ih,hkernel]
151     simp only [ContinuousRecords.observationLaw]
152     rw [
153       Measure.withDensity_compProd_withDensity (ContinuousRecords.observationDensity_measurable D _ _ n) hk,
154       Measure.compProd_const]
155     change (ContinuousRecords.reference μ (n+1)).withDensity _=
156       (ContinuousRecords.reference μ (n+1)).withDensity _
157     apply withDensity_congr_ae
158     have hmleft := ContinuousRecords.observationDensity_measurable D (fun _ => ()) (curve s) (n+1)
159     have hmright := ((ContinuousRecords.observationDensity_measurable D (fun _ => ()) (curve s) n).comp
160       (measurable_fst : Measurable (Prod.fst : ContinuousRecords.History ℝ n × ℝ → _))).mul hk
161     apply (Measure.ae_prod_iff_ae_ae (measurableSet_eq_fun hmleft hmright)).mpr
162     filter_upwards [R.observationRun_mass_factor a b ρ hρ hab s n,
163       ContinuousRecords.observationRun_mem_ae D (fun _ => ()) (curve_mem s s.2) n] with h hh hc
164     apply Filter.Eventually.of_forall
165     intro u
166     change ENNReal.ofReal (mass _)=ENNReal.ofReal (mass _)*ENNReal.ofReal (likelihood a b u (curve (currentSignal s n h)))
167     rw [hh u]
168     have hm : 0≤mass (ContinuousRecords.observationRun (R.instrument a b ρ hρ hab)
169         (fun _ => ()) (curve s) n h) := probabilityCone.mass_nonneg hc
170     exact ENNReal.ofReal_mul hm
171 
172 /-- Full future observation records telescope the genuine conditional kernel
173 error; no coordinate-state estimation error is accumulated. -/
174 theorem futureLaw_lawTV_le (a b ρ a' b' ρ' da db : ℝ)
175     (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ) (hρ' : 0≤ρ') (hab' : |a'|+|b'|≤1-ρ')
176     (ha : |a-a'|≤da) (hb : |b-b'|≤db) (s : Signal) (T : ℕ) :
177     SequentialLowerCertificate.lawTV (R.futureLaw a b ρ hρ hab s T)
178       (R.futureLaw a' b' ρ' hρ' hab' s T)≤min 1 ((T:ℝ)*R.parameterBudget da db) := by
179   apply le_min (SequentialLowerCertificate.lawTV_le_one _ _)
180   induction T with
181   | zero => simp [futureLaw,SequentialLowerCertificate.lawTV_self]
182   | succ n ih =>
183     have hu := MarkovStability.compProd_uniform_change
184       (R.futureLaw a b ρ hρ hab s n) (R.futureKernel a b ρ hρ hab s n)
185       (R.futureKernel a' b' ρ' hρ' hab' s n) (R.parameterBudget da db)
186       (fun h => R.signalKernel_lawTV_le a b ρ a' b' ρ' da db hρ hab hρ' hab' ha hb (currentSignal s n h))
187     have hc := MeasureTVCalculus.lawTV_compProd (R.futureLaw a b ρ hρ hab s n)
188       (R.futureLaw a' b' ρ' hρ' hab' s n) (R.futureKernel a' b' ρ' hρ' hab' s n)
189     have ht := MeasureTVCalculus.lawTV_triangle
190       (R.futureLaw a b ρ hρ hab s n ⊗ₘ R.futureKernel a b ρ hρ hab s n)
191       (R.futureLaw a b ρ hρ hab s n ⊗ₘ R.futureKernel a' b' ρ' hρ' hab' s n)
192       (R.futureLaw a' b' ρ' hρ' hab' s n ⊗ₘ R.futureKernel a' b' ρ' hρ' hab' s n)
193     change SequentialLowerCertificate.lawTV (_ ⊗ₘ _) (_ ⊗ₘ _)≤_
194     have he := ht.trans (add_le_add hu hc)
195     push_cast
196     linarith
197 
198 instance observationLaw_curve_probability (a b ρ : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ)
199     (s : Signal) (T : ℕ) : IsProbabilityMeasure
200       (ContinuousRecords.observationLaw (R.instrument a b ρ hρ hab) (fun _ => ()) (curve s) T) := by
201   let := R.probability
202   exact ContinuousRecords.observationLaw_probability _ _ (curveState s) T
203 
204 /-- The complete future records are the actual P52 operator-product measures. -/
205 theorem observationLaw_lawTV_le (a b ρ a' b' ρ' da db : ℝ)
206     (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ) (hρ' : 0≤ρ') (hab' : |a'|+|b'|≤1-ρ')
207     (ha : |a-a'|≤da) (hb : |b-b'|≤db) (s : Signal) (T : ℕ) :
208     SequentialLowerCertificate.lawTV
209       (ContinuousRecords.observationLaw (R.instrument a b ρ hρ hab) (fun _ => ()) (curve s) T)
210       (ContinuousRecords.observationLaw (R.instrument a' b' ρ' hρ' hab') (fun _ => ()) (curve s) T)
211       ≤min 1 ((T:ℝ)*R.parameterBudget da db) := by
212   simpa only [R.observationLaw_eq_futureLaw] using
213     R.futureLaw_lawTV_le a b ρ a' b' ρ' da db hρ hab hρ' hab' ha hb s T
214 
215 end Reference
216 end
217 end Komorebi.LSM.CurvedMoment

Back to source controls