PredictableResidualP66.lean

1 import KomorebiLSM.PredictableResidualAnytime
2 import KomorebiLSM.PredictableResidualAffine
3 
4 /-! Full P66: arbitrary probability sample spaces, actual conditional means,
5 finite/countable prospective budgets, general intervals including zero width,
6 and data-selected times on the same simultaneous event. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.PredictableResidualGeneral
9 open MeasureTheory ProbabilityTheory Real PredictableResidual PredictableResidualAffine
10 open scoped BigOperators NNReal ENNReal
11 variable {Ω J : Type*} [mΩ : MeasurableSpace Ω] [Countable J]
12 variable {μ : Measure Ω} [IsProbabilityMeasure μ]
13 
14 /-- Every registered interval-valued adapted process obeys the true
15 conditional-sum boundary at all positive times, on an arbitrary sample space. -/
16 theorem predictable_sum_interval_rules (ℱ : Filtration ℕ mΩ) (X : J → ℕ → Ω → ℝ)
17     (lower width : J → ℝ) (hw : ∀ j,0≤width j)
18     (hX : ∀ j i,Measurable[ℱ (i+1)] (X j i))
19     (hb : ∀ j i,∀ᵐ ω∂μ,X j i ω∈Set.Icc (lower j) (lower j+width j))
20     (α : J → NNReal) (hα : ∀ j,0<α j) (hs : Summable α)
21     (δ : NNReal) (hbudget : ∑' j,α j≤δ) (hδ1 : δ≤1) :
22     1-(δ:ℝ)≤μ.real {ω | ∀ j n,|centeredSum (μ:=μ) ℱ (X j) (n+1) ω|≤
23       width j*boundary (n+1) (α j)} := by
24   have ht := time_uniform_rules ℱ (normalizedProcess lower width X)
25     (normalized_adapted ℱ lower width X hX) (normalized_mem_unit_ae lower width X hw hb)
26     α hα hs δ hbudget hδ1
27   have htrans := normalized_bound_transfer_ae ℱ lower width X hX hw hb
28     (fun j n => boundary (n+1) (α j))
29   have hle : μ {ω | ∀ j n,|centeredSum (μ:=μ) ℱ
30       (normalizedProcess lower width X j) (n+1) ω|≤boundary (n+1) (α j)}≤
31       μ {ω | ∀ j n,|centeredSum (μ:=μ) ℱ (X j) (n+1) ω|≤
32         width j*boundary (n+1) (α j)} := measure_mono_ae htrans
33   exact ht.trans (ENNReal.toReal_mono (measure_ne_top _ _) hle)
34 
35 omit [IsProbabilityMeasure μ] in
36 /-- The simultaneous interval event is measurable, not merely an arbitrary
37 validity predicate supplied with an outer-probability interpretation. -/
38 theorem interval_event_measurable (ℱ : Filtration ℕ mΩ) (X : J → ℕ → Ω → ℝ)
39     (hX : ∀ j i,Measurable[ℱ (i+1)] (X j i)) (width : J → ℝ) (α : J → NNReal) :
40     MeasurableSet {ω | ∀ j n,|centeredSum (μ:=μ) ℱ (X j) (n+1) ω|≤
41       width j*boundary (n+1) (α j)} := by
42   simp only [Set.ofPred_forall]
43   apply MeasurableSet.iInter
44   intro j
45   apply MeasurableSet.iInter
46   intro n
47   exact measurableSet_le (centeredSum_measurable ℱ (X j) (hX j) (n+1)).norm measurable_const
48 
49 /-- The [0,1] residual/drift certificate for arbitrary countable rule indices. -/
50 theorem predictable_residual_certificate_countable (ℱ : Filtration ℕ mΩ)
51     (X p : J → ℕ → Ω → ℝ)
52     (hX : ∀ j i,Measurable[ℱ (i+1)] (X j i))
53     (hb : ∀ j i,∀ᵐ ω∂μ,X j i ω∈Set.Icc (0:ℝ) 1)
54     (α : J → NNReal) (hα : ∀ j,0<α j) (hs : Summable α)
55     (δ : NNReal) (hbudget : ∑' j,α j≤δ) (hδ1 : δ≤1) :
56     1-(δ:ℝ)≤μ.real {ω | ∀ j n,
57       |observedResidual (X j) (p j) (n+1) ω-
58         conditionalDrift (μ:=μ) ℱ (X j) (p j) (n+1) ω|≤boundary (n+1) (α j)} := by
59   simpa only [residual_sub_drift] using time_uniform_rules ℱ X hX hb α hα hs δ hbudget hδ1
60 
61 /-- Full P66 on the actual measurable residual/drift event. The predictions
62 may change with time; their errors cancel exactly. The interval width may be zero. -/
63 theorem predictable_residual_interval_certificate (ℱ : Filtration ℕ mΩ)
64     (X p : J → ℕ → Ω → ℝ) (lower width : J → ℝ) (hw : ∀ j,0≤width j)
65     (hX : ∀ j i,Measurable[ℱ (i+1)] (X j i))
66     (hb : ∀ j i,∀ᵐ ω∂μ,X j i ω∈Set.Icc (lower j) (lower j+width j))
67     (α : J → NNReal) (hα : ∀ j,0<α j) (hs : Summable α)
68     (δ : NNReal) (hbudget : ∑' j,α j≤δ) (hδ1 : δ≤1) :
69     MeasurableSet {ω | ∀ j n,
70       |observedResidual (X j) (p j) (n+1) ω-
71         conditionalDrift (μ:=μ) ℱ (X j) (p j) (n+1) ω|≤width j*boundary (n+1) (α j)} ∧
72     1-(δ:ℝ)≤μ.real {ω | ∀ j n,
73       |observedResidual (X j) (p j) (n+1) ω-
74         conditionalDrift (μ:=μ) ℱ (X j) (p j) (n+1) ω|≤width j*boundary (n+1) (α j)} := by
75   constructor
76   · simpa only [residual_sub_drift] using interval_event_measurable ℱ X hX width α
77   · simpa only [residual_sub_drift] using
78       predictable_sum_interval_rules ℱ X lower width hw hX hb α hα hs δ hbudget hδ1
79 
80 omit [Countable J] in
81 /-- Finite registrations retain the literal finite sum of their budgets. -/
82 theorem predictable_residual_interval_finite [Fintype J] (ℱ : Filtration ℕ mΩ)
83     (X p : J → ℕ → Ω → ℝ) (lower width : J → ℝ) (hw : ∀ j,0≤width j)
84     (hX : ∀ j i,Measurable[ℱ (i+1)] (X j i))
85     (hb : ∀ j i,∀ᵐ ω∂μ,X j i ω∈Set.Icc (lower j) (lower j+width j))
86     (α : J → NNReal) (hα : ∀ j,0<α j) (δ : NNReal)
87     (hbudget : ∑ j,α j≤δ) (hδ1 : δ≤1) :
88     1-(δ:ℝ)≤μ.real {ω | ∀ j n,
89       |observedResidual (X j) (p j) (n+1) ω-
90         conditionalDrift (μ:=μ) ℱ (X j) (p j) (n+1) ω|≤width j*boundary (n+1) (α j)} := by
91   exact (predictable_residual_interval_certificate ℱ X p lower width hw hX hb α hα
92     (summable_of_hasFiniteSupport (Set.toFinite _)) δ (by simpa only [tsum_fintype] using hbudget) hδ1).2
93 
94 omit [Countable J] [IsProbabilityMeasure μ] in
95 /-- Exact reindexing changes neither the simultaneous residual event nor the
96 actual total prospective budget; no padded rules consume extra probability. -/
97 theorem registration_transport {K : Type*} (e : K ≃ J) (ℱ : Filtration ℕ mΩ)
98     (X p : J → ℕ → Ω → ℝ) (width : J → ℝ) (α : J → NNReal) (hs : Summable α) :
99     Summable (fun k => α (e k)) ∧ (∑' k,α (e k))=∑' j,α j ∧
100     {ω | ∀ k n,|observedResidual (X (e k)) (p (e k)) (n+1) ω-
101       conditionalDrift (μ:=μ) ℱ (X (e k)) (p (e k)) (n+1) ω|≤
102         width (e k)*boundary (n+1) (α (e k))}=
103     {ω | ∀ j n,|observedResidual (X j) (p j) (n+1) ω-
104       conditionalDrift (μ:=μ) ℱ (X j) (p j) (n+1) ω|≤width j*boundary (n+1) (α j)} := by
105   obtain ⟨hS,hSum⟩ := CountableConfidence.budget_transport e α hs
106   refine ⟨hS,hSum,?_⟩
107   ext ω
108   exact CountableConfidence.forall_transport e (fun j => ∀ n : ℕ,
109     |observedResidual (X j) (p j) (n+1) ω-conditionalDrift (μ:=μ) ℱ (X j) (p j) (n+1) ω|≤
110       width j*boundary (n+1) (α j))
111 
112 omit [Countable J] [IsProbabilityMeasure μ] in
113 /-- A data-selected positive time and registered rule are already included in
114 the same simultaneous event; no optional stopping or independence is needed. -/
115 theorem selected_interval_bound (ℱ : Filtration ℕ mΩ)
116     (X p : J → ℕ → Ω → ℝ) (width : J → ℝ) (α : J → NNReal) (ω : Ω)
117     (hall : ∀ j n,|observedResidual (X j) (p j) (n+1) ω-
118       conditionalDrift (μ:=μ) ℱ (X j) (p j) (n+1) ω|≤width j*boundary (n+1) (α j))
119     (time : Ω → ℕ) (rule : Ω → J) (ht : 0<time ω) :
120     |observedResidual (X (rule ω)) (p (rule ω)) (time ω) ω-
121       conditionalDrift (μ:=μ) ℱ (X (rule ω)) (p (rule ω)) (time ω) ω|≤
122         width (rule ω)*boundary (time ω) (α (rule ω)) := by
123   have he : (time ω-1)+1=time ω := by omega
124   simpa only [he] using hall (rule ω) (time ω-1)
125 
126 end Komorebi.LSM.PredictableResidualGeneral

Back to source controls