LorentzCylinder.lean

1 import KomorebiLSM.EllipsoidGeometry
2 import KomorebiLSM.BaseNormIntegration
3 
4 /-! The Lorentz cylinder norm is the actual positive-decomposition base norm. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.LorentzCylinder
7 open scoped BigOperators
8 variable {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
9 
10 abbrev State (V : Type*) := ℝ × V
11 abbrev cone : Set (State V) := OrientedEllipsoid.lorentz
12 noncomputable abbrev probabilityCone : BaseNorm.ProbabilityCone (State V) :=
13   OrientedEllipsoid.lorentzProbabilityCone
14 
15 omit [NormedSpace ℝ V] in
16 @[simp] theorem mem_cone (z : State V) : z∈cone ↔ ‖z.2‖≤z.1 := Iff.rfl
17 @[simp] theorem mass_apply (z : State V) : probabilityCone.mass z=z.1 := rfl
18 
19 omit [NormedSpace ℝ V] in
20 theorem max_le_cost {z u v : State V} (hu : u∈cone) (hv : v∈cone) (hz : z=u-v) :
21     max |z.1| ‖z.2‖≤u.1+v.1 := by
22   have hu0 : 0≤u.1 := (norm_nonneg _).trans hu
23   have hv0 : 0≤v.1 := (norm_nonneg _).trans hv
24   apply max_le
25   · rw [hz,Prod.fst_sub]
26     exact abs_sub_le_iff.mpr ⟨by linarith,by linarith⟩
27   · rw [hz,Prod.snd_sub]
28     exact (norm_sub_le _ _).trans (add_le_add hu hv)
29 
30 theorem ray_mem {a : ℝ} (ha : 0≤a) {q : V} (hq : ‖q‖≤1) : (a,a • q)∈cone := by
31   change ‖a • q‖≤a
32   rw [norm_smul,Real.norm_eq_abs,abs_of_nonneg ha]
33   simpa using mul_le_mul_of_nonneg_left hq ha
34 
35 /-- The infimum is attained by two actual opposite positive rays. -/
36 theorem exists_minimal_decomposition (z : State V) :
37     ∃ u∈cone,∃ v∈cone,z=u-v ∧ u.1+v.1=max |z.1| ‖z.2‖ := by
38   let M : ℝ := max |z.1| ‖z.2‖
39   have hM : 0≤M := (norm_nonneg z.2).trans (le_max_right _ _)
40   have htM : |z.1|≤M := le_max_left _ _
41   have hsM : ‖z.2‖≤M := le_max_right _ _
42   by_cases hzero : M=0
43   · rw [hzero] at htM hsM
44     have ht : z.1=0 := abs_eq_zero.mp (le_antisymm htM (abs_nonneg _))
45     have hs : z.2=0 := norm_eq_zero.mp (le_antisymm hsM (norm_nonneg _))
46     have hz : z=0 := Prod.ext ht hs
47     subst z
48     exact ⟨0,probabilityCone.zero_mem,0,probabilityCone.zero_mem,by simp,by simp⟩
49   · have hMp : 0<M := lt_of_le_of_ne hM (Ne.symm hzero)
50     let q : V := M⁻¹ • z.2
51     let a : ℝ := (M+z.1)/2
52     let b : ℝ := (M-z.1)/2
53     have ha : 0≤a := by dsimp [a]; linarith [neg_abs_le z.1]
54     have hb : 0≤b := by dsimp [b]; linarith [le_abs_self z.1]
55     have hab : a+b=M := by dsimp [a,b]; ring
56     have hd : a-b=z.1 := by dsimp [a,b]; ring
57     have hq : ‖q‖≤1 := by
58       change ‖(M⁻¹ : ℝ) • z.2‖≤1
59       rw [norm_smul,Real.norm_eq_abs,abs_of_nonneg (inv_nonneg.mpr hM)]
60       exact (inv_mul_le_iff₀ hMp).mpr (by simpa using hsM)
61     refine ⟨(a,a • q),ray_mem ha hq,(b,b • -q),ray_mem hb (by simpa using hq),?_,?_⟩
62     · apply Prod.ext
63       · exact hd.symm
64       · change z.2=a • q-b • -q
65         rw [smul_neg,sub_neg_eq_add,← add_smul,hab,smul_smul,mul_inv_cancel₀ hzero,one_smul]
66     · exact hab
67 
68 /-- This equality derives the stated norm from the actual cone infimum. -/
69 theorem value_eq (z : State V) : probabilityCone.value z=max |z.1| ‖z.2‖ := by
70   apply le_antisymm
71   · obtain ⟨u,hu,v,hv,hz,hcost⟩ := exists_minimal_decomposition z
72     exact (probabilityCone.value_le_cost hu hv hz).trans_eq hcost
73   · apply probabilityCone.le_value
74     exact fun _ hu _ hv hz => max_le_cost hu hv hz
75 
76 @[simp] theorem value_zero_mass (v : V) : probabilityCone.value (0,v)=‖v‖ := by
77   rw [value_eq,abs_zero,max_eq_right (norm_nonneg _)]
78 
79 @[simp] theorem mem_base (z : State V) : z∈probabilityCone.base ↔ z.1=1 ∧ ‖z.2‖≤1 := by
80   change (‖z.2‖≤z.1 ∧ z.1=1) ↔ _
81   constructor
82   · rintro ⟨h,h1⟩
83     exact ⟨h1,h.trans_eq h1⟩
84   · rintro ⟨h1,h⟩
85     exact ⟨h.trans_eq h1.symm,h1⟩
86 
87 /-- A mass-preserving atlas pulls back every actual cone axiom. -/
88 noncomputable def atlasCone {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
89     [FiniteDimensional ℝ E] (T : E ≃ₗ[ℝ] State V) : BaseNorm.ProbabilityCone E where
90   carrier := T ⁻¹' cone
91   zero_mem := by simp only [Set.mem_preimage,map_zero]; exact probabilityCone.zero_mem
92   add_mem := by
93     intro x y hx hy
94     change T (x+y)∈cone
95     rw [map_add]
96     exact probabilityCone.add_mem hx hy
97   smul_mem := by
98     intro a ha x hx
99     change T (a • x)∈cone
100     rw [map_smul]
101     exact probabilityCone.smul_mem ha hx
102   spans := by
103     apply top_unique
104     intro z _
105     obtain ⟨u,hu,v,hv,he⟩ := probabilityCone.exists_decomposition (T z)
106     change u∈cone at hu
107     change v∈cone at hv
108     have he' : z=T.symm u-T.symm v :=
109       (T.symm_apply_apply z).symm.trans ((congrArg T.symm he).trans (map_sub T.symm u v))
110     rw [he']
111     exact Submodule.sub_mem _
112       (Submodule.subset_span (show T.symm u∈T ⁻¹' cone from by simpa only [Set.mem_preimage,LinearEquiv.apply_symm_apply] using hu))
113       (Submodule.subset_span (show T.symm v∈T ⁻¹' cone from by simpa only [Set.mem_preimage,LinearEquiv.apply_symm_apply] using hv))
114   mass := probabilityCone.mass.comp T.toLinearMap
115   mass_pos := by
116     intro x hx hne
117     exact probabilityCone.mass_pos hx (by intro h; exact hne (T.injective (by simpa using h)))
118   closed := probabilityCone.closed.preimage T.toLinearMap.continuous_of_finiteDimensional
119 
120 @[simp] theorem atlasCone_mass {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
121     [FiniteDimensional ℝ E] (T : E ≃ₗ[ℝ] State V) (z : E) :
122     (atlasCone T).mass z=(T z).1 := rfl
123 
124 end Komorebi.LSM.LorentzCylinder

Back to source controls