CurvedMomentMarkov.lean

1 import KomorebiLSM.CurvedMomentPolynomial
2 import Mathlib.Probability.Kernel.Composition.MapComap
3 import Mathlib.Tactic
4 
5 /-! The observable Markov kernel is defined at every signal in [-1,1].
6 Its conditional moments are integrals against the actual probability kernel. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.CurvedMoment
9 open MeasureTheory ProbabilityTheory
10 open scoped ENNReal
11 noncomputable section
12 
13 abbrev Signal := {s : ℝ // s∈Set.Icc (-1:ℝ) 1}
14 
15 def curveState (s : Signal) : ContinuousInstrument.DensityInstrument.State probabilityCone :=
16   ⟨curve s,curve_mem s s.2,rfl⟩
17 
18 theorem curveState_measurable : Measurable curveState := by
19   apply Measurable.subtype_mk
20   have hc : Continuous curve := by unfold curve; fun_prop
21   exact hc.measurable.comp measurable_subtype_coe
22 
23 namespace Reference
24 variable {μ : Measure ℝ} (R : Reference μ)
25 include R
26 
27 def signalKernel (a b ρ : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ) : Kernel Signal ℝ := by
28   letI := R.probability
29   exact ((R.instrument a b ρ hρ hab).kernel ()).comap curveState curveState_measurable
30 
31 instance signalKernel_markov (a b ρ : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ) :
32     IsMarkovKernel (R.signalKernel a b ρ hρ hab) := by
33   let := R.probability
34   unfold signalKernel
35   infer_instance
36 
37 theorem instrument_density (a b ρ u : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ) (z : State) :
38     (R.instrument a b ρ hρ hab).density () u z=likelihood a b u z := branch_mass a b u z
39 
40 theorem signalKernel_apply (a b ρ : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ) (s : Signal) :
41     R.signalKernel a b ρ hρ hab s=μ.withDensity
42       (fun u => ENNReal.ofReal (1+a*s*u+b*(s:ℝ)^2*legendre u)) := by
43   let := R.probability
44   change (R.instrument a b ρ hρ hab).kernel () (curveState s)=_
45   rw [ContinuousInstrument.DensityInstrument.kernel_apply]
46   congr 1
47   funext u
48   rw [R.instrument_density]
49   congr 1
50   change 1+a*u*(s:ℝ)+b*legendre u*(s:ℝ)^2=1+a*(s:ℝ)*u+b*(s:ℝ)^2*legendre u
51   ring
52 
53 theorem signalKernel_support (a b ρ : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ)
54     (s : Signal) : ∀ᵐ u∂R.signalKernel a b ρ hρ hab s,u∈Set.Icc (-1:ℝ) 1 := by
55   rw [R.signalKernel_apply]
56   exact (withDensity_absolutelyContinuous _ _).ae_le R.support
57 
58 theorem signalKernel_continuous_integrable (a b ρ : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ)
59     (s : Signal) {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
60     {f : ℝ→F} (hf : Continuous f) : Integrable f (R.signalKernel a b ρ hρ hab s) := by
61   have he : (R.signalKernel a b ρ hρ hab s).restrict (Set.Icc (-1:ℝ) 1)=
62       R.signalKernel a b ρ hρ hab s := Measure.restrict_eq_self_of_ae_mem (R.signalKernel_support a b ρ hρ hab s)
63   have hi : IntegrableOn f (Set.Icc (-1:ℝ) 1) (R.signalKernel a b ρ hρ hab s) :=
64     hf.continuousOn.integrableOn_compact isCompact_Icc
65   simpa only [IntegrableOn,he] using hi
66 
67 theorem density_lower (a b ρ u : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ)
68     (hu : u∈Set.Icc (-1:ℝ) 1) (z : ContinuousInstrument.DensityInstrument.State probabilityCone) :
69     ρ≤(R.instrument a b ρ hρ hab).density () u z.1 := by
70   rw [R.instrument_density]
71   exact likelihood_lower a b ρ u hρ hab hu (by rw [←base_eq_normalized];exact z.2)
72 
73 /-- Actual conditional expectations from the declared transition law. -/
74 theorem signalKernel_integral (a b ρ : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ)
75     (s : Signal) (g : ℝ→ℝ) :
76     (∫ u,g u∂R.signalKernel a b ρ hρ hab s)=
77       ∫ u,g u*likelihood a b u (curve s)∂μ := by
78   let := R.probability
79   let D := R.instrument a b ρ hρ hab
80   have hd : Measurable (fun u => ENNReal.ofReal (D.density () u (curve s))) :=
81     ((D.density_measurable ()).comp (measurable_const.prodMk measurable_id)).ennreal_ofReal
82   change (∫ u,g u∂D.kernel () (curveState s))=_
83   rw [D.kernel_apply]
84   change (∫ u,g u∂μ.withDensity (fun u => ENNReal.ofReal (D.density () u (curve s))))=_
85   rw [integral_withDensity_eq_integral_toReal_smul hd
86     (Filter.Eventually.of_forall (fun _ => ENNReal.ofReal_lt_top))]
87   apply integral_congr_ae
88   filter_upwards [D.density_nonneg_ae () (curve_mem s s.2)] with u hu
89   rw [ENNReal.toReal_ofReal hu]
90   change (R.instrument a b ρ hρ hab).density () u (curve s)*g u=g u*likelihood a b u (curve s)
91   rw [R.instrument_density]
92   ring
93 
94 theorem conditional_signal_mean (a b ρ : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ)
95     (s : Signal) : (∫ u,u∂R.signalKernel a b ρ hρ hab s)=a/3*s := by
96   rw [R.signalKernel_integral,R.integral_signal_likelihood]
97   simp [curve]
98   ring
99 
100 theorem conditional_legendre_mean (a b ρ : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ)
101     (s : Signal) : (∫ u,legendre u∂R.signalKernel a b ρ hρ hab s)=b/5*(s:ℝ)^2 := by
102   rw [R.signalKernel_integral,R.integral_legendre_likelihood]
103   simp [curve]
104   ring
105 
106 theorem update_curve_ae (a b ρ : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ)
107     (fallback z : ContinuousInstrument.DensityInstrument.State probabilityCone) :
108     ∀ᵐ u∂μ,0<likelihood a b u z.1 →
109       ((R.instrument a b ρ hρ hab).update fallback () z u).1=curve u := by
110   let D := R.instrument a b ρ hρ hab
111   filter_upwards [D.update_eq_ae fallback () z] with u hu hp
112   have hdp : 0<D.density () u z.1 := by
113     change 0<(R.instrument a b ρ hρ hab).density () u z.1
114     rwa [R.instrument_density]
115   change (D.update fallback () z u).1=_
116   rw [hu hdp]
117   change (mass (branch a b u z.1))⁻¹ • branch a b u z.1=_
118   exact posterior_curve a b u z.1 hp
119 
120 /-- Every branch with positive probability resets to the observed moment ray;
121 zero-density branches contribute no mass to this almost-everywhere statement. -/
122 theorem update_curve_kernel_ae [IsProbabilityMeasure μ] (a b ρ : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ)
123     (fallback z : ContinuousInstrument.DensityInstrument.State probabilityCone) :
124     ∀ᵐ u∂(R.instrument a b ρ hρ hab).kernel () z,
125       ((R.instrument a b ρ hρ hab).update fallback () z u).1=curve u := by
126   let := R.probability
127   let D := R.instrument a b ρ hρ hab
128   have hd : Measurable (fun u => ENNReal.ofReal (D.density () u z.1)) :=
129     ((D.density_measurable ()).comp (measurable_const.prodMk measurable_id)).ennreal_ofReal
130   rw [D.kernel_apply,ae_withDensity_iff hd]
131   filter_upwards [R.update_curve_ae a b ρ hρ hab fallback z] with u hu hn
132   apply hu
133   have hp : 0<D.density () u z.1 := ENNReal.ofReal_ne_zero_iff.mp hn
134   rwa [R.instrument_density] at hp
135 
136 /-- The next transition is the globally specified observable signal kernel,
137 including for a prior signal whose history has probability zero. -/
138 theorem observable_markov_transition [IsProbabilityMeasure μ] (a b ρ : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ)
139     (fallback z : ContinuousInstrument.DensityInstrument.State probabilityCone) :
140     ∀ᵐ u∂(R.instrument a b ρ hρ hab).kernel () z,
141       ∃ hu : u∈Set.Icc (-1:ℝ) 1,
142         (R.instrument a b ρ hρ hab).kernel ()
143           ((R.instrument a b ρ hρ hab).update fallback () z u)=R.signalKernel a b ρ hρ hab ⟨u,hu⟩ := by
144   let := R.probability
145   let D := R.instrument a b ρ hρ hab
146   have hs : ∀ᵐ u∂D.kernel () z,u∈Set.Icc (-1:ℝ) 1 := by
147     rw [D.kernel_apply]
148     exact (withDensity_absolutelyContinuous _ _).ae_le R.support
149   filter_upwards [R.update_curve_kernel_ae a b ρ hρ hab fallback z,hs] with u hu hs
150   refine ⟨hs,?_⟩
151   change D.kernel () (D.update fallback () z u)=D.kernel () (curveState ⟨u,hs⟩)
152   congr 1
153   exact Subtype.ext hu
154 
155 /-- The exact same operator density defines normalized laws at every finite horizon. -/
156 theorem record_probability (a b ρ : ℝ) (hρ : 0≤ρ) (hab : |a|+|b|≤1-ρ)
157     (π : ContinuousRecords.Policy (A:=Unit) (Y:=ℝ))
158     (z : ContinuousInstrument.DensityInstrument.State probabilityCone) (n : ℕ) :
159     IsProbabilityMeasure (ContinuousRecords.recordLaw (R.instrument a b ρ hρ hab) π z.1 n) := by
160   let := R.probability
161   exact ContinuousRecords.recordLaw_probability _ π z n
162 
163 end Reference
164 end
165 end Komorebi.LSM.CurvedMoment

Back to source controls