MatrixOrderUnit.lean

1 import Mathlib.Analysis.Matrix.Order
2 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
3 import Mathlib.Algebra.Order.Star.Real
4 import Mathlib.Tactic
5 
6 /-! A positive definite finite real matrix is an order unit for the full
7 symmetric matrix space. The bound is derived from its positive spectrum. -/
8 set_option autoImplicit false
9 namespace Komorebi.LSM.MatrixOrderUnit
10 open scoped Matrix MatrixOrder Matrix.Norms.L2Operator
11 
12 /-- No order-unit hypothesis is assumed: positive definiteness supplies a
13 strict scalar lower bound, which dominates any symmetric perturbation. -/
14 theorem exists_nonnegative_bound {D : Type*} [Fintype D] [DecidableEq D]
15     (A X : Matrix D D ℝ) (hA : A.PosDef) (hX : X.IsHermitian) :
16     ∃ a : ℝ, 0 ≤ a ∧ (a • A + X).PosSemidef ∧ (a • A - X).PosSemidef := by
17   rcases isEmpty_or_nonempty D with hD | hD
18   · let := hD
19     refine ⟨0,le_rfl,?_,?_⟩
20     all_goals
21       convert (Matrix.PosSemidef.zero : (0 : Matrix D D ℝ).PosSemidef) using 1
22       exact Subsingleton.elim _ _
23   · let := hD
24     have hsa : IsSelfAdjoint A := hA.isHermitian
25     have hxsa : IsSelfAdjoint X := hX
26     obtain ⟨r,hr,hrA⟩ := (CFC.exists_pos_algebraMap_le_iff A hsa).mpr
27       (fun x hx => hA.isStrictlyPositive.spectrum_pos hx)
28     have ha : 0 ≤ ‖X‖/r := div_nonneg (norm_nonneg X) hr.le
29     have hsmall := Matrix.PosSemidef.smul (Matrix.le_iff.mp hrA) ha
30     rw [smul_sub,Algebra.algebraMap_eq_smul_one,smul_smul,div_mul_cancel₀ _ hr.ne'] at hsmall
31     have upper (Y : Matrix D D ℝ) (hY : IsSelfAdjoint Y) :
32         Y ≤ algebraMap ℝ (Matrix D D ℝ) ‖Y‖ := by
33       apply (le_algebraMap_iff_spectrum_le hY).mpr
34       intro t ht
35       exact (Real.le_norm_self t).trans (spectrum.norm_le_norm_of_mem ht)
36     have hup : (‖X‖ • (1 : Matrix D D ℝ)-X).PosSemidef := by
37       simpa only [Algebra.algebraMap_eq_smul_one] using Matrix.le_iff.mp (upper X hxsa)
38     have hdown : (‖X‖ • (1 : Matrix D D ℝ)+X).PosSemidef := by
39       simpa only [norm_neg,Algebra.algebraMap_eq_smul_one,sub_neg_eq_add] using
40         Matrix.le_iff.mp (upper (-X) hxsa.neg)
41     refine ⟨‖X‖/r,ha,?_,?_⟩
42     · have he : (‖X‖/r) • A+X=
43           ((‖X‖/r) • A-‖X‖ • (1 : Matrix D D ℝ))+(‖X‖ • (1 : Matrix D D ℝ)+X) := by abel
44       rw [he]
45       exact hsmall.add hdown
46     · have he : (‖X‖/r) • A-X=
47           ((‖X‖/r) • A-‖X‖ • (1 : Matrix D D ℝ))+(‖X‖ • (1 : Matrix D D ℝ)-X) := by abel
48       rw [he]
49       exact hsmall.add hup
50 
51 end Komorebi.LSM.MatrixOrderUnit

Back to source controls