PolicyComparison.lean

1 import KomorebiLSM.ObservationTree
2 
3 /-! P43 includes shared randomized history-dependent policies.
4 The weights multiply complete instruments, not separately selected branches. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.ObservationTree
7 open scoped BigOperators
8 open BaseNorm FiniteBayes
9 variable {E A O : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
10 variable [Fintype A] [Fintype O] (C : ProbabilityCone E)
11 
12 noncomputable def policyBranches (π : List (A × O) → A → ℝ)
13     (B : List (A × O) → A × O → E →ₗ[ℝ] E) (h : List (A × O))
14     (s : A × O) : E →ₗ[ℝ] E := π h s.1 • B h s
15 
16 theorem policy_instrument (π : List (A × O) → A → ℝ) (hπ : ∀ h, IsPrior (π h))
17     (B : List (A × O) → A × O → E →ₗ[ℝ] E)
18     (hB : ∀ h a, C.Instrument (fun o => B h (a,o))) (h : List (A × O)) :
19     C.Instrument (policyBranches π B h) := by
20   constructor
21   · intro s x hx
22     exact C.smul_mem ((hπ h).1 s.1) ((hB h s.1).1 s.2 x hx)
23   · intro x
24     change (∑ s : A × O, C.mass (π h s.1 • B h s x))=C.mass x
25     rw [Fintype.sum_prod_type]
26     simp only [map_smul,smul_eq_mul,← Finset.mul_sum]
27     simp_rw [(hB h _).2 x]
28     rw [← Finset.sum_mul,(hπ h).2,one_mul]
29 
30 /-- Zero policy probabilities are permitted. No lower propensity is needed for comparison. -/
31 theorem policy_discrepancy (π : List (A × O) → A → ℝ) (hπ : ∀ h, IsPrior (π h))
32     (B D : List (A × O) → A × O → E →ₗ[ℝ] E) (ε : ℕ → ℝ)
33     (hε : ∀ h a z, z ∈ C.base →
34       C.discrepancy (fun o => B h (a,o)) (fun o => D h (a,o)) z ≤ ε h.length)
35     (h : List (A × O)) (z : E) (hz : z ∈ C.base) :
36     C.discrepancy (policyBranches π B h) (policyBranches π D h) z ≤ ε h.length := by
37   calc
38     _ = ∑ a, π h a*C.discrepancy (fun o => B h (a,o)) (fun o => D h (a,o)) z := by
39       unfold ProbabilityCone.discrepancy
40       rw [Fintype.sum_prod_type]
41       apply Finset.sum_congr rfl
42       intro a _
43       rw [Finset.mul_sum]
44       apply Finset.sum_congr rfl
45       intro o _
46       have he : (policyBranches π B h (a,o)-policyBranches π D h (a,o)) z =
47           π h a • ((B h (a,o)-D h (a,o)) z) := by
48         simp only [policyBranches,LinearMap.sub_apply,LinearMap.smul_apply,smul_sub]
49       rw [he,C.value_smul_of_nonneg ((hπ h).1 a)]
50     _ ≤ ∑ a, π h a*ε h.length :=
51       Finset.sum_le_sum (fun a _ => mul_le_mul_of_nonneg_left (hε h a z hz) ((hπ h).1 a))
52     _ = ε h.length := by rw [← Finset.sum_mul,(hπ h).2,one_mul]
53 
54 /-- P43 for the actual joint distribution of action and observation records. -/
55 theorem shared_randomized_policy_tv_bound
56     (π : List (A × O) → A → ℝ) (hπ : ∀ h, IsPrior (π h))
57     (B D : List (A × O) → A × O → E →ₗ[ℝ] E)
58     (hB : ∀ h a, C.Instrument (fun o => B h (a,o)))
59     (hD : ∀ h a, C.Instrument (fun o => D h (a,o)))
60     (ε : ℕ → ℝ) (hε : ∀ h a z, z ∈ C.base →
61       C.discrepancy (fun o => B h (a,o)) (fun o => D h (a,o)) z ≤ ε h.length)
62     (n : ℕ) (x y : E) (hx : x ∈ C.base) (hy : y ∈ C.base) :
63     FiniteTV.distance (recordLaw C (policyBranches π B) n [] x)
64       (recordLaw C (policyBranches π D) n [] y) ≤
65       min 1 (C.value (x-y)/2+(∑ t ∈ Finset.range n, ε t)/2) :=
66   observation_tree_tv_bound C _ _ (policy_instrument C π hπ B hB)
67     (policy_instrument C π hπ D hD) ε (policy_discrepancy C π hπ B D ε hε) n x y hx hy
68 
69 /-- The observation-only distribution is the pushforward forgetting actions. -/
70 noncomputable def observationLaw (π : List (A × O) → A → ℝ)
71     (B : List (A × O) → A × O → E →ₗ[ℝ] E) (n : ℕ) (x : E) : Record O n → ℝ := by
72   classical
73   exact aggregate (recordMap Prod.snd) (recordLaw C (policyBranches π B) n [] x)
74 
75 /-- The same bound holds after action coordinates have been summed out. -/
76 theorem shared_policy_observation_tv_bound
77     (π : List (A × O) → A → ℝ) (hπ : ∀ h, IsPrior (π h))
78     (B D : List (A × O) → A × O → E →ₗ[ℝ] E)
79     (hB : ∀ h a, C.Instrument (fun o => B h (a,o)))
80     (hD : ∀ h a, C.Instrument (fun o => D h (a,o)))
81     (ε : ℕ → ℝ) (hε : ∀ h a z, z ∈ C.base →
82       C.discrepancy (fun o => B h (a,o)) (fun o => D h (a,o)) z ≤ ε h.length)
83     (n : ℕ) (x y : E) (hx : x ∈ C.base) (hy : y ∈ C.base) :
84     FiniteTV.distance (observationLaw C π B n x) (observationLaw C π D n y) ≤
85       min 1 (C.value (x-y)/2+(∑ t ∈ Finset.range n, ε t)/2) := by
86   classical
87   exact (FiniteTV.distance_aggregate_le (recordMap Prod.snd) _ _).trans
88     (shared_randomized_policy_tv_bound C π hπ B D hB hD ε hε n x y hx hy)
89 
90 /-- The P42 supremum directly supplies both full-law bounds, with the same policy. -/
91 theorem shared_policy_instrumentError_bounds
92     (π : List (A × O) → A → ℝ) (hπ : ∀ h, IsPrior (π h))
93     (B D : List (A × O) → A × O → E →ₗ[ℝ] E)
94     (hB : ∀ h a, C.Instrument (fun o => B h (a,o)))
95     (hD : ∀ h a, C.Instrument (fun o => D h (a,o)))
96     (ε : ℕ → ℝ) (hε : ∀ h a,
97       C.instrumentError (fun o => B h (a,o)) (fun o => D h (a,o)) ≤ ε h.length)
98     (n : ℕ) (x y : E) (hx : x ∈ C.base) (hy : y ∈ C.base) :
99     FiniteTV.distance (recordLaw C (policyBranches π B) n [] x)
100       (recordLaw C (policyBranches π D) n [] y) ≤
101         min 1 (C.value (x-y)/2+(∑ t ∈ Finset.range n, ε t)/2) ∧
102     FiniteTV.distance (observationLaw C π B n x) (observationLaw C π D n y) ≤
103         min 1 (C.value (x-y)/2+(∑ t ∈ Finset.range n, ε t)/2) := by
104   have hp : ∀ h a z, z ∈ C.base →
105       C.discrepancy (fun o => B h (a,o)) (fun o => D h (a,o)) z ≤ ε h.length := by
106     intro h a z hz
107     exact (C.discrepancy_le_instrumentError _ _ (hB h a) (hD h a) hz).trans (hε h a)
108   exact ⟨shared_randomized_policy_tv_bound C π hπ B D hB hD ε hp n x y hx hy,
109     shared_policy_observation_tv_bound C π hπ B D hB hD ε hp n x y hx hy⟩
110 
111 /-- Deterministic policies are included as point-mass randomizations. -/
112 noncomputable def deterministicPolicy (π : List (A × O) → A) (h : List (A × O)) : A → ℝ := by
113   classical
114   exact pointMass (π h)
115 
116 omit [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype O] in
117 theorem deterministicPolicy_prior (π : List (A × O) → A) (h : List (A × O)) :
118     IsPrior (deterministicPolicy π h) := by
119   classical
120   exact FiniteInstruments.point_prior (π h)
121 
122 end Komorebi.LSM.ObservationTree

Back to source controls