ContinuousBins.lean

1 import KomorebiLSM.InstrumentContraction
2 import KomorebiLSM.ContinuousInstrument
3 import KomorebiLSM.PolicyComparison
4 import Mathlib.Analysis.Convex.Integral
5 import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
6 import Mathlib.MeasureTheory.Integral.Bochner.Set
7 import Mathlib.Analysis.Normed.Module.FiniteDimension
8 
9 /-! P56: exact event-cell operators and the averaged posterior. -/
10 set_option autoImplicit false
11 namespace Komorebi.LSM.ContinuousBins
12 open MeasureTheory
13 open scoped BigOperators
14 variable {E Y I : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
15 variable [CompleteSpace E] [MeasurableSpace Y]
16 variable (C : BaseNorm.ProbabilityCone E) (μ : Measure Y) [IsProbabilityMeasure μ]
17 
18 noncomputable def cellOperator (B : Y → E →L[ℝ] E) (S : Set Y) : E →L[ℝ] E :=
19   ∫ y in S, B y ∂μ
20 
21 omit [CompleteSpace E] [IsProbabilityMeasure μ] in
22 theorem cellOperator_apply (B : Y → E →L[ℝ] E) (hB : Integrable B μ)
23     (S : Set Y) (z : E) : cellOperator μ B S z = ∫ y in S, B y z ∂μ :=
24   ContinuousLinearMap.integral_apply hB.integrableOn z
25 
26 /-- A measurable event integrates cone-valued outputs to another cone element. -/
27 theorem setIntegral_mem {f : Y → E} (hf : Integrable f μ) (S : Set Y)
28     (hS : MeasurableSet S) (hpos : ∀ᵐ y ∂μ, f y ∈ C.carrier) :
29     (∫ y in S, f y ∂μ) ∈ C.carrier := by
30   rw [← integral_indicator hS]
31   apply C.convex_carrier.integral_mem C.closed ?_ (hf.indicator hS)
32   filter_upwards [hpos] with y hy
33   by_cases hs : y ∈ S
34   · simpa only [Set.indicator_of_mem hs] using hy
35   · simpa only [Set.indicator_of_notMem hs] using C.zero_mem
36 
37 theorem cellOperator_positive (B : Y → E →L[ℝ] E) (hB : Integrable B μ)
38     (hpos : ∀ᵐ y ∂μ, ∀ z ∈ C.carrier, B y z ∈ C.carrier)
39     (S : Set Y) (hS : MeasurableSet S) (z : E) (hz : z ∈ C.carrier) :
40     cellOperator μ B S z ∈ C.carrier := by
41   rw [cellOperator_apply μ B hB S z]
42   exact setIntegral_mem C μ ((ContinuousLinearMap.apply ℝ E z).integrable_comp hB) S hS
43     (hpos.mono fun _ hy => hy z hz)
44 
45 variable [Fintype I]
46 
47 omit [CompleteSpace E] [IsProbabilityMeasure μ] in
48 /-- The sum of exact cell operators is the original integrated operator. -/
49 theorem cellOperator_sum (B : Y → E →L[ℝ] E) (hB : Integrable B μ)
50     (S : I → Set Y) (hS : ∀ i, MeasurableSet (S i))
51     (hdis : Pairwise (fun i j => Disjoint (S i) (S j))) (hcover : ⋃ i, S i = Set.univ) :
52     ∑ i, cellOperator μ B (S i) = ∫ y, B y ∂μ := by
53   symm
54   simpa only [hcover,Measure.restrict_univ,cellOperator] using
55     (integral_iUnion_fintype hS hdis (fun _ => hB.integrableOn))
56 
57 /-- Exact integrated mass and event partitioning construct a finite instrument. -/
58 theorem cellInstrument (B : Y → E →L[ℝ] E) (hB : Integrable B μ)
59     (hpos : ∀ᵐ y ∂μ, ∀ z ∈ C.carrier, B y z ∈ C.carrier)
60     (hmass : ∀ z, C.mass ((∫ y, B y ∂μ) z)=C.mass z)
61     (S : I → Set Y) (hS : ∀ i, MeasurableSet (S i))
62     (hdis : Pairwise (fun i j => Disjoint (S i) (S j))) (hcover : ⋃ i, S i = Set.univ) :
63     C.Instrument (fun i => (cellOperator μ B (S i)).toLinearMap) := by
64   refine ⟨fun i z hz => cellOperator_positive C μ B hB hpos (S i) (hS i) z hz,?_⟩
65   intro z
66   calc
67     ∑ i, C.mass (cellOperator μ B (S i) z) = C.mass ((∑ i, cellOperator μ B (S i)) z) := by
68       simp only [_root_.sum_apply,map_sum]
69     _ = C.mass ((∫ y, B y ∂μ) z) := by rw [cellOperator_sum μ B hB S hS hdis hcover]
70     _ = C.mass z := hmass z
71 
72 /-- A concrete measurable version may choose any fixed fallback on zero density.
73 Multiplication by the likelihood removes this arbitrary choice. -/
74 noncomputable def posterior (B : Y → E →L[ℝ] E) (fallback : E) (z : E) (y : Y) : E :=
75   if 0 < C.mass (B y z) then (C.mass (B y z))⁻¹ • B y z else fallback
76 
77 omit [CompleteSpace E] [MeasurableSpace Y] in
78 theorem likelihood_smul_posterior (B : Y → E →L[ℝ] E) (fallback z : E) (y : Y)
79     (hy : B y z ∈ C.carrier) :
80     C.mass (B y z) • posterior C B fallback z y = B y z := by
81   by_cases hp : 0 < C.mass (B y z)
82   · simp only [posterior,ite_eq_left hp,smul_smul,mul_inv_cancel₀ (ne_of_gt hp),one_smul]
83   · have hm : C.mass (B y z)=0 := le_antisymm (le_of_not_gt hp) (C.mass_nonneg hy)
84     have hz : B y z=0 := (C.mass_zero_iff hy).mp hm
85     simp [posterior,hz]
86 
87 omit [CompleteSpace E] [IsProbabilityMeasure μ] in
88 /-- The exact cell posterior is the density-weighted average of the fine
89 posteriors. A representative observation point does not occur in this formula. -/
90 theorem cell_posterior_average (B : Y → E →L[ℝ] E) (hB : Integrable B μ)
91     (hpos : ∀ᵐ y ∂μ, ∀ z ∈ C.carrier, B y z ∈ C.carrier)
92     (S : Set Y) (fallback z : E) (hz : z ∈ C.carrier) :
93     (C.mass (cellOperator μ B S z))⁻¹ • cellOperator μ B S z =
94       (C.mass (cellOperator μ B S z))⁻¹ •
95         ∫ y in S, C.mass (B y z) • posterior C B fallback z y ∂μ := by
96   congr 1
97   rw [cellOperator_apply μ B hB S z]
98   symm
99   apply integral_congr_ae
100   filter_upwards [ae_restrict_of_ae hpos] with y hy
101   exact likelihood_smul_posterior C B fallback z y (hy z hz)
102 
103 theorem cell_posterior_base (B : Y → E →L[ℝ] E) (hB : Integrable B μ)
104     (hpos : ∀ᵐ y ∂μ, ∀ z ∈ C.carrier, B y z ∈ C.carrier)
105     (S : Set Y) (hS : MeasurableSet S) (z : E) (hz : z ∈ C.carrier)
106     (hp : 0 < C.mass (cellOperator μ B S z)) :
107     (C.mass (cellOperator μ B S z))⁻¹ • cellOperator μ B S z ∈ C.base := by
108   refine ⟨C.smul_mem (inv_pos.mpr hp).le (cellOperator_positive C μ B hB hpos S hS z hz),?_⟩
109   simp only [map_smul,smul_eq_mul,inv_mul_cancel₀ (ne_of_gt hp)]
110 
111 section Model
112 variable {A : Type*} [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
113 variable (D : ContinuousInstrument.DensityInstrument (A := A) C μ)
114 
115 /-- A cell probability is the literal event probability of the continuous kernel. -/
116 theorem kernel_cell_probability (a : A) (z : ContinuousInstrument.DensityInstrument.State C)
117     (S : Set Y) (hS : MeasurableSet S) :
118     (D.kernel a z).real S = C.mass (cellOperator μ (D.op a) S z.1) := by
119   rw [D.kernel_event_real a z S hS,cellOperator_apply μ (D.op a) (D.integrable_op a) S z.1]
120   exact (ContinuousInstrument.massCLM C).integral_comp_comm (D.applied_integrable a z.1).integrableOn
121 
122 omit [CompleteSpace E] [IsProbabilityMeasure μ] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] in
123 /-- The same measurable update used by the instrument, including its fixed
124 fallback, has the exact density-weighted cell average. -/
125 theorem kernel_cell_posterior_average (a : A) (fallback z : ContinuousInstrument.DensityInstrument.State C)
126     (S : Set Y) :
127     (C.mass (cellOperator μ (D.op a) S z.1))⁻¹ • cellOperator μ (D.op a) S z.1 =
128       (C.mass (cellOperator μ (D.op a) S z.1))⁻¹ •
129         ∫ y in S, D.density a y z.1 • (D.update fallback a z y).1 ∂μ := by
130   congr 1
131   rw [cellOperator_apply μ (D.op a) (D.integrable_op a) S z.1]
132   symm
133   apply integral_congr_ae
134   filter_upwards [ae_restrict_of_ae (D.positive a),ae_restrict_of_ae (D.update_eq_ae fallback a z)] with y hy hu
135   by_cases hp : 0 < D.density a y z.1
136   · rw [hu hp,smul_smul,mul_inv_cancel₀ hp.ne',one_smul]
137   · have hn : 0 ≤ D.density a y z.1 := C.mass_nonneg (hy z.1 z.2.1)
138     have he : D.density a y z.1=0 := le_antisymm (le_of_not_gt hp) hn
139     have hz : D.op a y z.1=0 := (C.mass_zero_iff (hy z.1 z.2.1)).mp he
140     rw [he,zero_smul,hz]
141 
142 end Model
143 
144 section Words
145 variable {A : Type*}
146 omit [Fintype I]
147 
148 /-- The cell history, rather than an unobserved within-cell value, selects each
149 next operator. Thus this construction permits exactly bin-measurable policies. -/
150 noncomputable def cellWordMap (B : List (A × I) → A → Y → E →L[ℝ] E)
151     (S : I → Set Y) : List (A × I) → List (A × I) → E →L[ℝ] E
152   | _, [] => ContinuousLinearMap.id ℝ E
153   | h, s::w => (cellWordMap B S (h++[s]) w).comp (cellOperator μ (B h s.1) (S s.2))
154 
155 /-- Literal chronological repeated integration of the operator density over
156 the observed cells, with no representative-point substitution. -/
157 noncomputable def iteratedCellVector (B : List (A × I) → A → Y → E →L[ℝ] E)
158     (S : I → Set Y) : List (A × I) → List (A × I) → E → E
159   | _, [], z => z
160   | h, s::w, z => ∫ y in S s.2, iteratedCellVector B S (h++[s]) w (B h s.1 y z) ∂μ
161 
162 omit [IsProbabilityMeasure μ] in
163 theorem iteratedCellVector_eq (B : List (A × I) → A → Y → E →L[ℝ] E)
164     (hB : ∀ h a,Integrable (B h a) μ) (S : I → Set Y)
165     (h w : List (A × I)) (z : E) :
166     iteratedCellVector μ B S h w z=cellWordMap μ B S h w z := by
167   induction w generalizing h z with
168   | nil => rfl
169   | cons s w ih =>
170     simp only [iteratedCellVector,cellWordMap,ContinuousLinearMap.comp_apply]
171     simp_rw [ih]
172     have hint : Integrable (fun y => B h s.1 y z) (μ.restrict (S s.2)) :=
173       ((ContinuousLinearMap.apply ℝ E z).integrable_comp (hB h s.1)).integrableOn
174     rw [(cellWordMap μ B S (h++[s]) w).integral_comp_comm hint]
175     rw [← cellOperator_apply μ (B h s.1) (hB h s.1) (S s.2) z]
176 
177 omit [CompleteSpace E] [IsProbabilityMeasure μ] in
178 theorem cellWordMap_recordState (B : List (A × I) → A → Y → E →L[ℝ] E)
179     (S : I → Set Y) (n : ℕ) (h : List (A × I)) (z : E)
180     (w : ObservationTree.Record (A × I) n) :
181     cellWordMap μ B S h (ObservationTree.recordList w) z =
182       ObservationTree.recordState
183         (fun h s => (cellOperator μ (B h s.1) (S s.2)).toLinearMap) n h z w := by
184   induction n generalizing h z with
185   | zero => rfl
186   | succ n ih =>
187     exact ih (h++[w.1]) (cellOperator μ (B h w.1.1) (S w.1.2) z) w.2
188 
189 omit [IsProbabilityMeasure μ] in
190 /-- The finite event law has the exact repeated-integral interpretation at
191 every horizon and every bin history. -/
192 theorem iterated_cell_record_probability (B : List (A × I) → A → Y → E →L[ℝ] E)
193     (hB : ∀ h a,Integrable (B h a) μ) (S : I → Set Y)
194     (n : ℕ) (h : List (A × I)) (z : E) (w : ObservationTree.Record (A × I) n) :
195     C.mass (iteratedCellVector μ B S h (ObservationTree.recordList w) z) =
196       ObservationTree.recordLaw C
197         (fun h s => (cellOperator μ (B h s.1) (S s.2)).toLinearMap) n h z w := by
198   rw [iteratedCellVector_eq μ B hB S h (ObservationTree.recordList w) z,
199     cellWordMap_recordState μ B S n h z w]
200   rfl
201 
202 end Words
203 
204 end Komorebi.LSM.ContinuousBins

Back to source controls