BaseNorm.lean

1 import Mathlib.Analysis.Normed.Module.FiniteDimension
2 import Mathlib.Analysis.Convex.Hull
3 import Mathlib.Topology.Order.Compact
4 import Mathlib.Tactic.Linarith
5 import Mathlib.Tactic.Positivity
6 import Mathlib.Tactic.Ring
7 
8 /-! The probability base norm is the infimum of actual positive decompositions.
9 Its algebraic laws are derived from cone closure and generation. -/
10 set_option autoImplicit false
11 namespace Komorebi.LSM.BaseNorm
12 open scoped BigOperators
13 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
14 
15 /-- Closed, generating positive cone with a strictly positive mass functional. -/
16 structure ProbabilityCone (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E] where
17   carrier : Set E
18   zero_mem : (0 : E) ∈ carrier
19   add_mem : ∀ {x y : E}, x ∈ carrier → y ∈ carrier → x+y ∈ carrier
20   smul_mem : ∀ {a : ℝ}, 0 ≤ a → ∀ {x : E}, x ∈ carrier → a • x ∈ carrier
21   spans : Submodule.span ℝ carrier = ⊤
22   mass : E →ₗ[ℝ] ℝ
23   mass_pos : ∀ {x : E}, x ∈ carrier → x ≠ 0 → 0 < mass x
24   closed : IsClosed carrier
25 
26 namespace ProbabilityCone
27 variable (C : ProbabilityCone E)
28 
29 def base : Set E := {x | x ∈ C.carrier ∧ C.mass x = 1}
30 
31 theorem mass_nonneg {x : E} (hx : x ∈ C.carrier) : 0 ≤ C.mass x := by
32   by_cases h : x = 0
33   · simp [h]
34   · exact (C.mass_pos hx h).le
35 
36 theorem mass_zero_iff {x : E} (hx : x ∈ C.carrier) : C.mass x = 0 ↔ x = 0 := by
37   constructor
38   · intro hm
39     by_contra hn
40     exact (ne_of_gt (C.mass_pos hx hn)) hm
41   · intro h; simp [h]
42 
43 theorem convex_carrier : Convex ℝ C.carrier := by
44   intro x hx y hy a b ha hb _
45   exact C.add_mem (C.smul_mem ha hx) (C.smul_mem hb hy)
46 
47 /-- Generation is converted to positive differences, rather than assumed as a norm law. -/
48 theorem exists_decomposition (x : E) : ∃ u ∈ C.carrier, ∃ v ∈ C.carrier, x = u-v := by
49   have hx : x ∈ Submodule.span ℝ C.carrier := by rw [C.spans]; trivial
50   induction hx using Submodule.span_induction with
51   | mem x hx => exact ⟨x,hx,0,C.zero_mem,by simp⟩
52   | zero => exact ⟨0,C.zero_mem,0,C.zero_mem,by simp⟩
53   | add x y _ _ hx hy =>
54     obtain ⟨u,hu,v,hv,rfl⟩ := hx
55     obtain ⟨s,hs,t,ht,rfl⟩ := hy
56     exact ⟨u+s,C.add_mem hu hs,v+t,C.add_mem hv ht,by abel⟩
57   | smul a x _ hx =>
58     obtain ⟨u,hu,v,hv,rfl⟩ := hx
59     by_cases ha : 0 ≤ a
60     · exact ⟨a • u,C.smul_mem ha hu,a • v,C.smul_mem ha hv,smul_sub a u v⟩
61     · have hn : 0 ≤ -a := neg_nonneg.mpr (le_of_not_ge ha)
62       refine ⟨(-a) • v,C.smul_mem hn hv,(-a) • u,C.smul_mem hn hu,?_⟩
63       simp only [smul_sub,neg_smul]; abel
64 
65 def costs (x : E) : Set ℝ :=
66   {r | ∃ u ∈ C.carrier, ∃ v ∈ C.carrier, x = u-v ∧ r = C.mass u + C.mass v}
67 
68 noncomputable def value (x : E) : ℝ := sInf (C.costs x)
69 
70 theorem costs_nonempty (x : E) : (C.costs x).Nonempty := by
71   obtain ⟨u,hu,v,hv,hx⟩ := C.exists_decomposition x
72   exact ⟨_,u,hu,v,hv,hx,rfl⟩
73 
74 theorem cost_nonneg {x : E} {r : ℝ} (hr : r ∈ C.costs x) : 0 ≤ r := by
75   obtain ⟨u,hu,v,hv,_,rfl⟩ := hr
76   exact add_nonneg (C.mass_nonneg hu) (C.mass_nonneg hv)
77 
78 theorem costs_bddBelow (x : E) : BddBelow (C.costs x) :=
79   ⟨0,fun _ h => C.cost_nonneg h⟩
80 
81 theorem value_nonneg (x : E) : 0 ≤ C.value x :=
82   le_csInf (C.costs_nonempty x) (fun _ h => C.cost_nonneg h)
83 
84 theorem value_le_cost {x u v : E} (hu : u ∈ C.carrier) (hv : v ∈ C.carrier)
85     (hx : x = u-v) : C.value x ≤ C.mass u + C.mass v :=
86   csInf_le (C.costs_bddBelow x) ⟨u,hu,v,hv,hx,rfl⟩
87 
88 theorem le_value {x : E} {a : ℝ}
89     (h : ∀ u ∈ C.carrier, ∀ v ∈ C.carrier, x = u-v → a ≤ C.mass u+C.mass v) :
90     a ≤ C.value x := by
91   apply le_csInf (C.costs_nonempty x)
92   rintro r ⟨u,hu,v,hv,hx,rfl⟩
93   exact h u hu v hv hx
94 
95 theorem abs_mass_le (x : E) : |C.mass x| ≤ C.value x := by
96   apply C.le_value
97   intro u hu v hv hx
98   rw [hx,map_sub]
99   exact abs_sub_le_iff.mpr ⟨by linarith [C.mass_nonneg hv],by linarith [C.mass_nonneg hu]⟩
100 
101 theorem value_on_cone {x : E} (hx : x ∈ C.carrier) : C.value x = C.mass x := by
102   apply le_antisymm
103   · simpa using C.value_le_cost hx C.zero_mem (by simp : x=x-0)
104   · simpa only [abs_of_nonneg (C.mass_nonneg hx)] using C.abs_mass_le x
105 
106 @[simp] theorem value_zero : C.value 0 = 0 := by
107   simpa using C.value_on_cone C.zero_mem
108 
109 theorem value_neg_le (x : E) : C.value (-x) ≤ C.value x := by
110   apply C.le_value
111   intro u hu v hv hx
112   have hn : -x=v-u := by rw [hx]; abel
113   simpa [add_comm] using C.value_le_cost hv hu hn
114 
115 @[simp] theorem value_neg (x : E) : C.value (-x) = C.value x := by
116   exact le_antisymm (C.value_neg_le x) (by simpa using C.value_neg_le (-x))
117 
118 theorem value_add_le (x y : E) : C.value (x+y) ≤ C.value x+C.value y := by
119   have h : C.value (x+y)-C.value y ≤ C.value x := by
120     apply C.le_value
121     intro u hu v hv hx
122     have h' : C.value (x+y)-(C.mass u+C.mass v) ≤ C.value y := by
123       apply C.le_value
124       intro s hs t ht hy
125       have he : x+y=(u+s)-(v+t) := by rw [hx,hy]; abel
126       have hb := C.value_le_cost (C.add_mem hu hs) (C.add_mem hv ht) he
127       simp only [map_add] at hb
128       linarith
129     linarith
130   linarith
131 
132 theorem value_sub_le (x y : E) : C.value (x-y) ≤ C.value x+C.value y := by
133   simpa only [sub_eq_add_neg,C.value_neg] using C.value_add_le x (-y)
134 
135 theorem value_smul_le {a : ℝ} (ha : 0 ≤ a) (x : E) : C.value (a • x) ≤ a*C.value x := by
136   by_cases hz : a=0
137   · simp [hz]
138   have hp : 0<a := lt_of_le_of_ne ha (Ne.symm hz)
139   rw [mul_comm a (C.value x)]
140   apply (div_le_iff₀ hp).mp
141   apply C.le_value
142   intro u hu v hv hx
143   apply (div_le_iff₀ hp).mpr
144   have he : a • x=(a • u)-(a • v) := by rw [hx,smul_sub]
145   have hb := C.value_le_cost (C.smul_mem ha hu) (C.smul_mem ha hv) he
146   simp only [map_smul,smul_eq_mul] at hb
147   nlinarith
148 
149 theorem value_smul_of_nonneg {a : ℝ} (ha : 0 ≤ a) (x : E) :
150     C.value (a • x) = a*C.value x := by
151   apply le_antisymm (C.value_smul_le ha x)
152   by_cases hz : a=0
153   · simp [hz]
154   have h := C.value_smul_le (inv_nonneg.mpr ha) (a • x)
155   simp only [smul_smul,inv_mul_cancel₀ hz,one_smul] at h
156   have hm := mul_le_mul_of_nonneg_left h ha
157   simpa only [← mul_assoc,mul_inv_cancel₀ hz,one_mul] using hm
158 
159 theorem value_smul (a : ℝ) (x : E) : C.value (a • x) = |a| * C.value x := by
160   by_cases ha : 0 ≤ a
161   · simpa [abs_of_nonneg ha] using C.value_smul_of_nonneg ha x
162   · have hn : 0 ≤ -a := neg_nonneg.mpr (le_of_not_ge ha)
163     have h := C.value_smul_of_nonneg hn x
164     simpa only [neg_smul,C.value_neg,abs_of_neg (lt_of_not_ge ha)] using h
165 
166 theorem value_sum_le {I : Type*} (s : Finset I) (f : I → E) :
167     C.value (∑ i ∈ s, f i) ≤ ∑ i ∈ s, C.value (f i) := by
168   classical
169   induction s using Finset.induction_on with
170   | empty => simp
171   | @insert i s hi ih =>
172     simp only [Finset.sum_insert hi]
173     exact (C.value_add_le _ _).trans (add_le_add le_rfl ih)
174 
175 theorem value_convex : ConvexOn ℝ Set.univ C.value := by
176   constructor
177   · exact convex_univ
178   · intro x _ y _ a b ha hb _
179     simpa only [C.value_smul_of_nonneg ha,C.value_smul_of_nonneg hb,smul_eq_mul] using
180       C.value_add_le (a • x) (b • y)
181 
182 end ProbabilityCone
183 end Komorebi.LSM.BaseNorm

Back to source controls