ConvexMargin.lean

1 import KomorebiLSM.RobustOrientedMargin
2 import Mathlib.Analysis.Convex.Combination
3 
4 /-! P76: convexity of the actual oriented margin, exact mass and covered
5 initial states in a fixed geometry. No convexity of geometry search is asserted. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.ConvexMargin
8 open LorentzCylinder RobustOrientedMargin
9 open scoped BigOperators
10 variable {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
11 
12 theorem slack_combination (x y : State V) (a b : ℝ) (ha : 0≤a) (hb : 0≤b) :
13     a*slack x+b*slack y≤slack (a • x+b • y) := by
14   have hn := norm_add_le (a • x.2) (b • y.2)
15   rw [norm_smul,norm_smul,Real.norm_eq_abs,Real.norm_eq_abs,
16     abs_of_nonneg ha,abs_of_nonneg hb] at hn
17   change a*(x.1-‖x.2‖)+b*(y.1-‖y.2‖)≤a*x.1+b*y.1-‖a • x.2+b • y.2‖
18   nlinarith
19 
20 variable [FiniteDimensional ℝ V]
21 
22 /-- The minimum over the entire normalized ball is concave in the operator. -/
23 theorem sigma_combination (F G : State V →L[ℝ] State V) (a b : ℝ)
24     (ha : 0≤a) (hb : 0≤b) :
25     a*sigma F+b*sigma G≤sigma (a • F+b • G) := by
26   apply (le_sigma_iff _ _).mpr
27   intro v hv
28   have hf := mul_le_mul_of_nonneg_left (sigma_le F v hv) ha
29   have hg := mul_le_mul_of_nonneg_left (sigma_le G v hv) hb
30   exact (add_le_add hf hg).trans (slack_combination (F (1,v)) (G (1,v)) a b ha hb)
31 
32 theorem convex_margin_set (kappa : ℝ) :
33     Convex ℝ {F : State V →L[ℝ] State V | kappa≤sigma F} := by
34   intro F hF G hG a b ha hb hab
35   have hf := mul_le_mul_of_nonneg_left hF ha
36   have hg := mul_le_mul_of_nonneg_left hG hb
37   have hs := sigma_combination F G a b ha hb
38   change kappa≤sigma (a • F+b • G)
39   have he : a*kappa+b*kappa=kappa := by rw [← add_mul,hab,one_mul]
40   linarith
41 
42 /-- Every finite convex combination of complete branch operators retains the margin. -/
43 theorem finite_margin {J : Type*} [Fintype J]
44     (F : J → State V →L[ℝ] State V) (w : J → ℝ) (kappa : ℝ)
45     (hw : ∀ j,0≤w j) (hs : ∑ j,w j=1) (hF : ∀ j,kappa≤sigma (F j)) :
46     kappa≤sigma (∑ j,w j • F j) := by
47   change (∑ j,w j • F j)∈{F : State V →L[ℝ] State V | kappa≤sigma F}
48   exact (convex_margin_set kappa).sum_mem (fun j _ => hw j) hs (fun j _ => hF j)
49 
50 omit [FiniteDimensional ℝ V] in
51 /-- Initial coverage is convex in this same fixed probability domain. -/
52 theorem convex_initial_base : Convex ℝ (probabilityCone (V := V)).base := by
53   intro x hx y hy a b ha hb hab
54   refine ⟨probabilityCone.add_mem (probabilityCone.smul_mem ha hx.1)
55     (probabilityCone.smul_mem hb hy.1),?_⟩
56   rw [map_add,map_smul,map_smul,hx.2,hy.2]
57   simpa using hab
58 
59 omit [FiniteDimensional ℝ V] in
60 theorem finite_initial {J : Type*} [Fintype J]
61     (z : J → State V) (w : J → ℝ) (hw : ∀ j,0≤w j) (hs : ∑ j,w j=1)
62     (hz : ∀ j,z j∈(probabilityCone (V := V)).base) :
63     (∑ j,w j • z j)∈(probabilityCone (V := V)).base :=
64   convex_initial_base.sum_mem (fun j _ => hw j) hs (fun j _ => hz j)
65 
66 abbrev Family (A : Type*) (n : ℕ) (V : Type*) [NormedAddCommGroup V] [NormedSpace ℝ V] :=
67   A → Fin n → State V →L[ℝ] State V
68 
69 variable {A : Type*} {n : ℕ}
70 
71 /-- Polynomial evaluation is linear in the complete operator family. -/
72 noncomputable def evaluate (a : A) (u : ℝ) : Family A n V →ₗ[ℝ] (State V →L[ℝ] State V) where
73   toFun F := PolynomialGram.operatorPolynomial (F a) u
74   map_add' F G := by
75     simp [PolynomialGram.operatorPolynomial,smul_add,Finset.sum_add_distrib]
76   map_smul' c F := by
77     simp only [PolynomialGram.operatorPolynomial,Pi.smul_apply,RingHom.id_apply,
78       Finset.smul_sum,smul_smul]
79     congr 1
80     funext k
81     rw [mul_comm]
82 
83 /-- Exact integrated mass is a linear coefficient constraint, using the
84 actual uniform-reference polynomial moments. -/
85 noncomputable def integratedMass (a : A) (z : State V) : Family A n V →ₗ[ℝ] ℝ where
86   toFun F := probabilityCone.mass ((∑ k : Fin n,UniformIntervalMoments.moment k • F a k) z)
87   map_add' F G := by
88     simp [smul_add,Finset.sum_add_distrib,map_add]
89   map_smul' c F := by
90     have he : (∑ k : Fin n,UniformIntervalMoments.moment k • (c • F a k))=
91         c • ∑ k : Fin n,UniformIntervalMoments.moment k • F a k := by
92       simp only [Finset.smul_sum,smul_smul]
93       congr 1
94       funext k
95       rw [mul_comm]
96     change probabilityCone.mass ((∑ k : Fin n,UniformIntervalMoments.moment k • (c • F a k)) z)= _
97     rw [he,smul_apply,map_smul]
98     rfl
99 
100 /-- The actual fixed-geometry feasible coefficient set. -/
101 def feasible (kappa : A → ℝ → ℝ) : Set (Family A n V) :=
102   {F | (∀ a u,u∈Set.Icc (-1 : ℝ) 1 → kappa a u≤sigma (evaluate a u F)) ∧
103     ∀ a z,integratedMass a z F=probabilityCone.mass z}
104 
105 theorem convex_feasible (kappa : A → ℝ → ℝ) : Convex ℝ (feasible (n := n) (V := V) kappa) := by
106   intro F hF G hG a b ha hb hab
107   constructor
108   · intro action u hu
109     rw [map_add,map_smul,map_smul]
110     exact convex_margin_set (kappa action u) (hF.1 action u hu) (hG.1 action u hu) ha hb hab
111   · intro action z
112     rw [map_add,map_smul,map_smul,hF.2 action z,hG.2 action z]
113     change a*probabilityCone.mass z+b*probabilityCone.mass z=probabilityCone.mass z
114     rw [← add_mul,hab,one_mul]
115 
116 /-- A convex data-consistency set can be intersected with the actual margin,
117 mass and initial constraints. Geometry is fixed throughout. -/
118 theorem convex_data_feasible (kappa : A → ℝ → ℝ)
119     (U : Set (Family A n V × State V)) (hU : Convex ℝ U) :
120     Convex ℝ {p : Family A n V × State V |
121       p.1∈feasible kappa ∧ p.2∈probabilityCone.base ∧ p∈U} := by
122   intro x hx y hy a b ha hb hab
123   exact ⟨convex_feasible kappa hx.1 hy.1 ha hb hab,
124     convex_initial_base hx.2.1 hy.2.1 ha hb hab,hU hx.2.2 hy.2.2 ha hb hab⟩
125 
126 theorem finite_feasible {J : Type*} [Fintype J]
127     (F : J → Family A n V) (w : J → ℝ) (kappa : A → ℝ → ℝ)
128     (hw : ∀ j,0≤w j) (hs : ∑ j,w j=1) (hF : ∀ j,F j∈feasible kappa) :
129     (∑ j,w j • F j)∈feasible kappa := by
130   have hc : Convex ℝ (feasible (A := A) (n := n) (V := V) kappa) := convex_feasible kappa
131   exact hc.sum_mem (t := Finset.univ) (w := w) (z := F)
132     (fun j _ => hw j) hs (fun j _ => hF j)
133 
134 theorem hull_feasible {J : Type*} (F : J → Family A n V) (kappa : A → ℝ → ℝ)
135     (hF : ∀ j,F j∈feasible kappa) :
136     convexHull ℝ (Set.range F)⊆feasible kappa := by
137   apply convexHull_min
138   · rintro _ ⟨j,rfl⟩
139     exact hF j
140   · exact convex_feasible kappa
141 
142 omit [FiniteDimensional ℝ V] in
143 theorem hull_initial {J : Type*} (z : J → State V)
144     (hz : ∀ j,z j∈(probabilityCone (V := V)).base) :
145     convexHull ℝ (Set.range z)⊆(probabilityCone (V := V)).base :=
146   convexHull_min (Set.range_subset_iff.mpr hz) convex_initial_base
147 
148 variable [MeasurableSpace V] [BorelSpace V]
149 
150 open MeasureTheory in
151 /-- Actual feasible coefficients with a nonnegative common margin construct
152 the literal polynomial probability instrument. -/
153 noncomputable def instrument (kappa : A → ℝ → ℝ) (F : Family A n V)
154     (hF : F∈feasible kappa) (hk : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → 0≤kappa a u) :
155     ContinuousInstrument.DensityInstrument (A := A) (probabilityCone (V := V)) UniformIntervalMoments.measure where
156   op a := PolynomialGram.operatorPolynomial (F a)
157   measurable_op a := (PolynomialGram.operatorPolynomial_continuous _).measurable
158   integrable_op a := PolynomialGram.operatorPolynomial_integrable _
159   positive a := PolynomialGram.uniform_ae_interval.mono fun u hu z hz => by
160     apply preserves_of_normalized _ _ hz
161     intro v hv
162     have hs := ((hk a u hu).trans (hF.1 a u hu)).trans (sigma_le _ v hv)
163     change ‖(PolynomialGram.operatorPolynomial (F a) u (1,v)).2‖≤
164       (PolynomialGram.operatorPolynomial (F a) u (1,v)).1
165     unfold slack at hs
166     change 0≤(PolynomialGram.operatorPolynomial (F a) u (1,v)).1-
167       ‖(PolynomialGram.operatorPolynomial (F a) u (1,v)).2‖ at hs
168     linarith
169   mass_preserving a z := by
170     rw [PolynomialGram.operatorPolynomial_integral]
171     exact hF.2 a z
172 
173 open MeasureTheory in
174 /-- The complete-family and initial hulls may use independent coefficients.
175 Every selected pair has actual normalized record laws at every horizon. -/
176 theorem hull_record_probability [Fintype A] [MeasurableSpace A] [MeasurableSingletonClass A]
177     {J K : Type*} (families : J → Family A n V) (initials : K → State V)
178     (kappa : A → ℝ → ℝ) (hF : ∀ j,families j∈feasible kappa)
179     (hz : ∀ k,initials k∈(probabilityCone (V := V)).base)
180     (hk : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → 0≤kappa a u)
181     (F : Family A n V) (hFh : F∈convexHull ℝ (Set.range families))
182     (z : State V) (hzh : z∈convexHull ℝ (Set.range initials))
183     (π : ContinuousRecords.Policy (A := A) (Y := ℝ)) (N : ℕ) :
184     IsProbabilityMeasure (ContinuousRecords.recordLaw
185       (instrument kappa F (hull_feasible families kappa hF hFh) hk) π z N) :=
186   ContinuousRecords.recordLaw_probability _ π ⟨z,hull_initial initials hz hzh⟩ N
187 
188 end Komorebi.LSM.ConvexMargin

Back to source controls