EllipsoidGeometry.lean

1 import KomorebiLSM.BaseNormTopology
2 import KomorebiLSM.MatrixOrderUnit
3 import Mathlib.Analysis.InnerProductSpace.PiL2
4 import Mathlib.Tactic
5 
6 /-! The actual positive-definite metric gives an invertible Lorentz transport. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.OrientedEllipsoid
9 open scoped BigOperators Matrix MatrixOrder Matrix.Norms.L2Operator
10 
11 abbrev State (D : Type*) := (Unit ⊕ D) → ℝ
12 variable {D : Type*}
13 
14 def mass : State D →ₗ[ℝ] ℝ := LinearMap.proj (Sum.inl ())
15 
16 def spatial : State D →ₗ[ℝ] (D → ℝ) where
17   toFun z i := z (Sum.inr i)
18   map_add' _ _ := rfl
19   map_smul' _ _ := rfl
20 
21 def point (m : ℝ) (x : D → ℝ) : State D := Sum.elim (fun _ => m) x
22 
23 @[simp] theorem mass_point (m : ℝ) (x : D → ℝ) : mass (point m x) = m := rfl
24 @[simp] theorem spatial_point (m : ℝ) (x : D → ℝ) : spatial (point m x) = x := rfl
25 @[simp] theorem point_mass_spatial (z : State D) : point (mass z) (spatial z) = z := by
26   ext i
27   rcases i with i | i
28   · cases i; rfl
29   · rfl
30 
31 def centered (c : D → ℝ) : State D →ₗ[ℝ] (D → ℝ) := spatial - mass.smulRight c
32 
33 @[simp] theorem centered_apply (c : D → ℝ) (z : State D) :
34     centered c z = spatial z - mass z • c := rfl
35 
36 variable [Fintype D] [DecidableEq D]
37 
38 def cone (c : D → ℝ) (H : Matrix D D ℝ) : Set (State D) :=
39   {z | 0 ≤ mass z ∧ centered c z ⬝ᵥ (H *ᵥ centered c z) ≤ (mass z)^2}
40 
41 /-- A positive definite real metric has an actual invertible square factor. -/
42 theorem exists_factor (H : Matrix D D ℝ) (hH : H.PosDef) :
43     ∃ L : Matrix D D ℝ, IsUnit L ∧ L.transpose * L = H := by
44   classical
45   rcases isEmpty_or_nonempty D with hD | hD
46   · let := hD
47     exact ⟨1,isUnit_one,Subsingleton.elim _ _⟩
48   · let := hD
49     have hroot : (CFC.sqrt H).PosSemidef := Matrix.nonneg_iff_posSemidef.mp (CFC.sqrt_nonneg H)
50     have hsquare : CFC.sqrt H * CFC.sqrt H = H := by
51       simpa only [pow_two] using CFC.sq_sqrt H hH.posSemidef.nonneg
52     have hi : IsUnit (CFC.sqrt H) := isUnit_of_mul_isUnit_left (hsquare ▸ hH.isUnit)
53     refine ⟨CFC.sqrt H,hi,?_⟩
54     have ht : (CFC.sqrt H).transpose = CFC.sqrt H := by
55       simpa only [Matrix.conjTranspose_eq_transpose_of_trivial] using hroot.isHermitian.eq
56     rw [ht,hsquare]
57 
58 noncomputable def factor (H : Matrix D D ℝ) (hH : H.PosDef) : Matrix D D ℝ :=
59   (exists_factor H hH).choose
60 
61 theorem factor_isUnit (H : Matrix D D ℝ) (hH : H.PosDef) : IsUnit (factor H hH) :=
62   (exists_factor H hH).choose_spec.1
63 
64 theorem factor_square (H : Matrix D D ℝ) (hH : H.PosDef) :
65     (factor H hH).transpose * factor H hH = H := (exists_factor H hH).choose_spec.2
66 
67 /-- The metric factor is an actual linear isomorphism to Euclidean spatial coordinates. -/
68 noncomputable def factorEquiv (H : Matrix D D ℝ) (hH : H.PosDef) :
69     (D → ℝ) ≃ₗ[ℝ] EuclideanSpace ℝ D := by
70   classical
71   exact (LinearEquiv.ofBijective (factor H hH).mulVecLin
72     ⟨Matrix.mulVec_injective_iff_isUnit.mpr (factor_isUnit H hH),
73       Matrix.mulVec_surjective_iff_isUnit.mpr (factor_isUnit H hH)⟩).trans
74         (WithLp.linearEquiv 2 ℝ (D → ℝ)).symm
75 
76 theorem factorEquiv_norm_sq (H : Matrix D D ℝ) (hH : H.PosDef) (x : D → ℝ) :
77     ‖factorEquiv H hH x‖^2 = x ⬝ᵥ (H *ᵥ x) := by
78   classical
79   rw [PiLp.norm_sq_eq_of_L2]
80   change (∑ i, ‖((factor H hH) *ᵥ x) i‖^2) = _
81   simp only [Real.norm_eq_abs,sq_abs]
82   calc
83     _ = ((factor H hH) *ᵥ x) ⬝ᵥ ((factor H hH) *ᵥ x) := by simp [dotProduct,pow_two]
84     _ = x ⬝ᵥ ((factor H hH).transpose *ᵥ ((factor H hH) *ᵥ x)) :=
85       (Matrix.dotProduct_transpose_mulVec _ _ _).symm
86     _ = x ⬝ᵥ (((factor H hH).transpose * factor H hH) *ᵥ x) := by rw [Matrix.mulVec_mulVec]
87     _ = _ := by rw [factor_square]
88 
89 /-- The standard forward Lorentz sheet for any real normed spatial space. -/
90 def lorentz {V : Type*} [NormedAddCommGroup V] : Set (ℝ × V) := {z | ‖z.2‖ ≤ z.1}
91 
92 section Lorentz
93 variable {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
94 
95 noncomputable def lorentzProbabilityCone : BaseNorm.ProbabilityCone (ℝ × V) where
96   carrier := lorentz
97   zero_mem := by simp [lorentz]
98   add_mem := by
99     intro x y hx hy
100     exact (norm_add_le x.2 y.2).trans (add_le_add hx hy)
101   smul_mem := by
102     intro a ha x hx
103     change ‖a • x.2‖ ≤ a * x.1
104     rw [norm_smul,Real.norm_eq_abs,abs_of_nonneg ha]
105     exact mul_le_mul_of_nonneg_left hx ha
106   spans := by
107     apply top_unique
108     intro x _
109     let a : ℝ := |x.1| + ‖x.2‖
110     have hu : (a + x.1,x.2) ∈ lorentz := by
111       change ‖x.2‖ ≤ |x.1| + ‖x.2‖ + x.1
112       linarith [neg_abs_le x.1]
113     have hv : (a,(0 : V)) ∈ lorentz := by
114       change ‖(0 : V)‖ ≤ |x.1| + ‖x.2‖
115       simpa using add_nonneg (abs_nonneg x.1) (norm_nonneg x.2)
116     have he : x = (a + x.1,x.2) - (a,(0 : V)) := by ext <;> simp
117     rw [he]
118     exact Submodule.sub_mem _ (Submodule.subset_span hu) (Submodule.subset_span hv)
119   mass := LinearMap.fst ℝ ℝ V
120   mass_pos := by
121     intro x hx hn
122     change 0 < x.1
123     have hnon : 0 ≤ x.1 := (norm_nonneg x.2).trans hx
124     apply lt_of_le_of_ne hnon
125     intro he
126     have hs : x.2 = 0 := norm_eq_zero.mp (le_antisymm (he ▸ hx) (norm_nonneg x.2))
127     exact hn (Prod.ext he.symm hs)
128   closed := isClosed_le (continuous_snd.norm) continuous_fst
129 end Lorentz
130 
131 variable (c : D → ℝ) (H : Matrix D D ℝ) (hH : H.PosDef)
132 
133 /-- This literal invertible linear change is the mass-preserving Lorentz transport. -/
134 noncomputable def lorentzTransport : State D ≃ₗ[ℝ] (ℝ × EuclideanSpace ℝ D) where
135   toFun z := (mass z,factorEquiv H hH (centered c z))
136   invFun p := point p.1 ((factorEquiv H hH).symm p.2 + p.1 • c)
137   left_inv z := by
138     change point (mass z) ((factorEquiv H hH).symm
139       (factorEquiv H hH (spatial z - mass z • c)) + mass z • c) = z
140     simp
141   right_inv p := by
142     apply Prod.ext
143     · rfl
144     · change factorEquiv H hH (((factorEquiv H hH).symm p.2 + p.1 • c)-p.1 • c) = p.2
145       simp
146   map_add' x y := by simp only [map_add,Prod.mk_add_mk]
147   map_smul' a x := by simp only [map_smul,Prod.smul_mk,RingHom.id_apply]
148 
149 @[simp] theorem lorentzTransport_mass (z : State D) :
150     (lorentzTransport c H hH z).1 = mass z := rfl
151 
152 /-- The quadratic ellipsoid cone is exactly the inverse image of one Lorentz sheet. -/
153 theorem cone_iff_lorentz (z : State D) :
154     z ∈ cone c H ↔ lorentzTransport c H hH z ∈ lorentz := by
155   change (0 ≤ mass z ∧ centered c z ⬝ᵥ (H *ᵥ centered c z) ≤ (mass z)^2) ↔
156     ‖factorEquiv H hH (centered c z)‖ ≤ mass z
157   rw [← factorEquiv_norm_sq H hH]
158   constructor
159   · rintro ⟨hm,hq⟩
160     nlinarith [norm_nonneg (factorEquiv H hH (centered c z))]
161   · intro hn
162     constructor
163     · exact (norm_nonneg (factorEquiv H hH (centered c z))).trans hn
164     · exact pow_le_pow_left₀ (norm_nonneg _) hn 2
165 
166 /-- Pulling back the standard Lorentz cone gives all actual ellipsoid cone axioms. -/
167 noncomputable def probabilityCone : BaseNorm.ProbabilityCone (State D) where
168   carrier := cone c H
169   zero_mem := (cone_iff_lorentz c H hH 0).mpr (by simp [lorentzTransport,lorentz])
170   add_mem := by
171     intro x y hx hy
172     apply (cone_iff_lorentz c H hH _).mpr
173     rw [map_add]
174     exact lorentzProbabilityCone.add_mem ((cone_iff_lorentz c H hH x).mp hx)
175       ((cone_iff_lorentz c H hH y).mp hy)
176   smul_mem := by
177     intro a ha x hx
178     apply (cone_iff_lorentz c H hH _).mpr
179     rw [map_smul]
180     exact lorentzProbabilityCone.smul_mem ha ((cone_iff_lorentz c H hH x).mp hx)
181   spans := by
182     apply top_unique
183     intro z _
184     obtain ⟨u,hu,v,hv,he⟩ := (lorentzProbabilityCone (V := EuclideanSpace ℝ D)).exists_decomposition
185       (lorentzTransport c H hH z)
186     change u ∈ lorentz at hu
187     change v ∈ lorentz at hv
188     have hu' : (lorentzTransport c H hH).symm u ∈ cone c H :=
189       (cone_iff_lorentz c H hH _).mpr (by simpa only [LinearEquiv.apply_symm_apply] using hu)
190     have hv' : (lorentzTransport c H hH).symm v ∈ cone c H :=
191       (cone_iff_lorentz c H hH _).mpr (by simpa only [LinearEquiv.apply_symm_apply] using hv)
192     have hz : z = (lorentzTransport c H hH).symm u - (lorentzTransport c H hH).symm v := by
193       exact ((lorentzTransport c H hH).symm_apply_apply z).symm.trans
194         ((congrArg (lorentzTransport c H hH).symm he).trans
195           (map_sub (lorentzTransport c H hH).symm u v))
196     rw [hz]
197     exact Submodule.sub_mem _ (Submodule.subset_span hu') (Submodule.subset_span hv')
198   mass := mass
199   mass_pos := by
200     intro z hz hn
201     have ht : lorentzTransport c H hH z ≠ 0 := by
202       intro he
203       exact hn ((lorentzTransport c H hH).injective (by simpa using he))
204     exact lorentzProbabilityCone.mass_pos ((cone_iff_lorentz c H hH z).mp hz) ht
205   closed := by
206     have he : cone c H = (lorentzTransport c H hH) ⁻¹' lorentz :=
207       Set.ext (cone_iff_lorentz c H hH)
208     rw [he]
209     exact lorentzProbabilityCone.closed.preimage
210       (lorentzTransport c H hH).toLinearMap.continuous_of_finiteDimensional
211 
212 @[simp] theorem probabilityCone_carrier : (probabilityCone c H hH).carrier = cone c H := rfl
213 @[simp] theorem probabilityCone_mass : (probabilityCone c H hH).mass = mass := rfl
214 
215 theorem cone_mass_pos (hH : H.PosDef) {z : State D} (hz : z∈cone c H) (hne : z≠0) : 0<mass z :=
216   (probabilityCone c H hH).mass_pos hz hne
217 
218 end Komorebi.LSM.OrientedEllipsoid

Back to source controls