Block7Examples.lean

1 import KomorebiLSM.BaseNormModels
2 import KomorebiLSM.PolicyComparison
3 import KomorebiLSM.SharpConditioning
4 
5 /-! Exact examples separate whole-record distance, conditioning, and signed coordinates. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.Block7Examples
8 open scoped BigOperators
9 open BaseNorm FiniteTV FiniteBayes FiniteInstruments ObservationTree
10 
11 noncomputable def bernoulli (p : ℝ) (o : Fin 2) : ℝ →ₗ[ℝ] ℝ :=
12   (![1-p,p] o) • LinearMap.id
13 
14 theorem bernoulli_instrument (p : ℝ) (hp : 0 ≤ p) (h1 : p ≤ 1) :
15     scalarCone.Instrument (bernoulli p) := by
16   constructor
17   · intro o x hx
18     change 0 ≤ x at hx
19     change 0 ≤ (![1-p,p] o)*x
20     apply mul_nonneg _ hx
21     fin_cases o <;> simp <;> linarith
22   · intro x
23     change (∑ o : Fin 2, (![1-p,p] o)*x)=x
24     simp only [Fin.sum_univ_two,Matrix.cons_val_zero,Matrix.cons_val_one]
25     ring
26 
27 theorem scalar_initial : (1 : ℝ) ∈ scalarCone.base := by
28   constructor
29   · change (0 : ℝ) ≤ 1; norm_num
30   · rfl
31 
32 theorem scalar_base_eq_one {x : ℝ} (hx : x ∈ scalarCone.base) : x=1 := hx.2
33 
34 theorem bernoulli_discrepancy (p q : ℝ) :
35     scalarCone.discrepancy (bernoulli p) (bernoulli q) 1=2*|p-q| := by
36   unfold ProbabilityCone.discrepancy
37   simp only [Fin.sum_univ_two,LinearMap.sub_apply,bernoulli,LinearMap.smul_apply,
38     LinearMap.id_apply,smul_eq_mul,mul_one,scalar_value]
39   have he : 1-p-(1-q)=-(p-q) := by ring
40   simp only [Matrix.cons_val_zero,Matrix.cons_val_one,he,abs_neg]
41   ring
42 
43 theorem bernoulli_instrumentError (p q : ℝ) :
44     scalarCone.instrumentError (bernoulli p) (bernoulli q)=2*|p-q| := by
45   unfold ProbabilityCone.instrumentError
46   have he : scalarCone.discrepancy (bernoulli p) (bernoulli q) '' scalarCone.base =
47       {2*|p-q|} := by
48     ext r
49     constructor
50     · rintro ⟨x,hx,rfl⟩
51       rw [scalar_base_eq_one hx,bernoulli_discrepancy]
52       exact Set.mem_singleton _
53     · intro hr
54       have hr' : r=2*|p-q| := hr
55       exact ⟨1,scalar_initial,(bernoulli_discrepancy p q).trans hr'.symm⟩
56   rw [he,csSup_singleton]
57 
58 /-- The general theorem supplies a bound for every horizon, not a tested maximum length. -/
59 theorem bernoulli_record_bound (p q : ℝ) (hp : 0 ≤ p) (hp1 : p ≤ 1)
60     (hq : 0 ≤ q) (hq1 : q ≤ 1) (n : ℕ) :
61     distance (recordLaw scalarCone (fun _ => bernoulli p) n [] 1)
62       (recordLaw scalarCone (fun _ => bernoulli q) n [] 1) ≤ min 1 (n*|p-q|) := by
63   have he : ∀ (h : List (Fin 2)) x, x ∈ scalarCone.base →
64       scalarCone.discrepancy (bernoulli p) (bernoulli q) x ≤ (fun _ : ℕ => 2*|p-q|) h.length := by
65     intro h x hx
66     rw [scalar_base_eq_one hx,bernoulli_discrepancy]
67   have hb := observation_tree_tv_bound scalarCone (fun _ => bernoulli p) (fun _ => bernoulli q)
68     (fun _ => bernoulli_instrument p hp hp1) (fun _ => bernoulli_instrument q hq hq1)
69     (fun _ => 2*|p-q|) he n 1 1 scalar_initial scalar_initial
70   simpa only [sub_self,ProbabilityCone.value_zero,zero_div,zero_add,Finset.sum_const,
71     Finset.card_range,nsmul_eq_mul,mul_div_assoc,mul_div_cancel_left₀ _ (by norm_num : (2:ℝ) ≠ 0)] using hb
72 
73 theorem bernoulli_quarter_two_step :
74     distance (recordLaw scalarCone (fun _ => bernoulli (1/4)) 2 [] 1)
75       (recordLaw scalarCone (fun _ => bernoulli (1/2)) 2 [] 1)=5/16 := by
76   unfold distance l1
77   simp_rw [Pi.sub_apply,sum_record_succ,sum_record_zero]
78   norm_num [recordLaw,recordState,Fin.sum_univ_two,bernoulli,scalarCone]
79 
80 theorem bernoulli_zero_half_one_step :
81     distance (recordLaw scalarCone (fun _ => bernoulli 0) 1 [] 1)
82       (recordLaw scalarCone (fun _ => bernoulli (1/2)) 1 [] 1)=1/2 := by
83   unfold distance l1
84   simp_rw [Pi.sub_apply,sum_record_succ,sum_record_zero]
85   norm_num [recordLaw,recordState,Fin.sum_univ_two,bernoulli,scalarCone]
86 
87 theorem bernoulli_zero_half_two_step :
88     distance (recordLaw scalarCone (fun _ => bernoulli 0) 2 [] 1)
89       (recordLaw scalarCone (fun _ => bernoulli (1/2)) 2 [] 1)=3/4 := by
90   unfold distance l1
91   simp_rw [Pi.sub_apply,sum_record_succ,sum_record_zero]
92   norm_num [recordLaw,recordState,Fin.sum_univ_two,bernoulli,scalarCone]
93 
94 theorem one_step_error_is_not_full_record_bound :
95     ¬ distance (recordLaw scalarCone (fun _ => bernoulli 0) 2 [] 1)
96       (recordLaw scalarCone (fun _ => bernoulli (1/2)) 2 [] 1) ≤ 1/2 := by
97   rw [bernoulli_zero_half_two_step]; norm_num
98 
99 /-- Zero-likelihood branches do not obstruct an unnormalized whole-law guarantee. -/
100 theorem zero_branch_record_is_prior (n : ℕ) :
101     IsPrior (recordLaw scalarCone (fun _ => bernoulli 0) n [] 1) :=
102   record_prior scalarCone _ (fun _ => bernoulli_instrument 0 (by norm_num) (by norm_num))
103     n [] 1 scalar_initial
104 
105 theorem rare_event_unconditional_distance :
106     distance (sharpP (1/100)) (sharpQ (1/100) (1/200))=1/200 :=
107   sharp_distance _ _ (by norm_num)
108 
109 theorem rare_event_conditional_distance :
110     distance (conditional (sharpP (1/100)) sharpEvent)
111       (conditional (sharpQ (1/100) (1/200)) sharpEvent)=1/2 := by
112   rw [sharp_conditional_distance _ _ (by norm_num) (by norm_num)]; norm_num
113 
114 theorem rare_event_attains_bound :
115     distance (conditional (sharpP (1/100)) sharpEvent)
116       (conditional (sharpQ (1/100) (1/200)) sharpEvent) =
117       distance (sharpP (1/100)) (sharpQ (1/100) (1/200)) /
118         eventMass (sharpP (1/100)) sharpEvent := by
119   rw [rare_event_conditional_distance,rare_event_unconditional_distance,sharpP_eventMass]
120   norm_num
121 
122 theorem missing_event_is_zero : eventMass (sharpP 0) sharpEvent=0 := sharpP_eventMass 0
123 
124 theorem missing_event_conditional_not_prior : ¬ IsPrior (conditional (sharpP 0) sharpEvent) := by
125   intro h
126   have hz : conditional (sharpP 0) sharpEvent=0 := by
127     unfold conditional FiniteInstruments.normalize
128     rw [restrict_mass,sharpP_eventMass]; simp
129   rw [hz] at h
130   have ht := h.2
131   norm_num at ht
132 
133 theorem signed_mass_zero : mass (![1,-1] : Fin 2 → ℝ)=0 := by
134   norm_num [mass_apply,Fin.sum_univ_two]
135 
136 theorem signed_base_norm_two : (orthant (Fin 2)).value (![1,-1])=2 := by
137   rw [orthant_value]; norm_num [l1,Fin.sum_univ_two]
138 
139 theorem signed_vector_not_positive : ¬ (![1,-1] : Fin 2 → ℝ) ∈ (orthant (Fin 2)).carrier := by
140   rw [orthant_carrier]
141   intro h
142   have ht := h 1
143   norm_num at ht
144 
145 /-- Aggregation can erase signed contrast without violating its contraction theorem. -/
146 theorem aggregation_can_strictly_contract :
147     l1 (aggregate (fun _ : Fin 2 => ()) (![1,-1] : Fin 2 → ℝ))=0 ∧
148     l1 (![1,-1] : Fin 2 → ℝ)=2 := by
149   norm_num [l1,aggregate,Fin.sum_univ_two]
150 
151 end Komorebi.LSM.Block7Examples

Back to source controls