ContinuousInstrument.lean

1 import KomorebiLSM.BaseNorm
2 import Mathlib.Probability.Kernel.WithDensity
3 import Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
4 import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
5 import Mathlib.MeasureTheory.Integral.Bochner.Set
6 import Mathlib.MeasureTheory.Measure.Real
7 
8 /-! P52: continuous observation densities are actual operator-valued Bochner
9 integrals. Probability kernels and normalized updates are derived from these
10 operators, whole-cone positivity almost everywhere, and exact integrated mass. -/
11 set_option autoImplicit false
12 namespace Komorebi.LSM.ContinuousInstrument
13 open MeasureTheory ProbabilityTheory
14 open scoped ENNReal
15 variable {E A Y : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
16 variable [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
17 variable [MeasurableSpace Y]
18 
19 noncomputable def massCLM (C : BaseNorm.ProbabilityCone E) : E →L[ℝ] ℝ :=
20   C.mass.toContinuousLinearMap
21 
22 /-- Input assumptions concern the literal operator density. In particular,
23 positivity holds on the entire cone outside one null set per action. -/
24 structure DensityInstrument (C : BaseNorm.ProbabilityCone E) (μ : Measure Y) where
25   op : A → Y → E →L[ℝ] E
26   measurable_op : ∀ a,Measurable (op a)
27   integrable_op : ∀ a,Integrable (op a) μ
28   positive : ∀ a,∀ᵐ y∂μ,∀ z∈C.carrier,op a y z∈C.carrier
29   mass_preserving : ∀ a z,C.mass ((∫ y,op a y∂μ) z)=C.mass z
30 
31 namespace DensityInstrument
32 variable {C : BaseNorm.ProbabilityCone E} {μ : Measure Y}
33 variable (D : DensityInstrument (A := A) C μ)
34 
35 noncomputable def density (a : A) (y : Y) (z : E) : ℝ := C.mass (D.op a y z)
36 
37 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] in
38 theorem applied_integrable (a : A) (z : E) : Integrable (fun y => D.op a y z) μ :=
39   (ContinuousLinearMap.apply ℝ E z).integrable_comp (D.integrable_op a)
40 
41 omit [MeasurableSpace E] [BorelSpace E] in
42 theorem density_integrable (a : A) (z : E) : Integrable (fun y => D.density a y z) μ :=
43   (massCLM C).integrable_comp (D.applied_integrable a z)
44 
45 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] in
46 theorem density_nonneg_ae (a : A) {z : E} (hz : z∈C.carrier) :
47     0≤ᵐ[μ] (fun y => D.density a y z) := by
48   filter_upwards [D.positive a] with y hy
49   exact C.mass_nonneg (hy z hz)
50 
51 omit [MeasurableSpace E] [BorelSpace E] in
52 theorem integral_density (a : A) (z : E) : (∫ y,D.density a y z∂μ)=C.mass z := by
53   change (∫ y,massCLM C (D.op a y z)∂μ)=C.mass z
54   rw [(massCLM C).integral_comp_comm (D.applied_integrable a z)]
55   rw [← ContinuousLinearMap.integral_apply (D.integrable_op a) z]
56   exact D.mass_preserving a z
57 
58 theorem density_measurable (a : A) :
59     Measurable (fun p : E × Y => D.density a p.2 p.1) := by
60   change Measurable (fun p : E × Y => massCLM C (D.op a p.2 p.1))
61   apply (massCLM C).continuous.measurable.comp
62   exact (isBoundedBilinearMap_apply (𝕜 := ℝ) (E := E) (F := E)).continuous.measurable.comp
63     (((D.measurable_op a).comp measurable_snd).prodMk measurable_fst)
64 
65 /-- The normalized state space carries the induced measurable structure. -/
66 abbrev State (C : BaseNorm.ProbabilityCone E) := {z : E // z∈C.base}
67 
68 noncomputable def kernel [IsProbabilityMeasure μ] (a : A) : Kernel (State C) Y :=
69   (Kernel.const (State C) μ).withDensity (fun z y => ENNReal.ofReal (D.density a y z.1))
70 
71 theorem kernel_density_measurable (a : A) :
72     Measurable (Function.uncurry (fun (z : State C) y => ENNReal.ofReal (D.density a y z.1))) := by
73   exact (D.density_measurable a |>.comp (measurable_subtype_coe.prodMap measurable_id)).ennreal_ofReal
74 
75 theorem kernel_apply [IsProbabilityMeasure μ] (a : A) (z : State C) :
76     D.kernel a z=μ.withDensity (fun y => ENNReal.ofReal (D.density a y z.1)) :=
77   Kernel.withDensity_apply _ (D.kernel_density_measurable a) z
78 
79 instance kernel_markov [IsProbabilityMeasure μ] (a : A) : IsMarkovKernel (D.kernel a) := by
80   constructor
81   intro z
82   constructor
83   rw [D.kernel_apply a z,withDensity_apply _ MeasurableSet.univ,Measure.restrict_univ,
84     ← ofReal_integral_eq_lintegral_ofReal (D.density_integrable a z.1)
85       (D.density_nonneg_ae a z.2.1),D.integral_density a z.1,z.2.2]
86   exact ENNReal.ofReal_one
87 
88 
89 theorem kernel_event_real [IsProbabilityMeasure μ] (a : A) (z : State C)
90     (S : Set Y) (hS : MeasurableSet S) :
91     (D.kernel a z).real S=∫ y in S,D.density a y z.1∂μ := by
92   rw [Measure.real,D.kernel_apply a z,withDensity_apply _ hS,
93     ← ofReal_integral_eq_lintegral_ofReal (D.density_integrable a z.1).integrableOn
94       ((D.density_nonneg_ae a z.2.1).filter_mono (ae_mono Measure.restrict_le_self)),
95     ENNReal.toReal_ofReal]
96   exact integral_nonneg_of_ae ((D.density_nonneg_ae a z.2.1).filter_mono
97     (ae_mono Measure.restrict_le_self))
98 
99 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] in
100 /-- A measurable common exceptional set is extracted from the whole-cone
101 almost-everywhere hypothesis, without presuming that an uncountable
102 intersection of measurable sets is measurable. -/
103 theorem exists_exceptional (a : A) : ∃ N : Set Y,MeasurableSet N ∧ μ N=0 ∧
104     ∀ y∉N,∀ z∈C.carrier,D.op a y z∈C.carrier := by
105   have hb : μ {y | ¬∀ z∈C.carrier,D.op a y z∈C.carrier}=0 := ae_iff.mp (D.positive a)
106   obtain ⟨N,hsub,hm,hnull⟩ := exists_measurable_superset_of_null hb
107   refine ⟨N,hm,hnull,?_⟩
108   intro y hy
109   by_contra hn
110   exact hy (hsub hn)
111 
112 noncomputable def exceptional (a : A) : Set Y := (D.exists_exceptional a).choose
113 
114 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] in
115 theorem exceptional_measurable (a : A) : MeasurableSet (D.exceptional a) :=
116   (D.exists_exceptional a).choose_spec.1
117 
118 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] in
119 theorem exceptional_null (a : A) : μ (D.exceptional a)=0 :=
120   (D.exists_exceptional a).choose_spec.2.1
121 
122 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] in
123 theorem positive_off_exceptional (a : A) (y : Y) (hy : y∉D.exceptional a)
124     {z : E} (hz : z∈C.carrier) : D.op a y z∈C.carrier :=
125   (D.exists_exceptional a).choose_spec.2.2 y hy z hz
126 
127 noncomputable def updateValue (fallback : State C) (a : A) (z : State C) (y : Y) : E := by
128   classical
129   exact if y∉D.exceptional a ∧ 0<D.density a y z.1 then
130     (D.density a y z.1)⁻¹ • D.op a y z.1 else fallback.1
131 
132 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] in
133 theorem updateValue_mem (fallback : State C) (a : A) (z : State C) (y : Y) :
134     D.updateValue fallback a z y∈C.base := by
135   classical
136   unfold updateValue
137   split_ifs with h
138   · refine ⟨C.smul_mem (inv_nonneg.mpr h.2.le)
139       (D.positive_off_exceptional a y h.1 z.2.1),?_⟩
140     rw [map_smul,smul_eq_mul]
141     exact inv_mul_cancel₀ h.2.ne'
142   · exact fallback.2
143 
144 /-- A fixed valid state fills null-set and zero-density branches. -/
145 noncomputable def update (fallback : State C) (a : A) (z : State C) (y : Y) : State C :=
146   ⟨D.updateValue fallback a z y,D.updateValue_mem fallback a z y⟩
147 
148 theorem update_measurable (fallback : State C) (a : A) :
149     Measurable (Function.uncurry (D.update fallback a)) := by
150   have hd : Measurable (fun p : State C × Y => D.density a p.2 p.1.1) :=
151     (D.density_measurable a).comp (measurable_subtype_coe.prodMap measurable_id)
152   have hp : Measurable (fun p : State C × Y => D.op a p.2 p.1.1) :=
153     (isBoundedBilinearMap_apply (𝕜 := ℝ) (E := E) (F := E)).continuous.measurable.comp
154       (((D.measurable_op a).comp measurable_snd).prodMk
155         (measurable_subtype_coe.comp measurable_fst))
156   have hg : MeasurableSet {p : State C × Y | p.2∉D.exceptional a ∧ 0<D.density a p.2 p.1.1} :=
157     ((D.exceptional_measurable a).compl.preimage measurable_snd).inter
158       (measurableSet_lt measurable_const hd)
159   have hm : Measurable (fun p : State C × Y => D.updateValue fallback a p.1 p.2) :=
160     (hd.inv.smul hp).ite hg measurable_const
161   exact hm.subtype_mk
162 
163 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] in
164 theorem update_eq_ae (fallback : State C) (a : A) (z : State C) :
165     ∀ᵐ y∂μ,0<D.density a y z.1 →
166       (D.update fallback a z y).1=(D.density a y z.1)⁻¹ • D.op a y z.1 := by
167   have hN : ∀ᵐ y∂μ,y∉D.exceptional a := by
168     exact ae_iff.mpr (by simpa using D.exceptional_null a)
169   filter_upwards [hN] with y hy hp
170   exact ite_eq_left ⟨hy,hp⟩
171 
172 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] in
173 /-- Density times the updated state is the unnormalized branch, including the
174 zero-density case. Strict positivity of cone mass makes that branch zero. -/
175 theorem density_smul_update (fallback : State C) (a : A) (z : State C) (y : Y)
176     (hy : y∉D.exceptional a) :
177     D.density a y z.1 • (D.update fallback a z y).1=D.op a y z.1 := by
178   have hc := D.positive_off_exceptional a y hy z.2.1
179   by_cases hp : 0<D.density a y z.1
180   · change D.density a y z.1 • D.updateValue fallback a z y=_
181     rw [updateValue,ite_eq_left ⟨hy,hp⟩,smul_smul,mul_inv_cancel₀ hp.ne',one_smul]
182   · have hz : D.density a y z.1=0 :=
183       le_antisymm (le_of_not_gt hp) (C.mass_nonneg hc)
184     have ho : D.op a y z.1=0 := (C.mass_zero_iff hc).mp hz
185     rw [hz,zero_smul,ho]
186 
187 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] in
188 theorem density_smul_update_ae (fallback : State C) (a : A) (z : State C) :
189     ∀ᵐ y∂μ,D.density a y z.1 • (D.update fallback a z y).1=D.op a y z.1 := by
190   have hN : ∀ᵐ y∂μ,y∉D.exceptional a :=
191     ae_iff.mpr (by simpa using D.exceptional_null a)
192   exact hN.mono (fun y hy => D.density_smul_update fallback a z y hy)
193 
194 end DensityInstrument
195 end Komorebi.LSM.ContinuousInstrument

Back to source controls