CoveredAdaptiveEvidence.lean

1 import KomorebiLSM.CoveredAdaptiveActions
2 import KomorebiLSM.PredictableResidualP66
3 
4 /-! Sequential covered-action evidence for actual contextual kernel means. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.CoveredAdaptiveActions
7 open MeasureTheory ProbabilityTheory
8 open scoped BigOperators NNReal
9 
10 variable {Ω A Y J : Type*} [mΩ : MeasurableSpace Ω] [mA : MeasurableSpace A]
11 variable [mY : MeasurableSpace Y] [Fintype A] [DecidableEq A] [MeasurableSingletonClass A]
12 variable {μ : Measure Ω} [IsProbabilityMeasure μ] [Countable J]
13 variable (ℱ : Filtration ℕ mΩ) (action : ℕ → Ω → A) (observation : ℕ → Ω → Y)
14 variable (E : ∀ n,Experiment (μ := μ) (ℱ.le n) (action n) (observation n))
15 
16 /-- Actual observations with the recorded propensity correction. -/
17 noncomputable def evidenceProcess (φ : J → ℕ → Ω × Y → ℝ) (target : J → A)
18     (j : J) (n : ℕ) : Ω → ℝ :=
19   evidence (ℱ.le n) (E n) (φ j n) (target j)
20 
21 /-- The action-conditioned quantities along the contexts actually encountered. -/
22 noncomputable def kernelMeanProcess (φ : J → ℕ → Ω × Y → ℝ) (target : J → A)
23     (j : J) (n : ℕ) : Ω → ℝ :=
24   targetMean (mH := ℱ n) (E n).observationKernel (φ j n) (target j)
25 
26 omit [IsProbabilityMeasure μ] [Countable J] [Fintype A] in
27 theorem evidenceProcess_adapted (φ : J → ℕ → Ω × Y → ℝ) (target : J → A)
28     (ha : ∀ n,Measurable[ℱ (n+1)] (action n))
29     (hy : ∀ n,Measurable[ℱ (n+1)] (observation n))
30     (hφ : ∀ j n,@Measurable (Ω × Y) ℝ ((ℱ n).prod mY) _ (φ j n)) (j : J) (n : ℕ) :
31     Measurable[ℱ (n+1)] (evidenceProcess ℱ action observation E φ target j n) :=
32   evidence_measurable_at (ℱ.le n) (E n) (ℱ.mono (by omega)) (ha n) (hy n) (φ j n) (hφ j n) (target j)
33 
34 omit [Countable J] in
35 theorem evidenceProcess_condExp (φ : J → ℕ → Ω × Y → ℝ) (target : J → A)
36     (hφ : ∀ j n,@Measurable (Ω × Y) ℝ ((ℱ n).prod mY) _ (φ j n))
37     (hb : ∀ j n ω y,φ j n (ω,y)∈Set.Icc (0:ℝ) 1)
38     (c : J → ℝ) (hc : ∀ j,0<c j)
39     (hcover : ∀ j n ω,c j≤propensity (mH := ℱ n) (E n).policy (target j) ω)
40     (j : J) (n : ℕ) :
41     μ[evidenceProcess ℱ action observation E φ target j n | ℱ n] =ᵐ[μ]
42       kernelMeanProcess ℱ action observation E φ target j n :=
43   evidence_condExp (ℱ.le n) (E n) (φ j n) (hφ j n) (hb j n) (target j) (c j) (hc j)
44     (hcover j n)
45 
46 /-- Every actual conditional mean in the accumulated error can be replaced
47 simultaneously by its derived action-conditioned observation-kernel integral. -/
48 theorem centeredSum_eq_kernelSum_ae (φ : J → ℕ → Ω × Y → ℝ) (target : J → A)
49     (hφ : ∀ j n,@Measurable (Ω × Y) ℝ ((ℱ n).prod mY) _ (φ j n))
50     (hb : ∀ j n ω y,φ j n (ω,y)∈Set.Icc (0:ℝ) 1)
51     (c : J → ℝ) (hc : ∀ j,0<c j)
52     (hcover : ∀ j n ω,c j≤propensity (mH := ℱ n) (E n).policy (target j) ω) :
53     ∀ᵐ ω∂μ,∀ j n,
54       PredictableResidual.centeredSum (μ := μ) ℱ
55         (evidenceProcess ℱ action observation E φ target j) n ω=
56       (∑ i∈Finset.range n,evidenceProcess ℱ action observation E φ target j i ω)-
57         ∑ i∈Finset.range n,kernelMeanProcess ℱ action observation E φ target j i ω := by
58   have hce : ∀ᵐ ω∂μ,∀ j n,
59       (μ[evidenceProcess ℱ action observation E φ target j n | ℱ n]) ω=
60         kernelMeanProcess ℱ action observation E φ target j n ω :=
61     ae_all_iff.mpr (fun j => ae_all_iff.mpr (fun n =>
62       evidenceProcess_condExp ℱ action observation E φ target hφ hb c hc hcover j n))
63   filter_upwards [hce] with ω hω
64   intro j n
65   rw [PredictableResidual.centeredSum,← Finset.sum_sub_distrib]
66   apply Finset.sum_congr rfl
67   intro i _
68   rw [hω j i]
69 
70 omit [IsProbabilityMeasure μ] [Fintype A] in
71 /-- The actual simultaneous contextual evidence event is measurable. -/
72 theorem covered_event_measurable (φ : J → ℕ → Ω × Y → ℝ) (target : J → A)
73     (ha : ∀ n,Measurable[ℱ (n+1)] (action n))
74     (hy : ∀ n,Measurable[ℱ (n+1)] (observation n))
75     (hφ : ∀ j n,@Measurable (Ω × Y) ℝ ((ℱ n).prod mY) _ (φ j n))
76     (c : J → ℝ) (α : J → NNReal) :
77     MeasurableSet {ω | ∀ j n,
78       |(∑ i∈Finset.range (n+1),evidenceProcess ℱ action observation E φ target j i ω)-
79         ∑ i∈Finset.range (n+1),kernelMeanProcess ℱ action observation E φ target j i ω|≤
80           (1/c j)*PredictableResidual.boundary (n+1) (α j)} := by
81   simp only [Set.ofPred_forall]
82   apply MeasurableSet.iInter
83   intro j
84   apply MeasurableSet.iInter
85   intro n
86   apply measurableSet_le _ measurable_const
87   simp_rw [← Real.norm_eq_abs]
88   apply Measurable.norm
89   apply Measurable.sub
90   · apply Finset.measurable_fun_sum
91     intro i _
92     exact (evidenceProcess_adapted ℱ action observation E φ target ha hy hφ j i).mono
93       (ℱ.le (i+1)) le_rfl
94   · apply Finset.measurable_fun_sum
95     intro i _
96     exact (targetMean_measurable (mH := ℱ i) (E i).observationKernel (φ j i) (hφ j i)
97       (target j)).mono (ℱ.le i) le_rfl
98 
99 /-- Full P67: covered randomized actions estimate their actual contextual
100 kernel means simultaneously at every positive time and every registered rule.
101 The interval-width boundary comes from the full P66 theorem, not an assumed
102 concentration certificate. -/
103 theorem covered_adaptive_action_certificate (φ : J → ℕ → Ω × Y → ℝ) (target : J → A)
104     (ha : ∀ n,Measurable[ℱ (n+1)] (action n))
105     (hy : ∀ n,Measurable[ℱ (n+1)] (observation n))
106     (hφ : ∀ j n,@Measurable (Ω × Y) ℝ ((ℱ n).prod mY) _ (φ j n))
107     (hb : ∀ j n ω y,φ j n (ω,y)∈Set.Icc (0:ℝ) 1)
108     (c : J → ℝ) (hc : ∀ j,0<c j)
109     (hcover : ∀ j n ω,c j≤propensity (mH := ℱ n) (E n).policy (target j) ω)
110     (α : J → NNReal) (hα : ∀ j,0<α j) (hs : Summable α)
111     (δ : NNReal) (hbudget : ∑' j,α j≤δ) (hδ1 : δ≤1) :
112     MeasurableSet {ω | ∀ j n,
113       |(∑ i∈Finset.range (n+1),evidenceProcess ℱ action observation E φ target j i ω)-
114         ∑ i∈Finset.range (n+1),kernelMeanProcess ℱ action observation E φ target j i ω|≤
115           (1/c j)*PredictableResidual.boundary (n+1) (α j)} ∧
116     1-(δ:ℝ)≤μ.real {ω | ∀ j n,
117       |(∑ i∈Finset.range (n+1),evidenceProcess ℱ action observation E φ target j i ω)-
118         ∑ i∈Finset.range (n+1),kernelMeanProcess ℱ action observation E φ target j i ω|≤
119           (1/c j)*PredictableResidual.boundary (n+1) (α j)} := by
120   refine ⟨covered_event_measurable ℱ action observation E φ target ha hy hφ c α,?_⟩
121   have ht := PredictableResidualGeneral.predictable_sum_interval_rules (μ := μ) ℱ
122     (evidenceProcess ℱ action observation E φ target) (fun _ => 0) (fun j => 1/c j)
123     (fun j => one_div_nonneg.mpr (hc j).le)
124     (evidenceProcess_adapted ℱ action observation E φ target ha hy hφ)
125     (fun j n => Filter.Eventually.of_forall (fun ω => by
126       simpa only [zero_add,evidenceProcess] using evidence_mem_Icc (ℱ.le n) (E n) (φ j n) (hb j n)
127         (target j) (c j) (hc j) (hcover j n) ω)) α hα hs δ hbudget hδ1
128   apply ht.trans
129   apply ENNReal.toReal_mono (measure_ne_top _ _)
130   apply measure_mono_ae
131   filter_upwards [centeredSum_eq_kernelSum_ae ℱ action observation E φ target hφ hb c hc hcover]
132     with ω hω
133   intro hgood j n
134   rw [← hω j (n+1)]
135   exact hgood j n
136 
137 omit [Countable J] [IsProbabilityMeasure μ] [Fintype A] [MeasurableSingletonClass A] in
138 /-- A rule and a positive observation time selected using the data already
139 belong to the same simultaneous contextual evidence event. -/
140 theorem covered_bound_at_selected_time (φ : J → ℕ → Ω × Y → ℝ) (target : J → A)
141     (c : J → ℝ) (α : J → NNReal) (ω : Ω)
142     (hall : ∀ j n,
143       |(∑ i∈Finset.range (n+1),evidenceProcess ℱ action observation E φ target j i ω)-
144         ∑ i∈Finset.range (n+1),kernelMeanProcess ℱ action observation E φ target j i ω|≤
145           (1/c j)*PredictableResidual.boundary (n+1) (α j))
146     (time : Ω → ℕ) (rule : Ω → J) (ht : 0<time ω) :
147     |(∑ i∈Finset.range (time ω),evidenceProcess ℱ action observation E φ target (rule ω) i ω)-
148       ∑ i∈Finset.range (time ω),kernelMeanProcess ℱ action observation E φ target (rule ω) i ω|≤
149         (1/c (rule ω))*PredictableResidual.boundary (time ω) (α (rule ω)) := by
150   have he : (time ω-1)+1=time ω := by omega
151   simpa only [he] using hall (rule ω) (time ω-1)
152 
153 end Komorebi.LSM.CoveredAdaptiveActions

Back to source controls