LorentzBaseNorm.lean

1 import KomorebiLSM.InstrumentContraction
2 import KomorebiLSM.RotationModel
3 import Mathlib.Analysis.Complex.Basic
4 import Mathlib.Tactic.FinCases
5 
6 /-! The actual positive-decomposition base norm of the Lorentz cone. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.LorentzBaseNorm
9 open BaseNorm
10 
11 abbrev State := Fin 3 → ℝ
12 
13 def spatial : State →ₗ[ℝ] ℂ where
14   toFun z := ⟨z 1,z 2⟩
15   map_add' := by intro x y; apply Complex.ext <;> rfl
16   map_smul' := by intro a z; apply Complex.ext <;> simp [Pi.smul_apply]
17 
18 def point (t : ℝ) (w : ℂ) : State := ![t,w.re,w.im]
19 
20 def mass : State →ₗ[ℝ] ℝ := LinearMap.proj 0
21 
22 def carrier : Set State := {z | ‖spatial z‖ ≤ z 0}
23 
24 @[simp] theorem mass_apply (z : State) : mass z=z 0 := rfl
25 @[simp] theorem spatial_apply_re (z : State) : (spatial z).re=z 1 := rfl
26 @[simp] theorem spatial_apply_im (z : State) : (spatial z).im=z 2 := rfl
27 @[simp] theorem point_zero (t : ℝ) (w : ℂ) : point t w 0=t := by simp [point]
28 @[simp] theorem point_one (t : ℝ) (w : ℂ) : point t w 1=w.re := by simp [point]
29 @[simp] theorem point_two (t : ℝ) (w : ℂ) : point t w 2=w.im := by simp [point]
30 @[simp] theorem spatial_point (t : ℝ) (w : ℂ) : spatial (point t w)=w := by apply Complex.ext <;> simp
31 @[simp] theorem point_mass_spatial (z : State) : point (z 0) (spatial z)=z := by
32   funext i; fin_cases i <;> simp
33 
34 theorem spatial_norm (z : State) : ‖spatial z‖=Real.sqrt (z 1^2+z 2^2) := by
35   rw [Complex.norm_eq_sqrt_sq_add_sq]
36   rfl
37 
38 theorem carrier_zero : (0:State) ∈ carrier := by simp [carrier]
39 
40 theorem carrier_mass_nonneg {z : State} (hz : z∈carrier) : 0≤z 0 :=
41   (norm_nonneg _).trans hz
42 
43 theorem carrier_add {x y : State} (hx : x∈carrier) (hy : y∈carrier) : x+y∈carrier := by
44   change ‖spatial (x+y)‖ ≤ x 0+y 0
45   rw [map_add]
46   exact (norm_add_le _ _).trans (add_le_add hx hy)
47 
48 theorem carrier_smul {a : ℝ} (ha : 0≤a) {z : State} (hz : z∈carrier) : a • z∈carrier := by
49   change ‖spatial (a • z)‖ ≤ a*z 0
50   rw [map_smul,norm_smul,Real.norm_eq_abs,abs_of_nonneg ha]
51   exact mul_le_mul_of_nonneg_left hz ha
52 
53 theorem spatial_eq_zero_and_mass_eq_zero {z : State} (hs : spatial z=0) (ht : z 0=0) : z=0 := by
54   rw [← point_mass_spatial z, hs, ht]
55   funext i; fin_cases i <;> simp
56 
57 theorem carrier_mass_pos {z : State} (hz : z∈carrier) (hne : z≠0) : 0<z 0 := by
58   have hn := carrier_mass_nonneg hz
59   apply lt_of_le_of_ne hn
60   intro he
61   have hs : spatial z=0 := norm_eq_zero.mp (le_antisymm (hz.trans_eq he.symm) (norm_nonneg _))
62   exact hne (spatial_eq_zero_and_mass_eq_zero hs he.symm)
63 
64 theorem carrier_closed : IsClosed carrier := by
65   exact isClosed_le (spatial.continuous_of_finiteDimensional.norm) (continuous_apply 0)
66 
67 /-- Every vector is an actual difference of two Lorentz-positive vectors. -/
68 theorem exists_positive_decomposition (z : State) :
69     ∃ u∈carrier, ∃ v∈carrier, z=u-v := by
70   let M : ℝ := ‖spatial z‖+|z 0|
71   refine ⟨point M (spatial z), ?_, point (M-z 0) 0, ?_, ?_⟩
72   · change ‖spatial (point M (spatial z))‖ ≤ M
73     simp only [spatial_point]
74     exact le_add_of_nonneg_right (abs_nonneg _)
75   · change ‖spatial (point (M-z 0) 0)‖ ≤ M-z 0
76     rw [spatial_point,norm_zero]
77     dsimp [M]
78     linarith [norm_nonneg (spatial z), le_abs_self (z 0)]
79   · funext i
80     fin_cases i <;> simp [point]
81 
82 theorem carrier_spans : Submodule.span ℝ carrier=⊤ := by
83   apply top_unique
84   intro z _
85   obtain ⟨u,hu,v,hv,hz⟩ := exists_positive_decomposition z
86   rw [hz]
87   exact Submodule.sub_mem _ (Submodule.subset_span hu) (Submodule.subset_span hv)
88 
89 noncomputable def coneInstance : ProbabilityCone State where
90   carrier := carrier
91   zero_mem := carrier_zero
92   add_mem := carrier_add
93   smul_mem := carrier_smul
94   spans := carrier_spans
95   mass := mass
96   mass_pos := carrier_mass_pos
97   closed := carrier_closed
98 
99 @[simp] theorem coneInstance_carrier (z : State) : z∈coneInstance.carrier ↔ ‖spatial z‖≤z 0 := Iff.rfl
100 @[simp] theorem coneInstance_mass (z : State) : coneInstance.mass z=z 0 := rfl
101 
102 theorem max_le_cost {z u v : State} (hu : u∈carrier) (hv : v∈carrier) (hz : z=u-v) :
103     max |z 0| ‖spatial z‖ ≤ u 0+v 0 := by
104   apply max_le
105   · rw [hz,Pi.sub_apply]
106     exact abs_sub_le_iff.mpr ⟨by linarith [carrier_mass_nonneg hv], by linarith [carrier_mass_nonneg hu]⟩
107   · rw [hz,map_sub]
108     exact (norm_sub_le _ _).trans (add_le_add hu hv)
109 
110 /-- A unit spatial direction supplies positive rays at both opposite boundary points. -/
111 theorem point_ray_mem {a : ℝ} (ha : 0≤a) {q : ℂ} (hq : ‖q‖≤1) :
112     point a (a • q)∈carrier := by
113   change ‖spatial (point a (a • q))‖ ≤ a
114   rw [spatial_point,norm_smul,Real.norm_eq_abs,abs_of_nonneg ha]
115   simpa using mul_le_mul_of_nonneg_left hq ha
116 
117 /-- The minimum positive-decomposition cost is attained, including zero. -/
118 theorem exists_minimal_decomposition (z : State) :
119     ∃ u∈carrier, ∃ v∈carrier, z=u-v ∧
120       u 0+v 0=max |z 0| ‖spatial z‖ := by
121   let M : ℝ := max |z 0| ‖spatial z‖
122   have hM : 0≤M := (norm_nonneg (spatial z)).trans (le_max_right _ _)
123   have htM : |z 0|≤M := le_max_left _ _
124   have hsM : ‖spatial z‖≤M := le_max_right _ _
125   by_cases hzero : M=0
126   · rw [hzero] at htM hsM
127     have ht : z 0=0 := abs_eq_zero.mp (le_antisymm htM (abs_nonneg _))
128     have hs : spatial z=0 := norm_eq_zero.mp (le_antisymm hsM (norm_nonneg _))
129     have hz := spatial_eq_zero_and_mass_eq_zero hs ht
130     subst z
131     exact ⟨0,carrier_zero,0,carrier_zero,by simp,by simp⟩
132   · have hMp : 0<M := lt_of_le_of_ne hM (Ne.symm hzero)
133     let q : ℂ := M⁻¹ • spatial z
134     let a : ℝ := (M+z 0)/2
135     let b : ℝ := (M-z 0)/2
136     have ht : |z 0|≤M := le_max_left _ _
137     have ha : 0≤a := by dsimp [a]; linarith [neg_abs_le (z 0)]
138     have hb : 0≤b := by dsimp [b]; linarith [le_abs_self (z 0)]
139     have hab : a+b=M := by dsimp [a,b]; ring
140     have hd : a-b=z 0 := by dsimp [a,b]; ring
141     have hq : ‖q‖≤1 := by
142       change ‖(M⁻¹ : ℝ) • spatial z‖≤1
143       rw [norm_smul,Real.norm_eq_abs,abs_of_nonneg (inv_nonneg.mpr hM)]
144       have hs : ‖spatial z‖≤M := le_max_right _ _
145       exact (inv_mul_le_iff₀ hMp).mpr (by simpa using hs)
146     refine ⟨point a (a • q),point_ray_mem ha hq,point b (b • -q),point_ray_mem hb (by simpa using hq),?_,?_⟩
147     · have hsp : a • q-b • -q=spatial z := by
148         rw [smul_neg,sub_neg_eq_add,← add_smul,hab]
149         change (M:ℝ) • ((M⁻¹:ℝ) • spatial z)=spatial z
150         rw [smul_smul,mul_inv_cancel₀ hzero,one_smul]
151       have he : point a (a • q)-point b (b • -q)=point (z 0) (spatial z) := by
152         funext i
153         fin_cases i
154         · simpa [point] using hd
155         · simpa [point,Complex.sub_re] using congrArg Complex.re hsp
156         · simpa [point,Complex.sub_im] using congrArg Complex.im hsp
157       exact (he.trans (point_mass_spatial z)).symm
158     · simpa only [point_zero] using hab
159 
160 /-- The base norm is the cylinder norm claimed in P47, derived from the actual infimum. -/
161 theorem value_eq (z : State) : coneInstance.value z=max |z 0| ‖spatial z‖ := by
162   apply le_antisymm
163   · obtain ⟨u,hu,v,hv,hz,hcost⟩ := exists_minimal_decomposition z
164     exact (coneInstance.value_le_cost hu hv hz).trans_eq hcost
165   · apply coneInstance.le_value
166     exact fun _ hu _ hv hz => max_le_cost hu hv hz
167 
168 theorem value_eq_sqrt (z : State) :
169     coneInstance.value z=max |z 0| (Real.sqrt (z 1^2+z 2^2)) := by
170   rw [value_eq,spatial_norm]
171 
172 theorem cone_iff_norm (z : State) : z∈RotationModel.cone ↔ ‖spatial z‖≤z 0 := by
173   rw [spatial_norm]
174   rfl
175 
176 theorem carrier_eq_model_cone : carrier=RotationModel.cone := by
177   ext z
178   exact (cone_iff_norm z).symm
179 
180 theorem coneInstance_carrier_eq : coneInstance.carrier=RotationModel.cone := carrier_eq_model_cone
181 
182 theorem coneInstance_mass_eq : coneInstance.mass=RotationModel.mass := rfl
183 
184 theorem model_cone_closed : IsClosed RotationModel.cone := by
185   rw [← carrier_eq_model_cone]
186   exact carrier_closed
187 
188 theorem model_cone_convex : Convex ℝ RotationModel.cone := by
189   rw [← coneInstance_carrier_eq]
190   exact coneInstance.convex_carrier
191 
192 theorem value_zero_mass (z : State) (hz : z 0=0) : coneInstance.value z=‖spatial z‖ := by
193   rw [value_eq,hz,abs_zero,max_eq_right (norm_nonneg _)]
194 
195 theorem mem_base_iff (z : State) : z∈coneInstance.base ↔
196     z 0=1 ∧ ‖spatial z‖≤1 := by
197   change (‖spatial z‖≤z 0 ∧ z 0=1) ↔ _
198   constructor
199   · rintro ⟨hn,hm⟩
200     exact ⟨hm,hn.trans_eq hm⟩
201   · rintro ⟨h,hz⟩
202     exact ⟨hz.trans_eq h.symm,h⟩
203 
204 theorem point_mem_base {w : ℂ} (hw : ‖w‖≤1) : point 1 w∈coneInstance.base := by
205   rw [mem_base_iff]
206   simpa using hw
207 
208 theorem initial_mem_base : RotationModel.initial∈coneInstance.base := by
209   constructor
210   · rw [coneInstance_carrier_eq]
211     exact RotationModel.initial_mem
212   · change RotationModel.initial 0=1
213     rfl
214 
215 /-- The displayed rational branch operators are complete instruments on the
216 actual curved cone, without a finite-generator assumption. -/
217 theorem model_instrument (a : Bool) :
218     coneInstance.Instrument (fun o => RotationModel.operator (a,o)) := by
219   constructor
220   · intro o z hz
221     rw [coneInstance_carrier_eq] at hz ⊢
222     exact RotationModel.operator_cone (a,o) hz
223   · intro z
224     simpa only [coneInstance_mass_eq] using RotationModel.operator_mass a z
225 
226 end Komorebi.LSM.LorentzBaseNorm

Back to source controls