CurvedMomentGeometry.lean

1 import KomorebiLSM.MatrixRotation
2 import Mathlib.Analysis.Convex.Hull
3 import Mathlib.Tactic
4 
5 /-! The exact three-coordinate truncated moment cone on [-1,1]. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.CurvedMoment
8 open scoped Matrix BigOperators
9 abbrev State := Fin 3 → ℝ
10 
11 def curve (u : ℝ) : State := ![1,u,u^2]
12 noncomputable def mass : State →ₗ[ℝ] ℝ := LinearMap.proj 0
13 noncomputable def momentMatrix : State →ₗ[ℝ] Matrix (Fin 2) (Fin 2) ℝ where
14   toFun z := !![z 0,z 1;z 1,z 2]
15   map_add' z w := by ext i j; fin_cases i <;> fin_cases j <;> simp
16   map_smul' c z := by ext i j; fin_cases i <;> fin_cases j <;> simp
17 
18 def cone : Set State := {z | (momentMatrix z).PosSemidef ∧ z 2 ≤ z 0}
19 def normalized : Set State := {z | z 0=1 ∧ (z 1)^2 ≤ z 2 ∧ z 2 ≤ 1}
20 
21 @[simp] theorem mass_apply (z : State) : mass z=z 0 := rfl
22 @[simp] theorem momentMatrix_apply (z : State) : momentMatrix z=!![z 0,z 1;z 1,z 2] := rfl
23 
24 theorem momentMatrix_psd_iff (z : State) :
25     (momentMatrix z).PosSemidef ↔ 0≤z 0 ∧ 0≤z 2 ∧ (z 1)^2≤z 0*z 2 := by
26   constructor
27   · intro h
28     have hd := h.det_nonneg
29     rw [momentMatrix_apply,Matrix.det_fin_two] at hd
30     change 0≤z 0*z 2-z 1*z 1 at hd
31     exact ⟨h.diag_nonneg (i:=0),h.diag_nonneg (i:=1),by nlinarith⟩
32   · rintro ⟨hm,hy,hxy⟩
33     apply Matrix.PosSemidef.of_dotProduct_mulVec_nonneg
34     · unfold Matrix.IsHermitian
35       ext i j
36       fin_cases i <;> fin_cases j <;> simp [Matrix.conjTranspose_apply]
37     · intro v
38       have h := MatrixRotation.binary_quadratic_nonneg _ _ _ hm hy hxy (v 0) (v 1)
39       have he : star v ⬝ᵥ (momentMatrix z *ᵥ v)=z 0*(v 0)^2+2*z 1*v 0*v 1+z 2*(v 1)^2 := by
40         simp [Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
41         ring
42       rw [he]
43       exact h
44 
45 theorem cone_iff (z : State) : z∈cone ↔
46     0≤z 0 ∧ 0≤z 2 ∧ (z 1)^2≤z 0*z 2 ∧ z 2≤z 0 := by
47   simp only [cone,Set.mem_ofPred_eq,momentMatrix_psd_iff]
48   tauto
49 
50 theorem curve_mem (u : ℝ) (hu : u∈Set.Icc (-1:ℝ) 1) : curve u∈cone := by
51   rw [cone_iff]
52   change 0≤(1:ℝ) ∧ 0≤u^2 ∧ u^2≤1*u^2 ∧ u^2≤1
53   exact ⟨by norm_num,sq_nonneg _,by simp,by nlinarith [hu.1,hu.2]⟩
54 
55 theorem cone_zero : (0:State)∈cone := by rw [cone_iff]; norm_num
56 
57 theorem cone_add {x y : State} (hx : x∈cone) (hy : y∈cone) : x+y∈cone := by
58   exact ⟨by simpa only [map_add] using hx.1.add hy.1,add_le_add hx.2 hy.2⟩
59 
60 theorem cone_smul {a : ℝ} (ha : 0≤a) {z : State} (hz : z∈cone) : a•z∈cone := by
61   exact ⟨by simpa only [map_smul] using hz.1.smul ha,mul_le_mul_of_nonneg_left hz.2 ha⟩
62 
63 theorem cone_mass_zero {z : State} (hz : z∈cone) (hm : z 0=0) : z=0 := by
64   obtain ⟨_,hy,hxy,hym⟩ := (cone_iff z).mp hz
65   have h2 : z 2=0 := by linarith
66   have h1 : z 1=0 := by nlinarith [sq_nonneg (z 1)]
67   ext i
68   fin_cases i <;> simp_all
69 
70 theorem cone_spans : Submodule.span ℝ cone=⊤ := by
71   apply top_unique
72   intro z _
73   have h0 : curve 0∈Submodule.span ℝ cone := Submodule.subset_span (curve_mem 0 (by norm_num))
74   have h1 : curve 1∈Submodule.span ℝ cone := Submodule.subset_span (curve_mem 1 (by norm_num))
75   have hn : curve (-1)∈Submodule.span ℝ cone := Submodule.subset_span (curve_mem (-1) (by norm_num))
76   have he : z=(z 0-z 2)•curve 0+((z 2+z 1)/2)•curve 1+((z 2-z 1)/2)•curve (-1) := by
77     ext i
78     fin_cases i <;> simp [curve] <;> ring
79   rw [he]
80   exact Submodule.add_mem _ (Submodule.add_mem _ (Submodule.smul_mem _ _ h0)
81     (Submodule.smul_mem _ _ h1)) (Submodule.smul_mem _ _ hn)
82 
83 theorem cone_closed : IsClosed cone := by
84   exact (Matrix.posSemidef_is_closed.preimage momentMatrix.continuous_of_finiteDimensional).inter
85     (isClosed_le (continuous_apply 2) (continuous_apply 0))
86 
87 noncomputable def probabilityCone : BaseNorm.ProbabilityCone State where
88   carrier := cone
89   zero_mem := cone_zero
90   add_mem := cone_add
91   smul_mem := cone_smul
92   spans := cone_spans
93   mass := mass
94   mass_pos := by
95     intro z hz hn
96     have hm := (momentMatrix_psd_iff z).mp hz.1
97     exact lt_of_le_of_ne hm.1 (fun he => hn (cone_mass_zero hz he.symm))
98   closed := cone_closed
99 
100 theorem base_eq_normalized : probabilityCone.base=normalized := by
101   ext z
102   simp only [BaseNorm.ProbabilityCone.base,probabilityCone,Set.mem_ofPred_eq,mass_apply,
103     normalized,cone_iff]
104   constructor
105   · rintro ⟨⟨_,_,hxy,hym⟩,hm⟩
106     exact ⟨hm,by simpa [hm] using hxy,by simpa [hm] using hym⟩
107   · rintro ⟨hm,hxy,hym⟩
108     exact ⟨⟨by simp [hm],(sq_nonneg _).trans hxy,by simpa [hm] using hxy,
109       by simpa [hm] using hym⟩,hm⟩
110 
111 theorem normalized_bounds {z : State} (hz : z∈normalized) :
112     |z 1|≤1 ∧ 0≤z 2 ∧ z 2≤1 := by
113   have h2 := (sq_nonneg (z 1)).trans hz.2.1
114   exact ⟨abs_le.mpr ⟨by nlinarith [hz.2.1,hz.2.2],by nlinarith [hz.2.1,hz.2.2]⟩,h2,hz.2.2⟩
115 
116 theorem convex_hull_curve : convexHull ℝ (curve '' Set.Icc (-1:ℝ) 1)=normalized := by
117   apply Set.Subset.antisymm
118   · apply convexHull_min
119     · rintro _ ⟨u,hu,rfl⟩
120       rw [←base_eq_normalized]
121       exact ⟨curve_mem u hu,rfl⟩
122     · rw [←base_eq_normalized]
123       intro x hx y hy a b ha hb hab
124       refine ⟨probabilityCone.convex_carrier hx.1 hy.1 ha hb hab,?_⟩
125       simp only [map_add,map_smul,hx.2,hy.2,smul_eq_mul,mul_one]
126       exact hab
127   · intro z hz
128     have hcv := convex_convexHull ℝ (curve '' Set.Icc (-1:ℝ) 1)
129     have hmem (u : ℝ) (hu : u∈Set.Icc (-1:ℝ) 1) :
130         curve u∈convexHull ℝ (curve '' Set.Icc (-1:ℝ) 1) := subset_convexHull ℝ _ ⟨u,hu,rfl⟩
131     have hb := normalized_bounds hz
132     have hx : z 1∈Set.Icc (-1:ℝ) 1 := abs_le.mp hb.1
133     have he : ![1,z 1,1] = ((1-z 1)/2)•curve (-1)+((1+z 1)/2)•curve 1 := by
134       ext i
135       fin_cases i <;> simp [curve] <;> ring
136     have htop : ![1,z 1,1]∈convexHull ℝ (curve '' Set.Icc (-1:ℝ) 1) := by
137       rw [he]
138       exact hcv (hmem (-1) (by norm_num)) (hmem 1 (by norm_num))
139         (by linarith [hx.2]) (by linarith [hx.1]) (by ring)
140     by_cases hsq : (z 1)^2=1
141     · have heq : z=curve (z 1) := by
142         ext i
143         fin_cases i
144         · exact hz.1
145         · rfl
146         · change z 2=(z 1)^2
147           nlinarith [hz.2.1,hz.2.2]
148       rw [heq]
149       exact hmem _ hx
150     · have hd : 0<1-(z 1)^2 := by
151         have hh : (z 1)^2<1 := lt_of_le_of_ne (hz.2.1.trans hz.2.2) hsq
152         linarith
153       let t := (z 2-(z 1)^2)/(1-(z 1)^2)
154       have ht0 : 0≤t := div_nonneg (sub_nonneg.mpr hz.2.1) hd.le
155       have ht1 : t≤1 := (div_le_one hd).mpr (by linarith [hz.2.2])
156       have heq : z=(1-t)•curve (z 1)+t•![1,z 1,1] := by
157         ext i
158         fin_cases i <;> simp [curve,t,hz.1] <;> field_simp [ne_of_gt hd] <;> ring
159       rw [heq]
160       exact hcv (hmem _ hx) htop (by linarith) ht0 (by ring)
161 
162 end Komorebi.LSM.CurvedMoment

Back to source controls