ConvexRepairBracketing.lean

1 import KomorebiLSM.InteriorRepair
2 import Mathlib.Topology.Order.Monotone
3 
4 /-! P80: the actual full-domain feasible repair weights have a least endpoint,
5 and genuine cone-positive functionals give lower brackets. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.ConvexRepairBracketing
8 open LorentzCylinder RobustOrientedMargin InteriorRepair
9 open scoped RealInnerProductSpace InnerProductSpace
10 variable {V A : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
11 
12 /-- Feasibility quantifies the actual minimum sigma at every observation and action. -/
13 noncomputable def feasibleWeights (H : A → ℝ → State V →L[ℝ] State V) (kappa : ℝ) : Set ℝ :=
14   {eta | eta∈Set.Icc 0 1 ∧ ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → kappa≤sigma (repair (H a u) 1 eta)}
15 
16 /-- On [0,1], the center-reset margin is the literal affine expression in eta. -/
17 theorem feasible_iff_linear (H : A → ℝ → State V →L[ℝ] State V) (kappa eta : ℝ) :
18     eta∈feasibleWeights H kappa ↔ eta∈Set.Icc 0 1 ∧
19       ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → ∀ v : V,‖v‖≤1 →
20         kappa≤(1-eta)*slack (H a u (1,v))+eta := by
21   constructor
22   · rintro ⟨heta,hm⟩
23     refine ⟨heta,?_⟩
24     intro a u hu v hv
25     have hp := (le_sigma_iff _ _).mp (hm a u hu) v hv
26     simpa only [repair_slack _ _ _ heta.2,mul_one] using hp
27   · rintro ⟨heta,hlin⟩
28     refine ⟨heta,?_⟩
29     intro a u hu
30     apply (le_sigma_iff _ _).mpr
31     intro v hv
32     simpa only [repair_slack _ _ _ heta.2,mul_one] using hlin a u hu v hv
33 
34 theorem feasible_closed (H : A → ℝ → State V →L[ℝ] State V) (kappa : ℝ) :
35     IsClosed (feasibleWeights H kappa) := by
36   have he : feasibleWeights H kappa=Set.Icc 0 1 ∩
37       {eta | ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → ∀ v : V,‖v‖≤1 →
38         kappa≤(1-eta)*slack (H a u (1,v))+eta} := by
39     ext eta
40     exact feasible_iff_linear H kappa eta
41   rw [he]
42   apply isClosed_Icc.inter
43   have hc (a : A) (u : ℝ) (v : V) :
44       IsClosed {eta : ℝ | kappa≤(1-eta)*slack (H a u (1,v))+eta} :=
45     isClosed_le continuous_const (((continuous_const.sub continuous_id).mul continuous_const).add continuous_id)
46   simpa only [Set.ofPred_forall] using
47     (isClosed_iInter fun a => isClosed_iInter fun u => isClosed_iInter fun (_hu : u∈Set.Icc (-1 : ℝ) 1) =>
48       isClosed_iInter fun v => isClosed_iInter fun (_hv : ‖v‖≤1) => hc a u v)
49 
50 theorem feasible_convex (H : A → ℝ → State V →L[ℝ] State V) (kappa : ℝ) :
51     Convex ℝ (feasibleWeights H kappa) := by
52   intro eta heta xi hxi a b ha hb hab
53   apply (feasible_iff_linear H kappa _).mpr
54   have hη := (feasible_iff_linear H kappa eta).mp heta
55   have hξ := (feasible_iff_linear H kappa xi).mp hxi
56   refine ⟨convex_Icc (0 : ℝ) 1 hη.1 hξ.1 ha hb hab,?_⟩
57   intro action u hu v hv
58   let s := slack (H action u (1,v))
59   change kappa≤(1-(a*eta+b*xi))*s+(a*eta+b*xi)
60   calc
61     kappa=a*kappa+b*kappa := by rw [← add_mul,hab,one_mul]
62     _≤a*((1-eta)*s+eta)+b*((1-xi)*s+xi) :=
63       add_le_add (mul_le_mul_of_nonneg_left (hη.2 action u hu v hv) ha)
64         (mul_le_mul_of_nonneg_left (hξ.2 action u hu v hv) hb)
65     _=((a+b)-(a*eta+b*xi))*s+(a*eta+b*xi) := by ring
66     _=_ := by rw [hab]
67 
68 theorem one_feasible (H : A → ℝ → State V →L[ℝ] State V) (kappa : ℝ) (hkappa : kappa≤1) :
69     (1 : ℝ)∈feasibleWeights H kappa := by
70   apply (feasible_iff_linear H kappa 1).mpr
71   refine ⟨by constructor <;> norm_num,?_⟩
72   intro a u hu v hv
73   simpa using hkappa
74 
75 theorem feasible_bddBelow (H : A → ℝ → State V →L[ℝ] State V) (kappa : ℝ) :
76     BddBelow (feasibleWeights H kappa) := ⟨0,fun _ h => h.1.1⟩
77 
78 noncomputable def etaStar (H : A → ℝ → State V →L[ℝ] State V) (kappa : ℝ) : ℝ :=
79   sInf (feasibleWeights H kappa)
80 
81 theorem etaStar_feasible (H : A → ℝ → State V →L[ℝ] State V) (kappa : ℝ) (hkappa : kappa≤1) :
82     etaStar H kappa∈feasibleWeights H kappa :=
83   (feasible_closed H kappa).csInf_mem ⟨1,one_feasible H kappa hkappa⟩ (feasible_bddBelow H kappa)
84 
85 theorem etaStar_in_unit (H : A → ℝ → State V →L[ℝ] State V) (kappa : ℝ) (hkappa : kappa≤1) :
86     etaStar H kappa∈Set.Icc 0 1 := (etaStar_feasible H kappa hkappa).1
87 
88 /-- The complete feasible set is the actual closed interval ending at the full reset. -/
89 theorem feasible_interval (H : A → ℝ → State V →L[ℝ] State V) (kappa : ℝ) (hkappa : kappa≤1) :
90     feasibleWeights H kappa=Set.Icc (etaStar H kappa) 1 := by
91   ext eta
92   constructor
93   · intro h
94     exact ⟨csInf_le (feasible_bddBelow H kappa) h,h.1.2⟩
95   · intro h
96     exact (feasible_convex H kappa).ordConnected.out
97       (etaStar_feasible H kappa hkappa) (one_feasible H kappa hkappa) h
98 
99 /-- The actual row functional ell=(1,-q transpose), with the standard real inner product. -/
100 def separator (q : V) : State V →ₗ[ℝ] ℝ where
101   toFun z := z.1-⟪q,z.2⟫_ℝ
102   map_add' z w := by
103     change z.1+w.1-⟪q,z.2+w.2⟫_ℝ=(z.1-⟪q,z.2⟫_ℝ)+(w.1-⟪q,w.2⟫_ℝ)
104     rw [inner_add_right]
105     ring
106   map_smul' a z := by
107     change a*z.1-⟪q,a • z.2⟫_ℝ=a*(z.1-⟪q,z.2⟫_ℝ)
108     rw [inner_smul_right]
109     ring
110 
111 omit [FiniteDimensional ℝ V] in
112 theorem slack_le_separator (q : V) (hq : ‖q‖≤1) (z : State V) : slack z≤separator q z := by
113   have hi := (real_inner_le_norm q z.2).trans
114     (mul_le_mul_of_nonneg_right hq (norm_nonneg z.2))
115   change z.1-‖z.2‖≤z.1-⟪q,z.2⟫_ℝ
116   nlinarith
117 
118 omit [FiniteDimensional ℝ V] in
119 /-- Cone positivity is derived for this literal functional, not assumed as an abstract field. -/
120 theorem separator_positive (q : V) (hq : ‖q‖≤1) {z : State V} (hz : z∈cone) :
121     0≤separator q z :=
122   (sub_nonneg.mpr hz).trans (slack_le_separator q hq z)
123 
124 omit [FiniteDimensional ℝ V] in
125 theorem separator_repair_normalized (q : V) (Fhat : State V →L[ℝ] State V)
126     (eta : ℝ) (v : V) : separator q (repair Fhat 1 eta (1,v))=
127       (1-eta)*separator q (Fhat (1,v))+eta := by
128   simp only [repair,add_apply,smul_apply,map_add,map_smul,resetOperator_normalized,smul_eq_mul]
129   change (1-eta)*separator q (Fhat (1,v))+eta*(1-⟪q,(0 : V)⟫_ℝ)=_
130   simp
131 
132 /-- Every feasible weight obeys the exact separating-functional ratio lower bound. -/
133 theorem separator_ratio_lower (H : A → ℝ → State V →L[ℝ] State V) (kappa : ℝ)
134     (hkappa : kappa≤1) (eta : ℝ) (heta : eta∈feasibleWeights H kappa)
135     (a : A) (u : ℝ) (hu : u∈Set.Icc (-1 : ℝ) 1) (v q : V) (hv : ‖v‖≤1) (hq : ‖q‖≤1)
136     (hbad : separator q (H a u (1,v))<kappa) :
137     (kappa-separator q (H a u (1,v)))/(1-separator q (H a u (1,v)))≤eta := by
138   have hm := (le_sigma_iff _ _).mp (heta.2 a u hu) v hv
139   have hs := hm.trans (slack_le_separator q hq (repair (H a u) 1 eta (1,v)))
140   rw [separator_repair_normalized] at hs
141   have hden : 0<1-separator q (H a u (1,v)) := sub_pos.mpr (hbad.trans_le hkappa)
142   apply (div_le_iff₀ hden).mpr
143   nlinarith
144 
145 theorem separator_lower_endpoint (H : A → ℝ → State V →L[ℝ] State V) (kappa : ℝ)
146     (hkappa : kappa≤1) (a : A) (u : ℝ) (hu : u∈Set.Icc (-1 : ℝ) 1)
147     (v q : V) (hv : ‖v‖≤1) (hq : ‖q‖≤1) (hbad : separator q (H a u (1,v))<kappa) :
148     (kappa-separator q (H a u (1,v)))/(1-separator q (H a u (1,v)))≤etaStar H kappa :=
149   separator_ratio_lower H kappa hkappa _ (etaStar_feasible H kappa hkappa) a u hu v q hv hq hbad
150 
151 /-- A sound complete margin certificate supplies an upper bracket on the true minimum. -/
152 theorem certificate_upper_bound (H : A → ℝ → State V →L[ℝ] State V) (kappa etaU : ℝ)
153     (hetaU : etaU∈Set.Icc 0 1)
154     (hcertificate : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → kappa≤sigma (repair (H a u) 1 etaU)) :
155     etaStar H kappa≤etaU := csInf_le (feasible_bddBelow H kappa) ⟨hetaU,hcertificate⟩
156 
157 end Komorebi.LSM.ConvexRepairBracketing

Back to source controls