Block7BoundaryExamples.lean

1 import KomorebiLSM.Block7Examples
2 
3 /-! Exact boundaries for shared policies and redundant coefficient choices. -/
4 set_option autoImplicit false
5 namespace Komorebi.LSM.Block7BoundaryExamples
6 open scoped BigOperators
7 open BaseNorm FiniteTV FiniteBayes FiniteInstruments ObservationTree PositiveLift Block7Examples
8 
9 /-- The same physical instrument reports the chosen action deterministically. -/
10 noncomputable def echo (_ : List (Fin 2 × Fin 2)) (s : Fin 2 × Fin 2) : ℝ →ₗ[ℝ] ℝ :=
11   if s.1=s.2 then LinearMap.id else 0
12 
13 theorem echo_instrument (h : List (Fin 2 × Fin 2)) (a : Fin 2) :
14     scalarCone.Instrument (fun o => echo h (a,o)) := by
15   constructor
16   · intro o x hx
17     by_cases hae : a=o
18     · simpa [echo,hae] using hx
19     · simpa [echo,hae] using scalarCone.zero_mem
20   · intro x
21     fin_cases a <;> simp [echo,Fin.sum_univ_two,scalarCone]
22 
23 noncomputable def fixedPolicy (a : Fin 2) : List (Fin 2 × Fin 2) → Fin 2 → ℝ :=
24   deterministicPolicy (fun _ => a)
25 
26 theorem fixedPolicy_prior (a : Fin 2) (h : List (Fin 2 × Fin 2)) :
27     IsPrior (fixedPolicy a h) := deterministicPolicy_prior (fun _ => a) h
28 
29 theorem one_record_eq (a b : Fin 2) :
30     (show Record (Fin 2) 1 from (a,PUnit.unit))=(b,PUnit.unit) ↔ a=b := by
31   constructor
32   · intro h; exact congrArg Prod.fst h
33   · intro h; subst b; rfl
34 
35 theorem recordMap_one_eq (a o b : Fin 2) :
36     recordMap Prod.snd (show Record (Fin 2 × Fin 2) 1 from ((a,o),PUnit.unit)) =
37       (show Record (Fin 2) 1 from (b,PUnit.unit)) ↔ o=b := by
38   exact one_record_eq o b
39 
40 theorem changed_policy_observation_distance :
41     distance (observationLaw scalarCone (fixedPolicy 0) echo 1 1)
42       (observationLaw scalarCone (fixedPolicy 1) echo 1 1)=1 := by
43   unfold distance l1 observationLaw aggregate
44   simp_rw [Pi.sub_apply,sum_record_succ,sum_record_zero]
45   simp_rw [Fintype.sum_prod_type]
46   simp_rw [recordMap_one_eq]
47   norm_num [recordLaw,recordState,policyBranches,fixedPolicy,deterministicPolicy,
48     pointMass,echo,scalarCone,Fin.sum_univ_two]
49 
50 theorem identical_instrument_has_zero_discrepancy (h : List (Fin 2 × Fin 2)) (a : Fin 2) (x : ℝ) :
51     scalarCone.discrepancy (fun o => echo h (a,o)) (fun o => echo h (a,o)) x=0 := by
52   simp [ProbabilityCone.discrepancy]
53 
54 /-- Model identity cannot bound laws generated by different policies. -/
55 theorem changed_policy_not_zero_error :
56     ¬ distance (observationLaw scalarCone (fixedPolicy 0) echo 1 1)
57       (observationLaw scalarCone (fixedPolicy 1) echo 1 1) ≤ 0 := by
58   rw [changed_policy_observation_distance]; norm_num
59 
60 noncomputable def fairPolicy (_ : List (Fin 2 × Fin 2)) : Fin 2 → ℝ := ![1/2,1/2]
61 
62 theorem fairPolicy_prior (h : List (Fin 2 × Fin 2)) : IsPrior (fairPolicy h) := by
63   constructor
64   · intro a; fin_cases a <;> norm_num [fairPolicy]
65   · norm_num [fairPolicy,Fin.sum_univ_two]
66 
67 /-- A shared randomized policy is an actual instance of the whole-record theorem. -/
68 theorem fair_policy_identical_laws (n : ℕ) :
69     distance (observationLaw scalarCone fairPolicy echo n 1)
70       (observationLaw scalarCone fairPolicy echo n 1)=0 := by
71   have he : ∀ (h : List (Fin 2 × Fin 2)) (a : Fin 2) x, x ∈ scalarCone.base →
72       scalarCone.discrepancy (fun o => echo h (a,o)) (fun o => echo h (a,o)) x ≤
73         (fun _ : ℕ => (0 : ℝ)) h.length := by
74     intro h a x _
75     rw [identical_instrument_has_zero_discrepancy]
76   have hb := shared_policy_observation_tv_bound scalarCone fairPolicy fairPolicy_prior echo echo
77     echo_instrument echo_instrument (fun _ => 0) he n 1 1 scalar_initial scalar_initial
78   simp only [sub_self,ProbabilityCone.value_zero,zero_div,Finset.sum_const_zero,add_zero,
79     min_eq_right (by norm_num : (0 : ℝ) ≤ 1)] at hb
80   exact le_antisymm hb (distance_nonneg _ _)
81 
82 noncomputable def redundantSynthesis : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 2 → ℝ) :=
83   (!![1,1,1;0,1,2] : Matrix (Fin 2) (Fin 3) ℝ).mulVecLin
84 
85 def firstMass : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
86 
87 theorem redundant_normalized : firstMass.comp redundantSynthesis=mass := by
88   apply LinearMap.ext
89   intro x
90   simp [firstMass,redundantSynthesis,Matrix.mulVec,dotProduct,mass_apply,Fin.sum_univ_three,Matrix.cons_val_two]
91 
92 theorem redundant_surjective : Function.Surjective redundantSynthesis := by
93   intro x
94   refine ⟨![x 0-x 1,x 1,0],?_⟩
95   funext i
96   fin_cases i <;> simp [redundantSynthesis,Matrix.mulVec,dotProduct,Fin.sum_univ_three,Matrix.cons_val_two]
97 
98 noncomputable def redundantCone : ProbabilityCone (Fin 2 → ℝ) :=
99   finiteCone redundantSynthesis firstMass redundant_normalized redundant_surjective
100 
101 noncomputable def leastSquareCoefficients : Fin 3 → ℝ := ![5/6,1/3,-1/6]
102 
103 theorem redundant_same_state : redundantSynthesis leastSquareCoefficients=![1,0] := by
104   ext i; fin_cases i <;> norm_num [redundantSynthesis,leastSquareCoefficients,
105     Matrix.mulVec,dotProduct,Fin.sum_univ_three,Matrix.cons_val_two]
106 
107 theorem redundant_state_in_cone : (![1,0] : Fin 2 → ℝ) ∈ redundantCone.carrier := by
108   refine ⟨![1,0,0],?_,?_⟩
109   · intro i; fin_cases i <;> norm_num
110   · ext i; fin_cases i <;> norm_num [redundantSynthesis,Matrix.mulVec,dotProduct,Fin.sum_univ_three,Matrix.cons_val_two]
111 
112 theorem redundant_base_norm_one : redundantCone.value (![1,0])=1 :=
113   (redundantCone.value_on_cone redundant_state_in_cone).trans (by rfl)
114 
115 theorem redundant_coefficients_l1 : l1 leastSquareCoefficients=4/3 := by
116   norm_num [l1,leastSquareCoefficients,Fin.sum_univ_three,Matrix.cons_val_two]
117 
118 /-- This coefficient vector really minimizes squared Euclidean length under the synthesis constraint. -/
119 theorem leastSquareCoefficients_minimal (a : Fin 3 → ℝ)
120     (ha : redundantSynthesis a=![1,0]) :
121     (∑ j, (leastSquareCoefficients j)^2) ≤ ∑ j, (a j)^2 := by
122   have h0 := congrFun ha 0
123   have h1 := congrFun ha 1
124   simp [redundantSynthesis,Matrix.mulVec,dotProduct,Fin.sum_univ_three,Matrix.cons_val_two] at h0 h1
125   have he0 : a 0=1+a 2 := by linarith
126   have he1 : a 1= -2*a 2 := by linarith
127   norm_num [leastSquareCoefficients,Fin.sum_univ_three,Matrix.cons_val_two]
128   rw [he0,he1]
129   nlinarith [sq_nonneg (a 2+1/6)]
130 
131 /-- Even minimum Euclidean-length coefficients need not compute the base norm. -/
132 theorem least_square_l1_is_not_base_norm :
133     redundantCone.value (redundantSynthesis leastSquareCoefficients) ≠ l1 leastSquareCoefficients := by
134   rw [redundant_same_state,redundant_base_norm_one,redundant_coefficients_l1]
135   norm_num
136 
137 end Komorebi.LSM.Block7BoundaryExamples

Back to source controls