ObservationLawComparison.lean

1 import KomorebiLSM.MeasureTVCalculus
2 import KomorebiLSM.KernelTVMeasurable
3 import KomorebiLSM.ObservationLawKernels
4 
5 /-! P69: actual causal record-law TV is bounded by conditional kernel TV averaged
6 under the true process and common policy. No common latent state space is used. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.ObservationLawComparison
9 open MeasureTheory ProbabilityTheory SequentialLowerCertificate MeasureTVCalculus
10 open scoped ENNReal BigOperators
11 
12 section KernelChange
13 variable {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
14 variable [MeasurableSpace.CountableOrCountablyGenerated X Y]
15 
16 /-- Changing one observation kernel under one actual common prefix costs its
17 conditional TV averaged over that prefix. -/
18 theorem compProd_change (μ : Measure X) [IsProbabilityMeasure μ]
19     (κ η : Kernel X Y) [IsMarkovKernel κ] [IsMarkovKernel η] :
20     lawTV (μ ⊗ₘ κ) (μ ⊗ₘ η)≤∫ x,KernelTVMeasurable.distance κ η x∂μ := by
21   apply lawTV_le_of_bounded_tests
22   intro f hf h0 h1
23   have hfi (K : Kernel X Y) [IsMarkovKernel K] (x : X) :
24       Integrable (fun y => f (x,y)) (K x) :=
25     bounded_test_integrable (K x) _ (hf.comp (measurable_const.prodMk measurable_id))
26       (fun y => h0 (x,y)) (fun y => h1 (x,y))
27   have hFm (K : Kernel X Y) [IsMarkovKernel K] :
28       Measurable (fun x => ∫ y,f (x,y)∂K x) :=
29     hf.stronglyMeasurable.integral_kernel_prod_right'.measurable
30   have hF0 (K : Kernel X Y) [IsMarkovKernel K] (x : X) :
31       0≤∫ y,f (x,y)∂K x := integral_nonneg (fun y => h0 (x,y))
32   have hF1 (K : Kernel X Y) [IsMarkovKernel K] (x : X) :
33       (∫ y,f (x,y)∂K x)≤1 := by
34     calc (∫ y,f (x,y)∂K x)≤∫ _ : Y,(1:ℝ)∂K x :=
35         integral_mono (hfi K x) (integrable_const _) (fun y => h1 (x,y))
36       _ = 1 := by simp
37   have hFk := bounded_test_integrable μ _ (hFm κ) (hF0 κ) (hF1 κ)
38   have hFe := bounded_test_integrable μ _ (hFm η) (hF0 η) (hF1 η)
39   have hd : Integrable (fun x => (∫ y,f (x,y)∂κ x)-(∫ y,f (x,y)∂η x)) μ :=
40     (hFk.sub hFe).congr (by filter_upwards with x; rfl)
41   rw [Measure.integral_compProd (bounded_test_integrable (μ ⊗ₘ κ) f hf h0 h1),
42     Measure.integral_compProd (bounded_test_integrable (μ ⊗ₘ η) f hf h0 h1),← integral_sub hFk hFe]
43   calc |∫ x,(∫ y,f (x,y)∂κ x)-(∫ y,f (x,y)∂η x)∂μ|≤
44       ∫ x,|(∫ y,f (x,y)∂κ x)-(∫ y,f (x,y)∂η x)|∂μ := abs_integral_le_integral_abs
45     _ ≤ ∫ x,KernelTVMeasurable.distance κ η x∂μ := by
46       apply integral_mono hd.abs (KernelTVMeasurable.distance_integrable κ η μ)
47       intro x
48       exact bounded_test_integral_le_tv (κ x) (η x) _
49         (hf.comp (measurable_const.prodMk measurable_id)) (fun y => h0 (x,y)) (fun y => h1 (x,y))
50 end KernelChange
51 
52 section CausalLaws
53 open ObservationLawKernels
54 variable {I A Y : Type*} [MeasurableSpace I] [MeasurableSpace A] [MeasurableSpace Y]
55 variable [StandardBorelSpace Y]
56 variable (π : Policy I A Y) (P Q : ObservationKernel I A Y)
57 variable [∀ n,IsMarkovKernel (π n)] [∀ n,IsMarkovKernel (P n)] [∀ n,IsMarkovKernel (Q n)]
58 
59 /-- The actual expected conditional discrepancy, under P's histories and policy actions. -/
60 noncomputable def drift (μ0 : Measure I) (t : ℕ) : ℝ :=
61   ∫ ha,KernelTVMeasurable.distance (P t) (Q t) ha∂policyPrefix π P μ0 t
62 
63 omit [StandardBorelSpace Y] [∀ n,IsMarkovKernel (π n)] in
64 theorem drift_nonneg (μ0 : Measure I) (t : ℕ) : 0≤drift π P Q μ0 t :=
65   integral_nonneg (fun ha => KernelTVMeasurable.distance_nonneg (P t) (Q t) ha)
66 
67 theorem drift_integrable (μ0 : Measure I) [IsProbabilityMeasure μ0] (t : ℕ) :
68     Integrable (fun ha => KernelTVMeasurable.distance (P t) (Q t) ha)
69       (policyPrefix π P μ0 t) :=
70   KernelTVMeasurable.distance_integrable (P t) (Q t) _
71 
72 /-- The expected error uses the actual P-history law, followed by the common
73 randomized action policy. -/
74 theorem drift_eq_iterated (μ0 : Measure I) [IsProbabilityMeasure μ0] (t : ℕ) :
75     drift π P Q μ0 t = ∫ h,∫ a,KernelTVMeasurable.distance (P t) (Q t) (h,a)
76       ∂π t h∂law π P μ0 t :=
77   Measure.integral_compProd (drift_integrable π P Q μ0 t)
78 
79 /-- The adjacent one-step hybrid uses the P prefix and the Q continuation.
80 Both contraction inequalities are derived for actual common Markov kernels. -/
81 theorem law_step (μ0 ν0 : Measure I) [IsProbabilityMeasure μ0] [IsProbabilityMeasure ν0] (n : ℕ) :
82     lawTV (law π P μ0 (n+1)) (law π Q ν0 (n+1))≤
83       lawTV (law π P μ0 n) (law π Q ν0 n)+drift π P Q μ0 n := by
84   have hmap := lawTV_map (((law π P μ0 n) ⊗ₘ π n) ⊗ₘ P n)
85     (((law π Q ν0 n) ⊗ₘ π n) ⊗ₘ Q n) (append n) (append_measurable n)
86   have htri := lawTV_triangle (((law π P μ0 n) ⊗ₘ π n) ⊗ₘ P n)
87     (((law π P μ0 n) ⊗ₘ π n) ⊗ₘ Q n) (((law π Q ν0 n) ⊗ₘ π n) ⊗ₘ Q n)
88   have hcost := compProd_change ((law π P μ0 n) ⊗ₘ π n) (P n) (Q n)
89   have hcont := (lawTV_compProd ((law π P μ0 n) ⊗ₘ π n) ((law π Q ν0 n) ⊗ₘ π n) (Q n)).trans
90     (lawTV_compProd (law π P μ0 n) (law π Q ν0 n) (π n))
91   calc lawTV (law π P μ0 (n+1)) (law π Q ν0 (n+1))≤
92       lawTV (((law π P μ0 n) ⊗ₘ π n) ⊗ₘ P n) (((law π Q ν0 n) ⊗ₘ π n) ⊗ₘ Q n) := hmap
93     _ ≤ lawTV (((law π P μ0 n) ⊗ₘ π n) ⊗ₘ P n) (((law π P μ0 n) ⊗ₘ π n) ⊗ₘ Q n)+
94         lawTV (((law π P μ0 n) ⊗ₘ π n) ⊗ₘ Q n) (((law π Q ν0 n) ⊗ₘ π n) ⊗ₘ Q n) := htri
95     _ ≤ drift π P Q μ0 n+lawTV (law π P μ0 n) (law π Q ν0 n) := add_le_add hcost hcont
96     _ = _ := add_comm _ _
97 
98 /-- Initial-history discrepancy adds its actual TV; every later cost is averaged
99 under P, including histories null under Q. -/
100 theorem lawTV_le_expected (μ0 ν0 : Measure I) [IsProbabilityMeasure μ0] [IsProbabilityMeasure ν0]
101     (n : ℕ) : lawTV (law π P μ0 n) (law π Q ν0 n)≤
102       min 1 (lawTV μ0 ν0+∑ t∈Finset.range n,drift π P Q μ0 t) := by
103   apply le_min (lawTV_le_one _ _)
104   induction n with
105   | zero =>
106     simp only [law,Finset.range_zero,Finset.sum_empty,add_zero]
107     exact lawTV_map μ0 ν0 (initial (A := A) (Y := Y)) initial_measurable
108   | succ n ih =>
109     calc lawTV (law π P μ0 (n+1)) (law π Q ν0 (n+1))≤
110         lawTV (law π P μ0 n) (law π Q ν0 n)+drift π P Q μ0 n := law_step π P Q μ0 ν0 n
111       _ ≤ (lawTV μ0 ν0+∑ t∈Finset.range n,drift π P Q μ0 t)+drift π P Q μ0 n :=
112         add_le_add ih le_rfl
113       _ = _ := by rw [Finset.sum_range_succ]; ring
114 
115 /-- The registered same-initial-history statement, with an actual initial law. -/
116 theorem lawTV_same_initial (μ0 : Measure I) [IsProbabilityMeasure μ0] (n : ℕ) :
117     lawTV (law π P μ0 n) (law π Q μ0 n)≤min 1 (∑ t∈Finset.range n,drift π P Q μ0 t) := by
118   simpa only [lawTV_self,zero_add] using lawTV_le_expected π P Q μ0 μ0 n
119 
120 theorem drift_le_uniform (μ0 : Measure I) [IsProbabilityMeasure μ0] (t : ℕ) (ε : ℝ)
121     (hε : ∀ h a,KernelTVMeasurable.distance (P t) (Q t) (h,a)≤ε) :
122     drift π P Q μ0 t≤ε := by
123   calc drift π P Q μ0 t≤∫ _ : History I A Y t × A,ε∂policyPrefix π P μ0 t :=
124       integral_mono (KernelTVMeasurable.distance_integrable (P t) (Q t) _)
125         (integrable_const _) (fun ha => hε ha.1 ha.2)
126     _ = ε := by simp
127 
128 /-- Uniform conditional budgets give the usual sum bound without any shared state. -/
129 theorem lawTV_le_uniform (μ0 ν0 : Measure I) [IsProbabilityMeasure μ0] [IsProbabilityMeasure ν0]
130     (ε : ℕ → ℝ) (hε : ∀ t h a,KernelTVMeasurable.distance (P t) (Q t) (h,a)≤ε t) (n : ℕ) :
131     lawTV (law π P μ0 n) (law π Q ν0 n)≤min 1 (lawTV μ0 ν0+∑ t∈Finset.range n,ε t) := by
132   apply (lawTV_le_expected π P Q μ0 ν0 n).trans
133   apply min_le_min le_rfl
134   exact add_le_add le_rfl (Finset.sum_le_sum (fun t _ => drift_le_uniform π P Q μ0 t (ε t) (hε t)))
135 
136 /-- Uniform budgets for the registered common-initial-history comparison. -/
137 theorem lawTV_same_initial_uniform (μ0 : Measure I) [IsProbabilityMeasure μ0]
138     (ε : ℕ → ℝ) (hε : ∀ t h a,KernelTVMeasurable.distance (P t) (Q t) (h,a)≤ε t) (n : ℕ) :
139     lawTV (law π P μ0 n) (law π Q μ0 n)≤min 1 (∑ t∈Finset.range n,ε t) := by
140   simpa only [lawTV_self,zero_add] using lawTV_le_uniform π P Q μ0 μ0 ε hε n
141 
142 /-- A fixed initial history is the point-mass special case of the same-law bound. -/
143 theorem lawTV_fixed_history (i : I) (n : ℕ) :
144     lawTV (law π P (Measure.dirac i) n) (law π Q (Measure.dirac i) n)≤
145       min 1 (∑ t∈Finset.range n,drift π P Q (Measure.dirac i) t) :=
146   lawTV_same_initial π P Q (Measure.dirac i) n
147 
148 /-- Every measurable observation-only readout of the record inherits the budget. -/
149 theorem lawTV_readout {Z : Type*} [MeasurableSpace Z]
150     (μ0 ν0 : Measure I) [IsProbabilityMeasure μ0] [IsProbabilityMeasure ν0]
151     (n : ℕ) (readout : History I A Y n → Z) (hr : Measurable readout) :
152     lawTV ((law π P μ0 n).map readout) ((law π Q ν0 n).map readout)≤
153       min 1 (lawTV μ0 ν0+∑ t∈Finset.range n,drift π P Q μ0 t) :=
154   (lawTV_map _ _ readout hr).trans (lawTV_le_expected π P Q μ0 ν0 n)
155 
156 end CausalLaws
157 end Komorebi.LSM.ObservationLawComparison

Back to source controls