ObservationTree.lean

1 import KomorebiLSM.InstrumentContraction
2 import KomorebiLSM.FiniteTV
3 
4 /-! P43: actual finite records and their unnormalized state trees.
5 Every horizon is proved by induction, without a branch-likelihood lower bound. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.ObservationTree
8 open scoped BigOperators
9 open BaseNorm FiniteBayes
10 
11 universe u
12 /-- Chronological fixed-length records. -/
13 def Record (O : Type u) : ℕ → Type u
14   | 0 => PUnit.{u+1}
15   | n+1 => O × Record O n
16 
17 instance recordFintype {O : Type*} [Fintype O] : (n : ℕ) → Fintype (Record O n)
18   | 0 => inferInstanceAs (Fintype PUnit)
19   | n+1 => by
20     letI : Fintype (Record O n) := recordFintype n
21     exact inferInstanceAs (Fintype (O × Record O n))
22 
23 theorem sum_record_zero {O : Type*} [Fintype O] (f : Record O 0 → ℝ) :
24     (∑ w, f w)=f PUnit.unit := by
25   let : Unique (Record O 0) := inferInstanceAs (Unique PUnit)
26   exact Fintype.sum_unique f
27 
28 theorem sum_record_succ {O : Type*} [Fintype O] (n : ℕ) (f : Record O (n+1) → ℝ) :
29     (∑ w, f w)=∑ o, ∑ v : Record O n, f (o,v) := by
30   change (∑ w : O × Record O n, f w)=_
31   exact Fintype.sum_prod_type f
32 
33 theorem record_pair_eq_iff {O : Type*} {n : ℕ} (a b : O) (v w : Record O n) :
34     (show Record O (n+1) from (a,v))=(b,w) ↔ a=b ∧ v=w := by
35   constructor
36   · intro h; exact ⟨congrArg Prod.fst h,congrArg Prod.snd h⟩
37   · rintro ⟨rfl,rfl⟩; rfl
38 
39 def recordList {O : Type*} : {n : ℕ} → Record O n → List O
40   | 0, _ => []
41   | _+1, w => w.1 :: recordList w.2
42 
43 theorem recordList_length {O : Type*} (n : ℕ) (w : Record O n) : (recordList w).length=n := by
44   induction n with
45   | zero => rfl
46   | succ n ih => exact congrArg Nat.succ (ih w.2)
47 
48 def recordMap {O J : Type*} (f : O → J) : {n : ℕ} → Record O n → Record J n
49   | 0, _ => PUnit.unit
50   | _+1, w => (f w.1,recordMap f w.2)
51 
52 variable {E O : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
53 variable [Fintype O] (C : ProbabilityCone E)
54 
55 /-- The next map is selected using the complete chronological prefix. -/
56 def recordState (B : List O → O → E →ₗ[ℝ] E) :
57     (n : ℕ) → List O → E → Record O n → E
58   | 0, _, x, _ => x
59   | n+1, h, x, w => recordState B n (h ++ [w.1]) (B h w.1 x) w.2
60 
61 noncomputable def recordLaw (B : List O → O → E →ₗ[ℝ] E) (n : ℕ) (h : List O) (x : E) :
62     Record O n → ℝ := fun w => C.mass (recordState B n h x w)
63 
64 theorem recordState_mem (B : List O → O → E →ₗ[ℝ] E)
65     (hB : ∀ h, C.Instrument (B h)) (n : ℕ) (h : List O) (x : E) (hx : x ∈ C.carrier)
66     (w : Record O n) : recordState B n h x w ∈ C.carrier := by
67   induction n generalizing h x with
68   | zero => exact hx
69   | succ n ih => exact ih _ _ ((hB h).1 w.1 x hx) w.2
70 
71 theorem record_mass (B : List O → O → E →ₗ[ℝ] E)
72     (hB : ∀ h, C.Instrument (B h)) (n : ℕ) (h : List O) (x : E) :
73     ∑ w, recordLaw C B n h x w=C.mass x := by
74   induction n generalizing h x with
75   | zero =>
76     change (∑ _ : PUnit, C.mass x)=C.mass x
77     simp
78   | succ n ih =>
79     change (∑ w : O × Record O n, recordLaw C B n (h++[w.1]) (B h w.1 x) w.2)=C.mass x
80     rw [Fintype.sum_prod_type]
81     simp_rw [ih]
82     exact (hB h).2 x
83 
84 theorem record_prior (B : List O → O → E →ₗ[ℝ] E)
85     (hB : ∀ h, C.Instrument (B h)) (n : ℕ) (h : List O) (x : E) (hx : x ∈ C.base) :
86     IsPrior (recordLaw C B n h x) :=
87   ⟨fun w => C.mass_nonneg (recordState_mem C B hB n h x hx.1 w),
88     (record_mass C B hB n h x).trans hx.2⟩
89 
90 noncomputable def tailBudget (ε : ℕ → ℝ) (t n : ℕ) : ℝ := ∑ k ∈ Finset.range n, ε (t+k)
91 
92 theorem tailBudget_succ (ε : ℕ → ℝ) (t n : ℕ) :
93     tailBudget ε t (n+1)=ε t+tailBudget ε (t+1) n := by
94   unfold tailBudget
95   rw [Finset.sum_range_succ']
96   simp only [Nat.add_zero]
97   rw [add_comm]
98   congr 1
99   apply Finset.sum_congr rfl
100   intro k _
101   congr 1
102   omega
103 
104 /-- The central positive-mass-weighted tree induction. -/
105 theorem record_state_error (B D : List O → O → E →ₗ[ℝ] E)
106     (hB : ∀ h, C.Instrument (B h)) (hD : ∀ h, C.Instrument (D h))
107     (ε : ℕ → ℝ) (hε : ∀ h z, z ∈ C.base → C.discrepancy (B h) (D h) z ≤ ε h.length)
108     (n : ℕ) (h : List O) (x y : E) (hy : y ∈ C.carrier) :
109     (∑ w, C.value (recordState B n h x w-recordState D n h y w)) ≤
110       C.value (x-y)+C.mass y*tailBudget ε h.length n := by
111   induction n generalizing h x y with
112   | zero =>
113     change (∑ _ : PUnit, C.value (x-y)) ≤ _
114     simp [tailBudget]
115   | succ n ih =>
116     change (∑ w : O × Record O n, C.value
117       (recordState B n (h++[w.1]) (B h w.1 x) w.2-
118        recordState D n (h++[w.1]) (D h w.1 y) w.2)) ≤ _
119     rw [Fintype.sum_prod_type]
120     calc
121       _ ≤ ∑ o, (C.value (B h o x-D h o y)+
122           C.mass (D h o y)*tailBudget ε (h.length+1) n) := by
123         apply Finset.sum_le_sum
124         intro o _
125         simpa only [List.length_append,List.length_singleton] using
126           ih (h++[o]) (B h o x) (D h o y) ((hD h).1 o y hy)
127       _ = (∑ o, C.value (B h o x-D h o y))+C.mass y*tailBudget ε (h.length+1) n := by
128         rw [Finset.sum_add_distrib,← Finset.sum_mul,(hD h).2]
129       _ ≤ C.value (x-y)+ε h.length*C.mass y+C.mass y*tailBudget ε (h.length+1) n :=
130         add_le_add (C.instrument_pair_step (B h) (D h) (hB h) (ε h.length) (hε h) x hy) le_rfl
131       _ = C.value (x-y)+C.mass y*tailBudget ε h.length (n+1) := by
132         rw [tailBudget_succ]
133         ring
134 
135 /-- Total variation is bounded by the summed unnormalized state differences. -/
136 theorem record_l1_le_state_error (B D : List O → O → E →ₗ[ℝ] E)
137     (n : ℕ) (h : List O) (x y : E) :
138     FiniteTV.l1 (recordLaw C B n h x-recordLaw C D n h y) ≤
139       ∑ w, C.value (recordState B n h x w-recordState D n h y w) := by
140   unfold FiniteTV.l1
141   apply Finset.sum_le_sum
142   intro w _
143   simpa only [recordLaw,Pi.sub_apply,map_sub] using C.abs_mass_le (recordState B n h x w-recordState D n h y w)
144 
145 /-- P43 for arbitrary history-dependent finite branch families. -/
146 theorem observation_tree_tv_bound (B D : List O → O → E →ₗ[ℝ] E)
147     (hB : ∀ h, C.Instrument (B h)) (hD : ∀ h, C.Instrument (D h))
148     (ε : ℕ → ℝ) (hε : ∀ h z, z ∈ C.base → C.discrepancy (B h) (D h) z ≤ ε h.length)
149     (n : ℕ) (x y : E) (hx : x ∈ C.base) (hy : y ∈ C.base) :
150     FiniteTV.distance (recordLaw C B n [] x) (recordLaw C D n [] y) ≤
151       min 1 (C.value (x-y)/2+(∑ t ∈ Finset.range n, ε t)/2) := by
152   apply le_min
153   · exact FiniteTV.distance_le_one _ _ (record_prior C B hB n [] x hx) (record_prior C D hD n [] y hy)
154   · have hb := (record_l1_le_state_error C B D n [] x y).trans
155       (record_state_error C B D hB hD ε hε n [] x y hy.1)
156     simp only [hy.2,one_mul,List.length_nil,tailBudget,Nat.zero_add] at hb
157     unfold FiniteTV.distance
158     linarith
159 
160 end Komorebi.LSM.ObservationTree

Back to source controls