ObservationLawKernels.lean

1 import KomorebiLSM.ContinuousRecords
2 import Mathlib.Probability.Kernel.Composition.IntegralCompProd
3 
4 /-! Actual finite causal record laws from total history-indexed observation
5 kernels and a common measurable action-policy kernel. No latent state is used. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.ObservationLawKernels
8 open MeasureTheory ProbabilityTheory
9 open scoped ENNReal
10 variable {I A Y : Type*} [MeasurableSpace I] [MeasurableSpace A] [MeasurableSpace Y]
11 
12 abbrev History (I A Y : Type*) (n : ℕ) := I × ContinuousRecords.History (A × Y) n
13 
14 def initial (i : I) : History I A Y 0 := (i,PUnit.unit)
15 
16 def append (n : ℕ) (r : (History I A Y n × A) × Y) : History I A Y (n+1) :=
17   (r.1.1.1,(r.1.1.2,(r.1.2,r.2)))
18 
19 def drop (n : ℕ) (h : History I A Y (n+1)) : History I A Y n := (h.1,h.2.1)
20 
21 omit [MeasurableSpace A] [MeasurableSpace Y] in
22 theorem initial_measurable : Measurable (initial (I := I) (A := A) (Y := Y)) :=
23   measurable_id.prodMk measurable_const
24 
25 theorem append_measurable (n : ℕ) : Measurable (append (I := I) (A := A) (Y := Y) n) :=
26   ((measurable_fst.comp measurable_fst).comp measurable_fst).prodMk
27     (((measurable_snd.comp measurable_fst).comp measurable_fst).prodMk
28       ((measurable_snd.comp measurable_fst).prodMk measurable_snd))
29 
30 theorem drop_measurable (n : ℕ) : Measurable (drop (I := I) (A := A) (Y := Y) n) :=
31   measurable_fst.prodMk (measurable_fst.comp measurable_snd)
32 
33 /-- Policies are actual Markov kernels on the full recorded history. -/
34 abbrev Policy (I A Y : Type*) [MeasurableSpace I] [MeasurableSpace A] [MeasurableSpace Y] :=
35   (n : ℕ) → Kernel (History I A Y n) A
36 
37 /-- An observation kernel is defined on every history and action, including
38 histories null under its own generated law. -/
39 abbrev ObservationKernel (I A Y : Type*) [MeasurableSpace I] [MeasurableSpace A] [MeasurableSpace Y] :=
40   (n : ℕ) → Kernel (History I A Y n × A) Y
41 
42 variable (π : Policy I A Y) (P : ObservationKernel I A Y)
43 
44 /-- Choose an action, then an observation, and append both to the actual record. -/
45 noncomputable def law (μ0 : Measure I) : (n : ℕ) → Measure (History I A Y n)
46   | 0 => μ0.map initial
47   | n+1 => (((law μ0 n) ⊗ₘ π n) ⊗ₘ P n).map (append n)
48 
49 variable [∀ n,IsMarkovKernel (π n)] [∀ n,IsMarkovKernel (P n)]
50 
51 theorem law_probability_aux (μ0 : Measure I) [IsProbabilityMeasure μ0] :
52     (n : ℕ) → IsProbabilityMeasure (law π P μ0 n)
53   | 0 => inferInstanceAs (IsProbabilityMeasure (μ0.map initial))
54   | n+1 => by
55     have := law_probability_aux μ0 n
56     exact inferInstanceAs (IsProbabilityMeasure ((((law π P μ0 n) ⊗ₘ π n) ⊗ₘ P n).map (append n)))
57 
58 instance law_probability (μ0 : Measure I) [IsProbabilityMeasure μ0] (n : ℕ) :
59     IsProbabilityMeasure (law π P μ0 n) := law_probability_aux π P μ0 n
60 
61 instance law_zero_probability (μ0 : Measure I) [IsProbabilityMeasure μ0] :
62     IsProbabilityMeasure (law π P μ0 0) := law_probability_aux π P μ0 0
63 
64 /-- The explicit successor instance keeps the recursively expanded history type
65 visible to instance search. -/
66 instance law_succ_probability (μ0 : Measure I) [IsProbabilityMeasure μ0] (n : ℕ) :
67     IsProbabilityMeasure (law π P μ0 (n+1)) := law_probability_aux π P μ0 (n+1)
68 
69 /-- The policy-chosen action has the actual current P-history distribution. -/
70 noncomputable def policyPrefix (μ0 : Measure I) (n : ℕ) : Measure (History I A Y n × A) :=
71   (law π P μ0 n) ⊗ₘ π n
72 
73 instance policyPrefix_probability (μ0 : Measure I) [IsProbabilityMeasure μ0] (n : ℕ) :
74     IsProbabilityMeasure (policyPrefix π P μ0 n) := by
75   unfold policyPrefix
76   infer_instance
77 
78 /-- Marginal consistency follows from normalized kernels and the actual append map. -/
79 theorem law_consistent (μ0 : Measure I) [IsProbabilityMeasure μ0] (n : ℕ) :
80     (law π P μ0 (n+1)).map (drop n)=law π P μ0 n := by
81   change (((((law π P μ0 n) ⊗ₘ π n) ⊗ₘ P n).map (append n)).map (drop n))=_
82   rw [Measure.map_map (drop_measurable n) (append_measurable n)]
83   have he : (drop (I := I) (A := A) (Y := Y) n) ∘ append n=Prod.fst ∘ Prod.fst := rfl
84   rw [he,← Measure.map_map measurable_fst measurable_fst]
85   change (((law π P μ0 n) ⊗ₘ π n) ⊗ₘ P n).fst.fst=_
86   rw [Measure.fst_compProd,Measure.fst_compProd]
87 
88 /-- The defining joint law has the chronological iterated-kernel integral. -/
89 theorem lintegral_law_succ (μ0 : Measure I) [IsProbabilityMeasure μ0] (n : ℕ)
90     (f : History I A Y (n+1) → ℝ≥0∞) (hf : Measurable f) :
91     (∫⁻ h,f h∂law π P μ0 (n+1))=
92       ∫⁻ h,∫⁻ a,∫⁻ y,f (append n ((h,a),y))∂P n (h,a)∂π n h∂law π P μ0 n := by
93   have hm : Measurable (fun r : (History I A Y n × A) × Y => f (append n r)) :=
94     hf.comp (append_measurable n)
95   calc (∫⁻ h,f h∂law π P μ0 (n+1))=
96       ∫⁻ r,f (append n r)∂((law π P μ0 n) ⊗ₘ π n) ⊗ₘ P n :=
97         lintegral_map (μ := ((law π P μ0 n) ⊗ₘ π n) ⊗ₘ P n) hf (append_measurable n)
98     _ = ∫⁻ ha,∫⁻ y,f (append n (ha,y))∂P n ha∂(law π P μ0 n) ⊗ₘ π n :=
99       Measure.lintegral_compProd hm
100     _ = _ := Measure.lintegral_compProd (hm.lintegral_kernel_prod_right' (κ := P n))
101 
102 end Komorebi.LSM.ObservationLawKernels

Back to source controls