MarkovWindows.lean

1 import KomorebiLSM.MarkovRecords
2 
3 /-! Rolling windows are actual measurable pushforwards of full chronological
4 Markov records; their restart-at-entry identity is proved from kernel algebra. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.MarkovStability
7 open MeasureTheory ProbabilityTheory SequentialLowerCertificate MeasureTVCalculus
8 open scoped ENNReal
9 
10 /-- Mapping the retained prefix of a composition product gives the corresponding
11 mapped-prefix joint law, with the conditional row pulled back along that map. -/
12 theorem map_compProd_left {A B C : Type*} [MeasurableSpace A] [MeasurableSpace B] [MeasurableSpace C]
13     (ν : Measure A) [IsProbabilityMeasure ν] (f : A → B) (hf : Measurable f)
14     (K : Kernel B C) [IsMarkovKernel K] :
15     (ν ⊗ₘ K.comap f hf).map (Prod.map f id)=ν.map f ⊗ₘ K := by
16   have hm : Measurable (Prod.map f (id : C → C)) :=
17     (hf.comp measurable_fst).prodMk measurable_snd
18   ext s hs
19   let g : B × C → ℝ≥0∞ := s.indicator 1
20   have hg : Measurable g := measurable_const.indicator hs
21   have hrow : Measurable (fun b => ∫⁻ c,g (b,c)∂K b) := hg.lintegral_kernel_prod_right'
22   rw [← lintegral_indicator_one (μ := (ν ⊗ₘ K.comap f hf).map (Prod.map f id)) hs,
23     ← lintegral_indicator_one (μ := ν.map f ⊗ₘ K) hs]
24   change (∫⁻ p,g p∂(ν ⊗ₘ K.comap f hf).map (Prod.map f id))=∫⁻ p,g p∂ν.map f ⊗ₘ K
25   rw [lintegral_map hg hm]
26   calc (∫⁻ a,g (Prod.map f id a)∂ν ⊗ₘ K.comap f hf)=
27       ∫⁻ a,∫⁻ c,g (Prod.map f id (a,c))∂K.comap f hf a∂ν :=
28         Measure.lintegral_compProd (hg.comp hm)
29     _ = ∫⁻ b,∫⁻ c,g (b,c)∂K b∂ν.map f := by
30       rw [lintegral_map hrow hf]
31       rfl
32     _ = ∫⁻ p,g p∂ν.map f ⊗ₘ K := (Measure.lintegral_compProd hg).symm
33 
34 /-- Keep the entry state at time t and the following L states. -/
35 def recordSegment {X : Type*} (t : ℕ) : (L : ℕ) → Record X (t+L) → Record X L
36   | 0,r => recordLast t r
37   | L+1,r => (recordSegment t L r.1,r.2)
38 
39 theorem recordSegment_measurable {X : Type*} [MeasurableSpace X] (t : ℕ) :
40     (L : ℕ) → Measurable (recordSegment (X := X) t L)
41   | 0 => recordLast_measurable t
42   | L+1 => (recordSegment_measurable t L |>.comp measurable_fst).prodMk measurable_snd
43 
44 theorem recordLast_segment {X : Type*} (t L : ℕ) (r : Record X (t+L)) :
45     recordLast L (recordSegment t L r)=recordLast (t+L) r := by
46   cases L <;> rfl
47 
48 variable {X : Type*} [MeasurableSpace X]
49 
50 /-- Restarting the Markov construction at its actual time-t marginal equals
51 extracting that segment from the actual full record law. -/
52 theorem recordLaw_segment (P : Kernel X X) [IsMarkovKernel P]
53     (ν0 : Measure X) [IsProbabilityMeasure ν0] (t : ℕ) :
54     ∀ L,(recordLaw P ν0 (t+L)).map (recordSegment t L)=recordLaw P (marginal P ν0 t) L
55   | 0 => by
56     change (recordLaw P ν0 t).map (recordLast t)=marginal P ν0 t
57     exact recordLaw_last P ν0 t
58   | L+1 => by
59     let f := recordSegment (X := X) t L
60     let K := P.comap (recordLast L) (recordLast_measurable L)
61     have hk : K.comap f (recordSegment_measurable t L)=
62         P.comap (recordLast (t+L)) (recordLast_measurable (t+L)) := by
63       ext r s hs
64       change P (recordLast L (recordSegment t L r)) s=P (recordLast (t+L) r) s
65       rw [recordLast_segment]
66     change ((recordLaw P ν0 (t+L)) ⊗ₘ
67       P.comap (recordLast (t+L)) (recordLast_measurable (t+L))).map (Prod.map f id)=
68         recordLaw P (marginal P ν0 t) L ⊗ₘ K
69     rw [← hk,map_compProd_left (recordLaw P ν0 (t+L)) f (recordSegment_measurable t L) K]
70     have hi := recordLaw_segment P ν0 t L
71     change ((recordLaw P ν0 (t+L)).map (recordSegment t L)) ⊗ₘ K=_
72     rw [hi]
73 
74 /-- The literal rolling-window law is a pushforward from the full record. Its
75 L transitions contain L+1 observations. -/
76 noncomputable def rollingWindowLaw (P : Kernel X X) (ν0 : Measure X) (t L : ℕ) : Measure (Record X L) :=
77   (recordLaw P ν0 (t+L)).map (recordSegment t L)
78 
79 instance rollingWindow_probability (P : Kernel X X) [IsMarkovKernel P]
80     (ν0 : Measure X) [IsProbabilityMeasure ν0] (t L : ℕ) :
81     IsProbabilityMeasure (rollingWindowLaw P ν0 t L) := by unfold rollingWindowLaw; infer_instance
82 
83 /-- Full registered rolling-window bound from the actual marginal entry error. -/
84 theorem rollingWindow_bound (P Q : Kernel X X) [IsMarkovKernel P] [IsMarkovKernel Q]
85     (Δ : ℝ) (hΔ : ∀ x,lawTV (P x) (Q x)≤Δ)
86     (ν0 η0 : Measure X) [IsProbabilityMeasure ν0] [IsProbabilityMeasure η0] (t L : ℕ) :
87     lawTV (rollingWindowLaw P ν0 t L) (rollingWindowLaw Q η0 t L)≤
88       min 1 (lawTV (marginal P ν0 t) (marginal Q η0 t)+(L:ℝ)*Δ) := by
89   simpa only [rollingWindowLaw,recordLaw_segment] using
90     recordLaw_bound P Q Δ hΔ (marginal P ν0 t) (marginal Q η0 t) L
91 
92 /-- Inserting the derived geometric entry bound gives an explicit window budget. -/
93 theorem rollingWindow_geometric_bound (P Q : Kernel X X) [IsMarkovKernel P] [IsMarkovKernel Q]
94     (reference : Measure X) [IsProbabilityMeasure reference] (ρ Δ : ℝ)
95     (hρ0 : 0<ρ) (hρ1 : ρ≤1) (hmin : Minorized P ρ reference)
96     (hΔ : ∀ x,lawTV (P x) (Q x)≤Δ)
97     (ν0 η0 : Measure X) [IsProbabilityMeasure ν0] [IsProbabilityMeasure η0] (t L : ℕ) :
98     lawTV (rollingWindowLaw P ν0 t L) (rollingWindowLaw Q η0 t L)≤
99       min 1 ((1-ρ)^t*lawTV ν0 η0+Δ*(1-(1-ρ)^t)/ρ+(L:ℝ)*Δ) := by
100   apply (rollingWindow_bound P Q Δ hΔ ν0 η0 t L).trans
101   apply min_le_min le_rfl
102   exact add_le_add ((marginal_bound P Q reference ρ Δ hρ0 hρ1 hmin hΔ ν0 η0 t).trans
103     (min_le_right _ _)) le_rfl
104 
105 /-- The common-initial-law window budget is uniform in its start time. -/
106 theorem rollingWindow_same_initial_uniform (P Q : Kernel X X) [IsMarkovKernel P] [IsMarkovKernel Q]
107     (reference : Measure X) [IsProbabilityMeasure reference] (ρ Δ : ℝ)
108     (hρ0 : 0<ρ) (hρ1 : ρ≤1) (hΔ0 : 0≤Δ) (hmin : Minorized P ρ reference)
109     (hΔ : ∀ x,lawTV (P x) (Q x)≤Δ)
110     (ν0 : Measure X) [IsProbabilityMeasure ν0] (t L : ℕ) :
111     lawTV (rollingWindowLaw P ν0 t L) (rollingWindowLaw Q ν0 t L)≤
112       min 1 (Δ/ρ+(L:ℝ)*Δ) := by
113   apply (rollingWindow_bound P Q Δ hΔ ν0 ν0 t L).trans
114   apply min_le_min le_rfl
115   exact add_le_add ((marginal_same_initial_uniform P Q reference ρ Δ hρ0 hρ1 hΔ0 hmin hΔ ν0 t).trans
116     (min_le_right _ _)) le_rfl
117 
118 /-- The source's reference confidence rectangle gives this actual all-time
119 one-marginal error bound, separate from any complete-record guarantee. -/
120 theorem reference_marginal_uniform (P Q : Kernel X X) [IsMarkovKernel P] [IsMarkovKernel Q]
121     (reference : Measure X) [IsProbabilityMeasure reference]
122     (hmin : Minorized P (31/125) reference)
123     (hΔ : ∀ x,lawTV (P x) (Q x)≤(2437/90000:ℝ))
124     (ν0 : Measure X) [IsProbabilityMeasure ν0] (t : ℕ) :
125     lawTV (marginal P ν0 t) (marginal Q ν0 t)≤(2437/22320:ℝ) := by
126   have hb := (marginal_same_initial_uniform P Q reference (31/125) (2437/90000)
127     (by norm_num) (by norm_num) (by norm_num) hmin hΔ ν0 t).trans (min_le_right _ _)
128   norm_num at hb ⊢
129   exact hb
130 
131 end Komorebi.LSM.MarkovStability

Back to source controls