InstrumentContraction.lean

1 import KomorebiLSM.BaseNormTopology
2 import KomorebiLSM.RobustFiniteDomains
3 
4 /-! P42: contraction in the constructed base norm and finite-generator maxima. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.BaseNorm.ProbabilityCone
7 open scoped BigOperators
8 variable {E O : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
9 variable [Fintype O] (C : ProbabilityCone E)
10 
11 /-- These are positivity and mass constraints, not a contraction assumption. -/
12 def Instrument (B : O → E →ₗ[ℝ] E) : Prop :=
13   (∀ o x, x ∈ C.carrier → B o x ∈ C.carrier) ∧
14   (∀ x, ∑ o, C.mass (B o x)=C.mass x)
15 
16 /-- P42's summed contraction, derived by taking the positive-decomposition infimum. -/
17 theorem instrument_contraction (B : O → E →ₗ[ℝ] E) (hB : C.Instrument B) (x : E) :
18     ∑ o, C.value (B o x) ≤ C.value x := by
19   apply C.le_value
20   intro u hu v hv hx
21   calc
22     ∑ o, C.value (B o x) ≤ ∑ o, (C.mass (B o u)+C.mass (B o v)) := by
23       apply Finset.sum_le_sum
24       intro o _
25       exact C.value_le_cost (hB.1 o u hu) (hB.1 o v hv) (by rw [hx,map_sub])
26     _ = C.mass u+C.mass v := by rw [Finset.sum_add_distrib,hB.2,hB.2]
27 
28 noncomputable def discrepancy (B D : O → E →ₗ[ℝ] E) (x : E) : ℝ :=
29   ∑ o, C.value ((B o-D o) x)
30 
31 noncomputable def instrumentError (B D : O → E →ₗ[ℝ] E) : ℝ :=
32   sSup (C.discrepancy B D '' C.base)
33 
34 theorem discrepancy_nonneg (B D : O → E →ₗ[ℝ] E) (x : E) : 0 ≤ C.discrepancy B D x :=
35   Finset.sum_nonneg (fun _ _ => C.value_nonneg _)
36 
37 theorem discrepancy_smul (B D : O → E →ₗ[ℝ] E) {a : ℝ} (ha : 0 ≤ a) (x : E) :
38     C.discrepancy B D (a • x) = a*C.discrepancy B D x := by
39   simp only [discrepancy,map_smul,C.value_smul_of_nonneg ha,Finset.mul_sum]
40 
41 theorem discrepancy_add_le (B D : O → E →ₗ[ℝ] E) (x y : E) :
42     C.discrepancy B D (x+y) ≤ C.discrepancy B D x+C.discrepancy B D y := by
43   simp only [discrepancy,map_add,← Finset.sum_add_distrib]
44   exact Finset.sum_le_sum (fun o _ => C.value_add_le _ _)
45 
46 theorem discrepancy_convex (B D : O → E →ₗ[ℝ] E) :
47     ConvexOn ℝ Set.univ (C.discrepancy B D) := by
48   refine ⟨convex_univ,?_⟩
49   intro x _ y _ a b ha hb _
50   simpa only [C.discrepancy_smul B D ha,C.discrepancy_smul B D hb,smul_eq_mul] using
51     C.discrepancy_add_le B D (a • x) (b • y)
52 
53 theorem discrepancy_le_two (B D : O → E →ₗ[ℝ] E)
54     (hB : C.Instrument B) (hD : C.Instrument D) {x : E} (hx : x ∈ C.base) :
55     C.discrepancy B D x ≤ 2 := by
56   calc
57     C.discrepancy B D x ≤ ∑ o, (C.value (B o x)+C.value (D o x)) :=
58       Finset.sum_le_sum (fun o _ => C.value_sub_le _ _)
59     _ = ∑ o, (C.mass (B o x)+C.mass (D o x)) := by
60       apply Finset.sum_congr rfl
61       intro o _
62       rw [C.value_on_cone (hB.1 o x hx.1),C.value_on_cone (hD.1 o x hx.1)]
63     _ = 2 := by rw [Finset.sum_add_distrib,hB.2,hD.2,hx.2]; norm_num
64 
65 /-- A finite normalized generating hull has a genuine maximizing generator. -/
66 theorem discrepancy_max_generator {J : Type*} [Fintype J] [Nonempty J]
67     (v : J → E) (hv : C.base = convexHull ℝ (Set.range v))
68     (B D : O → E →ₗ[ℝ] E) :
69     ∃ j, v j ∈ C.base ∧ C.instrumentError B D=C.discrepancy B D (v j) ∧
70       ∀ x ∈ C.base, C.discrepancy B D x ≤ C.discrepancy B D (v j) := by
71   classical
72   obtain ⟨j,_,hj⟩ := Finset.exists_max_image Finset.univ
73     (fun j => C.discrepancy B D (v j)) Finset.univ_nonempty
74   have hjbase : v j ∈ C.base := by rw [hv]; exact subset_convexHull ℝ _ ⟨j,rfl⟩
75   have hc : Convex ℝ {x | C.discrepancy B D x ≤ C.discrepancy B D (v j)} := by
76     intro x hx y hy a b ha hb hab
77     have he := (C.discrepancy_convex B D).2 (Set.mem_univ x) (Set.mem_univ y) ha hb hab
78     change C.discrepancy B D (a • x+b • y) ≤ C.discrepancy B D (v j)
79     have hm₁ := mul_le_mul_of_nonneg_left hx ha
80     have hm₂ := mul_le_mul_of_nonneg_left hy hb
81     simp only [smul_eq_mul] at he
82     have hh := he.trans (add_le_add hm₁ hm₂)
83     rw [← add_mul,hab,one_mul] at hh
84     exact hh
85   have hK : ∀ x ∈ C.base, C.discrepancy B D x ≤ C.discrepancy B D (v j) := by
86     rw [hv]
87     apply convexHull_min _ hc
88     rintro _ ⟨i,rfl⟩
89     exact hj i (Finset.mem_univ i)
90   refine ⟨j,hjbase,?_,hK⟩
91   apply le_antisymm
92   · exact csSup_le ⟨_,v j,hjbase,rfl⟩ (by rintro r ⟨x,hx,rfl⟩; exact hK x hx)
93   · apply le_csSup
94     · exact ⟨_,by rintro r ⟨x,hx,rfl⟩; exact hK x hx⟩
95     · exact ⟨v j,hjbase,rfl⟩
96 
97 /-- The all-state supremum is at most two for two valid instruments. -/
98 theorem instrumentError_le_two (B D : O → E →ₗ[ℝ] E)
99     (hB : C.Instrument B) (hD : C.Instrument D) (hne : C.base.Nonempty) :
100     C.instrumentError B D ≤ 2 := by
101   apply csSup_le (hne.image _)
102   rintro r ⟨x,hx,rfl⟩
103   exact C.discrepancy_le_two B D hB hD hx
104 
105 /-- The supremum in P42 supplies the pointwise budget used by the tree theorem. -/
106 theorem discrepancy_le_instrumentError (B D : O → E →ₗ[ℝ] E)
107     (hB : C.Instrument B) (hD : C.Instrument D) {x : E} (hx : x ∈ C.base) :
108     C.discrepancy B D x ≤ C.instrumentError B D := by
109   apply le_csSup
110   · refine ⟨2,?_⟩
111     rintro r ⟨y,hy,rfl⟩
112     exact C.discrepancy_le_two B D hB hD hy
113   · exact ⟨x,hx,rfl⟩
114 
115 /-- Normalization is used only on positive-mass states, with the zero state handled separately. -/
116 theorem discrepancy_homogeneous_bound (B D : O → E →ₗ[ℝ] E) (ε : ℝ)
117     (hε : ∀ x ∈ C.base, C.discrepancy B D x ≤ ε)
118     {y : E} (hy : y ∈ C.carrier) : C.discrepancy B D y ≤ ε*C.mass y := by
119   by_cases hz : y=0
120   · subst y; simp [discrepancy]
121   have hm : 0<C.mass y := C.mass_pos hy hz
122   let z := (C.mass y)⁻¹ • y
123   have hb : z ∈ C.base := by
124     refine ⟨C.smul_mem (inv_nonneg.mpr hm.le) hy,?_⟩
125     simp [z,ne_of_gt hm]
126   have he : y=C.mass y • z := by simp [z,smul_smul,ne_of_gt hm]
127   calc
128     C.discrepancy B D y = C.mass y*C.discrepancy B D z := by
129       conv_lhs => rw [he]
130       exact C.discrepancy_smul B D hm.le z
131     _ ≤ C.mass y*ε := mul_le_mul_of_nonneg_left (hε z hb) hm.le
132     _ = ε*C.mass y := mul_comm _ _
133 
134 /-- One node of the observation tree, before conditioning. -/
135 theorem instrument_pair_step (B D : O → E →ₗ[ℝ] E) (hB : C.Instrument B)
136     (ε : ℝ) (hε : ∀ x ∈ C.base, C.discrepancy B D x ≤ ε)
137     (x : E) {y : E} (hy : y ∈ C.carrier) :
138     ∑ o, C.value (B o x-D o y) ≤ C.value (x-y)+ε*C.mass y := by
139   calc
140     ∑ o, C.value (B o x-D o y) ≤
141         ∑ o, (C.value (B o (x-y))+C.value ((B o-D o) y)) := by
142       apply Finset.sum_le_sum
143       intro o _
144       have he : B o x-D o y = B o (x-y)+(B o-D o) y := by
145         simp only [map_sub,LinearMap.sub_apply]; abel
146       rw [he]
147       exact C.value_add_le _ _
148     _ = (∑ o, C.value (B o (x-y)))+C.discrepancy B D y := by
149       rw [Finset.sum_add_distrib]; rfl
150     _ ≤ C.value (x-y)+ε*C.mass y :=
151       add_le_add (C.instrument_contraction B hB _) (C.discrepancy_homogeneous_bound B D ε hε hy)
152 
153 end Komorebi.LSM.BaseNorm.ProbabilityCone

Back to source controls