EllipsoidDiscovery.lean

1 import Mathlib.Analysis.Matrix.PosDef
2 import Mathlib.Algebra.Order.Star.Real
3 import Mathlib.Data.Matrix.Block
4 import Mathlib.LinearAlgebra.FiniteDimensional.Basic
5 import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
6 import Mathlib.Tactic
7 
8 /-! P63: operator-only affine centers and normalized invariant ellipsoid
9 proposals. The dimension-one invariant-form hypothesis is a genuine finrank
10 statement about the symmetric fixed-point subspace. It is used to derive
11 uniqueness, rather than assuming the desired normalized metric. -/
12 set_option autoImplicit false
13 namespace Komorebi.LSM.EllipsoidDiscovery
14 open Matrix
15 open scoped BigOperators
16 
17 variable {D : Type*} [Fintype D]
18 
19 /-- The actual linear space of real symmetric forms fixed by congruence. -/
20 def invariantForms (A : Matrix D D ℝ) : Submodule ℝ (Matrix D D ℝ) where
21   carrier := {H | H.IsHermitian ∧ A.transpose * H * A=H}
22   zero_mem' := ⟨Matrix.isHermitian_zero,by simp⟩
23   add_mem' := by
24     rintro H K ⟨hH,hA⟩ ⟨hK,hB⟩
25     exact ⟨hH.add hK,by simp only [Matrix.mul_add,Matrix.add_mul,hA,hB]⟩
26   smul_mem' := by
27     intro a H hH
28     refine ⟨hH.1.smul (by simp [IsSelfAdjoint]),?_⟩
29     simp only [Matrix.mul_smul,Matrix.smul_mul,hH.2]
30 
31 @[simp] theorem mem_invariantForms (A H : Matrix D D ℝ) :
32     H∈invariantForms A ↔ H.IsHermitian ∧ A.transpose * H * A=H := Iff.rfl
33 
34 /-- Real quadratic evaluation, with no positivity assumed in the definition. -/
35 def quadratic (H : Matrix D D ℝ) (x : D → ℝ) : ℝ := x ⬝ᵥ (H *ᵥ x)
36 
37 theorem quadratic_smul (a : ℝ) (H : Matrix D D ℝ) (x : D → ℝ) :
38     quadratic (a • H) x=a * quadratic H x := by
39   simp [quadratic,Matrix.smul_mulVec,dotProduct_smul]
40 
41 theorem quadratic_pos {H : Matrix D D ℝ} (hH : H.PosDef)
42     {x : D → ℝ} (hx : x≠0) : 0<quadratic H x := by
43   simpa only [quadratic,Pi.star_apply,star_trivial] using hH.dotProduct_mulVec_pos hx
44 
45 /-- One-dimensionality makes every actual symmetric invariant form a multiple
46 of any specified nonzero member of that subspace. -/
47 theorem invariant_scalar (A H₀ : Matrix D D ℝ)
48     (hdim : Module.finrank ℝ (invariantForms A)=1)
49     (hH₀ : H₀∈invariantForms A) (hne : H₀≠0)
50     (H : Matrix D D ℝ) (hH : H∈invariantForms A) : ∃ a : ℝ,H=a • H₀ := by
51   have hn : (⟨H₀,hH₀⟩ : invariantForms A)≠0 := by
52     intro h
53     exact hne (congrArg Subtype.val h)
54   obtain ⟨a,ha⟩ := exists_smul_eq_of_finrank_eq_one hdim hn (⟨H,hH⟩ : invariantForms A)
55   exact ⟨a,(congrArg Subtype.val ha).symm⟩
56 
57 /-- Normalize the form so the nonzero anchor displacement has squared length one. -/
58 noncomputable def normalizedMetric (H₀ : Matrix D D ℝ) (δ : D → ℝ) : Matrix D D ℝ :=
59   (quadratic H₀ δ)⁻¹ • H₀
60 
61 theorem normalizedMetric_posDef {H₀ : Matrix D D ℝ} (hH₀ : H₀.PosDef)
62     {δ : D → ℝ} (hδ : δ≠0) : (normalizedMetric H₀ δ).PosDef :=
63   hH₀.smul (inv_pos.mpr (quadratic_pos hH₀ hδ))
64 
65 theorem normalizedMetric_invariant (A H₀ : Matrix D D ℝ)
66     (hH₀ : H₀∈invariantForms A) (δ : D → ℝ) : normalizedMetric H₀ δ∈invariantForms A :=
67   (invariantForms A).smul_mem _ hH₀
68 
69 theorem normalizedMetric_boundary {H₀ : Matrix D D ℝ} (hH₀ : H₀.PosDef)
70     {δ : D → ℝ} (hδ : δ≠0) : quadratic (normalizedMetric H₀ δ) δ=1 := by
71   rw [normalizedMetric,quadratic_smul]
72   exact inv_mul_cancel₀ (quadratic_pos hH₀ hδ).ne'
73 
74 /-- The unique normalized member is derived from actual subspace dimension.
75 Positivity of a competing form is not needed for this stronger uniqueness. -/
76 theorem normalizedMetric_unique (A H₀ : Matrix D D ℝ)
77     (hdim : Module.finrank ℝ (invariantForms A)=1)
78     (hH₀ : H₀∈invariantForms A) (hp : H₀.PosDef)
79     {δ : D → ℝ} (hδ : δ≠0) (H : Matrix D D ℝ)
80     (hH : H∈invariantForms A) (hb : quadratic H δ=1) : H=normalizedMetric H₀ δ := by
81   have hq := quadratic_pos hp hδ
82   have hn : H₀≠0 := by
83     intro h
84     subst H₀
85     simp [quadratic] at hq
86   obtain ⟨a,rfl⟩ := invariant_scalar A H₀ hdim hH₀ hn H hH
87   rw [quadratic_smul] at hb
88   have ha : a=(quadratic H₀ δ)⁻¹ := by
89     have h := congrArg (fun r : ℝ => r * (quadratic H₀ δ)⁻¹) hb
90     simpa only [mul_assoc,mul_inv_cancel₀ hq.ne',mul_one,one_mul] using h
91   rw [ha]
92   rfl
93 
94 theorem unique_positive_boundary_metric (A H₀ : Matrix D D ℝ)
95     (hdim : Module.finrank ℝ (invariantForms A)=1)
96     (hH₀ : H₀∈invariantForms A) (hp : H₀.PosDef)
97     {δ : D → ℝ} (hδ : δ≠0) :
98     ∃! H : Matrix D D ℝ,H∈invariantForms A ∧ H.PosDef ∧ quadratic H δ=1 := by
99   refine ⟨normalizedMetric H₀ δ,
100     ⟨normalizedMetric_invariant A H₀ hH₀ δ,normalizedMetric_posDef hp hδ,
101       normalizedMetric_boundary hp hδ⟩,?_⟩
102   intro H hH
103   exact normalizedMetric_unique A H₀ hdim hH₀ hp hδ H hH.1 hH.2.2
104 
105 /-- The metric is independent of which positive invariant reference form was
106 chosen, hence in particular of its arbitrary positive scale. -/
107 theorem positive_reference_independent (A H₀ H₁ : Matrix D D ℝ)
108     (hdim : Module.finrank ℝ (invariantForms A)=1)
109     (hH₀ : H₀∈invariantForms A) (hp₀ : H₀.PosDef)
110     (hH₁ : H₁∈invariantForms A) (hp₁ : H₁.PosDef)
111     {δ : D → ℝ} (hδ : δ≠0) : normalizedMetric H₁ δ=normalizedMetric H₀ δ :=
112   normalizedMetric_unique A H₀ hdim hH₀ hp₀ hδ _
113     (normalizedMetric_invariant A H₁ hH₁ δ) (normalizedMetric_boundary hp₁ hδ)
114 
115 theorem positive_scale_independent (a : ℝ) (ha : 0<a)
116     {H₀ : Matrix D D ℝ} (hp : H₀.PosDef) {δ : D → ℝ} (hδ : δ≠0) :
117     normalizedMetric (a • H₀) δ=normalizedMetric H₀ δ := by
118   have hq := quadratic_pos hp hδ
119   unfold normalizedMetric
120   rw [quadratic_smul,smul_smul]
121   congr 1
122   field_simp
123 
124 section Affine
125 variable [DecidableEq D]
126 
127 abbrev State (D : Type*) := (Unit ⊕ D) → ℝ
128 
129 def mass : State D →ₗ[ℝ] ℝ := LinearMap.proj (Sum.inl ())
130 def spatial (z : State D) : D → ℝ := fun i => z (Sum.inr i)
131 def point (m : ℝ) (x : D → ℝ) : State D := Sum.elim (fun _ => m) x
132 
133 omit [Fintype D] [DecidableEq D] in
134 @[simp] theorem mass_point (m : ℝ) (x : D → ℝ) : mass (point m x)=m := rfl
135 omit [Fintype D] [DecidableEq D] in
136 @[simp] theorem spatial_point (m : ℝ) (x : D → ℝ) : spatial (point m x)=x := rfl
137 
138 omit [Fintype D] [DecidableEq D] in
139 theorem point_eta (z : State D) : point (mass z) (spatial z)=z := by
140   funext i
141   cases i with
142   | inl u => cases u; rfl
143   | inr i => rfl
144 
145 /-- The affine mass-first block matrix. -/
146 noncomputable def affineMatrix (b : D → ℝ) (A : Matrix D D ℝ) :
147     Matrix (Unit ⊕ D) (Unit ⊕ D) ℝ :=
148   Matrix.fromBlocks 1 0 (fun i _ => b i) A
149 
150 def translation (F : Matrix (Unit ⊕ D) (Unit ⊕ D) ℝ) : D → ℝ :=
151   fun i => F (Sum.inr i) (Sum.inl ())
152 
153 def spatialBlock (F : Matrix (Unit ⊕ D) (Unit ⊕ D) ℝ) : Matrix D D ℝ :=
154   fun i j => F (Sum.inr i) (Sum.inr j)
155 
156 /-- The actual mass-row identity forces the top blocks 1 and 0. -/
157 theorem mass_first_block (F : Matrix (Unit ⊕ D) (Unit ⊕ D) ℝ)
158     (hm : mass.comp F.mulVecLin=mass) : F=affineMatrix (translation F) (spatialBlock F) := by
159   have hrow (j : Unit ⊕ D) : F (Sum.inl ()) j=(Pi.single j (1 : ℝ) : State D) (Sum.inl ()) := by
160     have he := congrArg (fun L : State D →ₗ[ℝ] ℝ => L (Pi.single j 1)) hm
161     simpa only [LinearMap.comp_apply,Matrix.mulVecLin_apply,Matrix.mulVec_single_one,
162       mass,LinearMap.proj_apply,Matrix.col_apply] using he
163   funext i j
164   cases i with
165   | inl u =>
166     cases u
167     cases j with
168     | inl u => cases u; simpa [affineMatrix,Matrix.fromBlocks,Matrix.one_apply] using hrow (Sum.inl ())
169     | inr j => simpa [affineMatrix,Matrix.fromBlocks,Matrix.one_apply] using hrow (Sum.inr j)
170   | inr i =>
171     cases j with
172     | inl u => cases u; rfl
173     | inr j => rfl
174 
175 omit [DecidableEq D] in
176 theorem affineMatrix_apply (b : D → ℝ) (A : Matrix D D ℝ) (z : State D) :
177     affineMatrix b A *ᵥ z=point (mass z) (mass z • b+A *ᵥ spatial z) := by
178   funext i
179   cases i with
180   | inl u => cases u; simp [affineMatrix,Matrix.fromBlocks,point,mass,Matrix.mulVec,dotProduct,Fintype.sum_sum_type]
181   | inr i => simp [affineMatrix,Matrix.fromBlocks,point,mass,spatial,Matrix.mulVec,dotProduct,Fintype.sum_sum_type,mul_comm]
182 
183 /-- The fitted ratio is literal matrix multiplication by the actual inverse. -/
184 noncomputable def ratio (Bₐ Bᵦ : Matrix (Unit ⊕ D) (Unit ⊕ D) ℝ) := Bᵦ * Bₐ⁻¹
185 
186 theorem ratio_reconstructs (Bₐ Bᵦ : Matrix (Unit ⊕ D) (Unit ⊕ D) ℝ)
187     (hi : IsUnit Bₐ.det) : ratio Bₐ Bᵦ * Bₐ=Bᵦ := by
188   rw [ratio,Matrix.mul_assoc,Matrix.nonsing_inv_mul _ hi,Matrix.mul_one]
189 
190 theorem ratio_isUnit (Bₐ Bᵦ : Matrix (Unit ⊕ D) (Unit ⊕ D) ℝ)
191     (hₐ : IsUnit Bₐ.det) (hᵦ : IsUnit Bᵦ.det) : IsUnit (ratio Bₐ Bᵦ) := by
192   apply (Matrix.isUnit_iff_isUnit_det _).mpr
193   rw [ratio,Matrix.det_mul]
194   exact hᵦ.mul (Bₐ.isUnit_nonsing_inv_det hₐ)
195 
196 /-- The proposed center is derived from the actual inverse of I-A. -/
197 noncomputable def fixedCenter (A : Matrix D D ℝ) (b : D → ℝ) : D → ℝ :=
198   (1-A)⁻¹ *ᵥ b
199 
200 theorem fixedCenter_equation (A : Matrix D D ℝ) (b : D → ℝ)
201     (hi : IsUnit (1-A).det) : fixedCenter A b=b+A *ᵥ fixedCenter A b := by
202   have he : (1-A) *ᵥ fixedCenter A b=b := by
203     rw [fixedCenter,Matrix.mulVec_mulVec,Matrix.mul_nonsing_inv _ hi,Matrix.one_mulVec]
204   rw [Matrix.sub_mulVec,Matrix.one_mulVec] at he
205   exact sub_eq_iff_eq_add.mp he
206 
207 theorem fixedCenter_unique (A : Matrix D D ℝ) (b : D → ℝ)
208     (hi : IsUnit (1-A).det) (x : D → ℝ) (hx : x=b+A *ᵥ x) : x=fixedCenter A b := by
209   have he : (1-A) *ᵥ x=b := by
210     rw [Matrix.sub_mulVec,Matrix.one_mulVec]
211     exact sub_eq_iff_eq_add.mpr hx
212   calc
213     x=(1-A)⁻¹ *ᵥ ((1-A) *ᵥ x) := by
214       rw [Matrix.mulVec_mulVec,Matrix.nonsing_inv_mul _ hi,Matrix.one_mulVec]
215     _=fixedCenter A b := by rw [he]; rfl
216 
217 theorem unique_fixedCenter (A : Matrix D D ℝ) (b : D → ℝ)
218     (hi : IsUnit (1-A).det) : ∃! x : D → ℝ,x=b+A *ᵥ x :=
219   ⟨fixedCenter A b,fixedCenter_equation A b hi,fun x hx => fixedCenter_unique A b hi x hx⟩
220 
221 /-- Centering the normalized affine action leaves precisely the fitted spatial
222 matrix A; the ratio need not itself be an available action or a positive map. -/
223 theorem centered_action (A : Matrix D D ℝ) (b : D → ℝ)
224     (hi : IsUnit (1-A).det) (w : D → ℝ) :
225     b+A *ᵥ (fixedCenter A b+w)=fixedCenter A b+A *ᵥ w := by
226   rw [Matrix.mulVec_add,← add_assoc,← fixedCenter_equation A b hi]
227 
228 theorem centered_affineMatrix (A : Matrix D D ℝ) (b : D → ℝ)
229     (hi : IsUnit (1-A).det) (w : D → ℝ) :
230     affineMatrix b A *ᵥ point 1 (fixedCenter A b+w)=
231       point 1 (fixedCenter A b+A *ᵥ w) := by
232   rw [affineMatrix_apply,mass_point,spatial_point,one_smul,centered_action A b hi]
233 
234 omit [DecidableEq D] in
235 theorem affine_fixed_point_iff (A : Matrix D D ℝ) (b x : D → ℝ) :
236     affineMatrix b A *ᵥ point 1 x=point 1 x ↔ x=b+A *ᵥ x := by
237   rw [affineMatrix_apply,mass_point,spatial_point,one_smul]
238   constructor
239   · intro h
240     exact (congrArg spatial h).symm
241   · intro h
242     exact congrArg (point 1) h.symm
243 
244 theorem ratio_fixed_center (Bₐ Bᵦ : Matrix (Unit ⊕ D) (Unit ⊕ D) ℝ)
245     (hm : mass.comp (ratio Bₐ Bᵦ).mulVecLin=mass)
246     (hi : IsUnit (1-spatialBlock (ratio Bₐ Bᵦ)).det) :
247     ∃! x : D → ℝ,ratio Bₐ Bᵦ *ᵥ point 1 x=point 1 x := by
248   rw [mass_first_block _ hm]
249   simp_rw [affine_fixed_point_iff]
250   exact unique_fixedCenter _ _ hi
251 
252 end Affine
253 
254 section RankOneAnchor
255 
256 /-- Normalize a literal branch image by its actual mass row. This is only a
257 proposal anchor; no probability-domain validity is presumed. -/
258 noncomputable def normalizedImage (L : State D →ₗ[ℝ] State D) (z : State D) : State D :=
259   (mass (L z))⁻¹ • L z
260 
261 omit [Fintype D] in
262 theorem normalizedImage_mass (L : State D →ₗ[ℝ] State D) (z : State D)
263     (hm : mass (L z)≠0) : mass (normalizedImage L z)=1 := by
264   rw [normalizedImage,map_smul,smul_eq_mul]
265   exact inv_mul_cancel₀ hm
266 
267 omit [Fintype D] in
268 theorem normalizedImage_point (L : State D →ₗ[ℝ] State D) (z : State D)
269     (hm : mass (L z)≠0) : normalizedImage L z=point 1 (spatial (normalizedImage L z)) := by
270   rw [← normalizedImage_mass L z hm]
271   exact (point_eta _).symm
272 
273 omit [Fintype D] in
274 theorem normalizedImage_mem_range (L : State D →ₗ[ℝ] State D) (z : State D) :
275     normalizedImage L z∈L.range := by
276   refine ⟨(mass (L z))⁻¹ • z,?_⟩
277   exact L.map_smul _ z
278 
279 omit [Fintype D] in
280 /-- A true rank-one range gives the same mass-normalized anchor from every
281 nonzero-mass image. Rank one is not merely asserted of a chosen output vector. -/
282 theorem rank_one_normalized_image (L : State D →ₗ[ℝ] State D)
283     (hr : Module.finrank ℝ L.range=1) (z w : State D)
284     (hz : mass (L z)≠0) (hw : mass (L w)≠0) : normalizedImage L w=normalizedImage L z := by
285   have hn : (⟨L z,⟨z,rfl⟩⟩ : L.range)≠0 := by
286     intro h
287     have hv : L z=0 := congrArg Subtype.val h
288     exact hz (by rw [hv,map_zero])
289   obtain ⟨a,ha⟩ := exists_smul_eq_of_finrank_eq_one hr hn (⟨L w,⟨w,rfl⟩⟩ : L.range)
290   have hv : a • L z=L w := congrArg Subtype.val ha
291   have ha0 : a≠0 := by
292     intro h
293     have hmass := congrArg mass hv
294     rw [h,zero_smul,map_zero] at hmass
295     exact hw hmass.symm
296   unfold normalizedImage
297   rw [← hv,map_smul,smul_eq_mul,smul_smul]
298   congr 1
299   field_simp
300 
301 /-- The rank-one anchor is mass-normalized, and a noncentral image specifies
302 exactly one positive invariant form with that chosen boundary placement. -/
303 theorem rank_one_boundary_proposal (A H₀ : Matrix D D ℝ)
304     (hdim : Module.finrank ℝ (invariantForms A)=1)
305     (hH₀ : H₀∈invariantForms A) (hp : H₀.PosDef)
306     (L : State D →ₗ[ℝ] State D) (hr : Module.finrank ℝ L.range=1)
307     (z : State D) (hz : mass (L z)≠0) (c : D → ℝ)
308     (hδ : spatial (normalizedImage L z)≠c) :
309     normalizedImage L z=point 1 (spatial (normalizedImage L z)) ∧
310     (∀ w : State D,mass (L w)≠0 → normalizedImage L w=normalizedImage L z) ∧
311     ∃! H : Matrix D D ℝ,H∈invariantForms A ∧ H.PosDef ∧
312       quadratic H (spatial (normalizedImage L z)-c)=1 := by
313   refine ⟨normalizedImage_point L z hz,fun w hw => rank_one_normalized_image L hr z w hz hw,?_⟩
314   exact unique_positive_boundary_metric A H₀ hdim hH₀ hp (sub_ne_zero.mpr hδ)
315 
316 end RankOneAnchor
317 
318 section OperatorProposal
319 variable [DecidableEq D]
320 
321 /-- The complete operator-only algebraic proposal: literal invertible ratio,
322 mass-forced affine blocks, unique center, rank-one normalized image, and the
323 unique positive invariant metric placing that chosen image on the boundary.
324 This theorem deliberately has no full-family probability conclusion. -/
325 theorem operator_only_proposal
326     (Bₐ Bᵦ : Matrix (Unit ⊕ D) (Unit ⊕ D) ℝ)
327     (hₐ : IsUnit Bₐ.det) (hᵦ : IsUnit Bᵦ.det)
328     (hm : mass.comp (ratio Bₐ Bᵦ).mulVecLin=mass)
329     (hi : IsUnit (1-spatialBlock (ratio Bₐ Bᵦ)).det)
330     (H₀ : Matrix D D ℝ)
331     (hdim : Module.finrank ℝ (invariantForms (spatialBlock (ratio Bₐ Bᵦ)))=1)
332     (hH₀ : H₀∈invariantForms (spatialBlock (ratio Bₐ Bᵦ))) (hp : H₀.PosDef)
333     (L : State D →ₗ[ℝ] State D) (hr : Module.finrank ℝ L.range=1)
334     (z : State D) (hz : mass (L z)≠0)
335     (hδ : spatial (normalizedImage L z)≠
336       fixedCenter (spatialBlock (ratio Bₐ Bᵦ)) (translation (ratio Bₐ Bᵦ))) :
337     let F := ratio Bₐ Bᵦ
338     let c := fixedCenter (spatialBlock F) (translation F)
339     let δ := spatial (normalizedImage L z)-c
340     let H := normalizedMetric H₀ δ
341     IsUnit F ∧ F=affineMatrix (translation F) (spatialBlock F) ∧
342     (∃! x : D → ℝ,F *ᵥ point 1 x=point 1 x) ∧
343     (∀ w : D → ℝ,F *ᵥ point 1 (c+w)=point 1 (c+spatialBlock F *ᵥ w)) ∧
344     normalizedImage L z=point 1 (spatial (normalizedImage L z)) ∧
345     (∀ w : State D,mass (L w)≠0 → normalizedImage L w=normalizedImage L z) ∧
346     H∈invariantForms (spatialBlock F) ∧ H.PosDef ∧ quadratic H δ=1 ∧
347     (∀ K : Matrix D D ℝ,K∈invariantForms (spatialBlock F) → quadratic K δ=1 → K=H) := by
348   dsimp only
349   have hn := sub_ne_zero.mpr hδ
350   refine ⟨ratio_isUnit Bₐ Bᵦ hₐ hᵦ,mass_first_block _ hm,
351     ratio_fixed_center Bₐ Bᵦ hm hi,?_,normalizedImage_point L z hz,
352     fun w hw => rank_one_normalized_image L hr z w hz hw,
353     normalizedMetric_invariant _ H₀ hH₀ _,normalizedMetric_posDef hp hn,
354     normalizedMetric_boundary hp hn,?_⟩
355   · intro w
356     rw [mass_first_block _ hm]
357     exact centered_affineMatrix _ _ hi w
358   · intro K hK hboundary
359     exact normalizedMetric_unique _ H₀ hdim hH₀ hp hn K hK hboundary
360 
361 end OperatorProposal
362 
363 end Komorebi.LSM.EllipsoidDiscovery

Back to source controls