Prove PSD Loewner variance-proxy norm monotonicity

HighDimProb/RandomMatrix/HardboneStatements.lean

@@ -653,6 +653,44 @@ abbrev deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement {n : Nat}
     MatrixLE U V ->
       deterministicMatrixVarianceProxyNorm U <= deterministicMatrixVarianceProxyNorm V
 
+/-- Deterministic PSD Loewner monotonicity for the variance-proxy norm.
+
+This discharges the local HighDimProb-to-Mathlib order bridge only: `U` is
+assumed PSD in the explicit HighDimProb predicate, `U <= V` is assumed via the
+explicit `MatrixLE` predicate, and the conclusion is the corresponding
+operator-norm monotonicity for deterministic variance proxies. -/
+theorem deterministicMatrixVarianceProxyNorm_mono_of_matrixLE {n : Nat}
+    (U V : Matrix (Fin n) (Fin n) Real) :
+    deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement U V := by
+  intro hU hUV
+  cases n with
+  | zero =>
+      have hUzero : U = 0 := by
+        ext i
+        exact Fin.elim0 i
+      have hVzero : V = 0 := by
+        ext i
+        exact Fin.elim0 i
+      simp [hUzero, hVzero, deterministicMatrixVarianceProxyNorm,
+        deterministicOperatorNorm]
+  | succ n =>
+      have hUself : IsSelfAdjointMatrix U :=
+        (posSemidef_of_isPSDMatrix hU).1
+      rcases exists_unitVector_abs_matrixQuadraticForm_eq_deterministicOperatorNorm
+          hUself with ⟨x, hx, hnorm⟩
+      have hUquad_nonneg : 0 <= matrixQuadraticForm U x := hU.2 x
+      have hnormU_eq :
+          deterministicMatrixVarianceProxyNorm U = matrixQuadraticForm U x := by
+        rw [deterministicMatrixVarianceProxyNorm, ← hnorm,
+          abs_of_nonneg hUquad_nonneg]
+      calc
+        deterministicMatrixVarianceProxyNorm U
+            = matrixQuadraticForm U x := hnormU_eq
+        _ <= matrixQuadraticForm V x := quadraticForm_le_of_matrixLE hUV x
+        _ <= deterministicMatrixVarianceProxyNorm V := by
+          simpa [deterministicMatrixVarianceProxyNorm] using
+            matrixQuadraticForm_le_deterministicOperatorNorm V hx
+
 /-- Centered-square variance-proxy provider under an explicit norm-monotonicity
 contract.
 

HighDimProb/RandomMatrix/MatrixOrder.lean

@@ -1,3 +1,4 @@
+import Mathlib.Analysis.Matrix.Order
 import HighDimProb.RandomMatrix.Algebra
 import HighDimProb.RandomMatrix.SelfAdjoint
 
@@ -19,7 +20,7 @@ form. `MatrixLE A B` is the corresponding Loewner-style predicate
 namespace HighDimProb
 
 open MeasureTheory
-open scoped BigOperators
+open scoped BigOperators MatrixOrder
 
 noncomputable section
 
@@ -42,6 +43,20 @@ symmetric plus nonnegative quadratic form. -/
 def IsPSDMatrix {n : Nat} (A : Matrix (Fin n) (Fin n) Real) : Prop :=
   IsSymmetricMatrix A /\ forall x : Fin n -> Real, 0 <= matrixQuadraticForm A x
 
+/-- HighDimProb's explicit real PSD predicate implies Mathlib's
+`Matrix.PosSemidef` predicate. -/
+theorem posSemidef_of_isPSDMatrix {n : Nat}
+    {A : Matrix (Fin n) (Fin n) Real} (hA : IsPSDMatrix A) :
+    A.PosSemidef := by
+  classical
+  refine ⟨?_, ?_⟩
+  · apply Matrix.IsHermitian.ext
+    intro i j
+    simpa using isSymmetricMatrix_apply hA.1 i j
+  · intro x
+    have hquad := hA.2 (fun i : Fin n => x i)
+    simpa [matrixQuadraticForm, Finsupp.sum_fintype] using hquad
+
 /-- Pointwise PSD random square matrix. -/
 def RandomPSDMatrix {Omega : Type*} [MeasurableSpace Omega] {n : Nat}
     (_P : Measure Omega) (A : RandomMatrix Omega n n) : Prop :=
@@ -87,6 +102,21 @@ theorem randomPSDMatrix_rankOneRandomMatrix {Omega : Type*}
 def MatrixLE {n : Nat} (A B : Matrix (Fin n) (Fin n) Real) : Prop :=
   IsPSDMatrix (B - A)
 
+/-- HighDimProb's explicit PSD predicate gives nonnegativity in Mathlib's
+scoped matrix Loewner order. -/
+theorem matrix_nonneg_of_isPSDMatrix {n : Nat}
+    {A : Matrix (Fin n) (Fin n) Real} (hA : IsPSDMatrix A) :
+    (0 : Matrix (Fin n) (Fin n) Real) <= A :=
+  Matrix.PosSemidef.nonneg (posSemidef_of_isPSDMatrix hA)
+
+/-- HighDimProb's explicit `MatrixLE` predicate gives Mathlib's scoped matrix
+Loewner order. -/
+theorem matrix_le_of_matrixLE {n : Nat}
+    {A B : Matrix (Fin n) (Fin n) Real} (hAB : MatrixLE A B) :
+    A <= B := by
+  rw [Matrix.le_iff]
+  exact posSemidef_of_isPSDMatrix hAB
+
 theorem matrixQuadraticForm_sub {n : Nat}
     (B A : Matrix (Fin n) (Fin n) Real) (x : Fin n -> Real) :
     matrixQuadraticForm (B - A) x =

HighDimProb/RandomMatrix/Spectral.lean

@@ -380,25 +380,6 @@ theorem matrixQuadraticForm_nonneg_of_posSemidef {n : Nat}
   simpa [matrixQuadraticForm, dotProduct, Matrix.mulVec,
     Finset.mul_sum, Finset.sum_mul, mul_assoc] using h
 
-/-- HighDimProb's explicit PSD predicate gives Mathlib positive
-semidefiniteness.
-
-Formula reference: positive semidefinite real matrices are characterized by a
-nonnegative quadratic form; see https://en.wikipedia.org/wiki/Definite_matrix .
-This bridge keeps the explicit HighDimProb assumptions visible while exposing
-Mathlib's `Matrix.PosSemidef` API. -/
-theorem posSemidef_of_isPSDMatrix {n : Nat}
-    {A : Matrix (Fin n) (Fin n) Real} (hA : IsPSDMatrix A) :
-    A.PosSemidef := by
-  apply Matrix.PosSemidef.of_dotProduct_mulVec_nonneg
-  · apply Matrix.IsHermitian.ext
-    intro i j
-    simpa using Matrix.IsSymm.apply hA.1 i j
-  · intro x
-    have hx := hA.2 x
-    simpa [matrixQuadraticForm, dotProduct, Matrix.mulVec,
-      Finset.mul_sum, Finset.sum_mul, mul_assoc] using hx
-
 /-- PSD nullspace converse in HighDimProb's explicit quadratic-form vocabulary.
 
 Formula reference: for a positive semidefinite matrix, a zero quadratic form
@@ -577,6 +558,57 @@ theorem lambdaMaxOrdered_rayleighUpperBound
   rayleighUpperBound_of_spectralUpperBound
     (lambdaMaxOrdered_spectralUpperBound hA)
 
+/-- The absolute explicit quadratic form of a unit vector is bounded by the
+deterministic L2 operator norm. -/
+theorem abs_matrixQuadraticForm_le_deterministicOperatorNorm {n : Nat}
+    (A : Matrix (Fin n) (Fin n) Real) {x : Fin n -> Real}
+    (hx : IsUnitVector x) :
+    abs (matrixQuadraticForm A x) <= deterministicOperatorNorm A := by
+  have hxnorm :
+      norm (WithLp.toLp 2 x : EuclideanSpace Real (Fin n)) = 1 :=
+    norm_toLp_eq_one_of_isUnitVector hx
+  have hmul :=
+    Matrix.l2_opNorm_mulVec A (WithLp.toLp 2 x : EuclideanSpace Real (Fin n))
+  have hmul' :
+      norm ((EuclideanSpace.equiv (Fin n) Real).symm (Matrix.mulVec A x) :
+        EuclideanSpace Real (Fin n)) <= norm A := by
+    simpa [hxnorm] using hmul
+  have hinner :
+      matrixQuadraticForm A x =
+        inner Real
+          ((EuclideanSpace.equiv (Fin n) Real).symm (Matrix.mulVec A x) :
+            EuclideanSpace Real (Fin n))
+          (WithLp.toLp 2 x : EuclideanSpace Real (Fin n)) := by
+    simp [matrixQuadraticForm, Matrix.mulVec, dotProduct, inner, mul_assoc]
+    apply Finset.sum_congr rfl
+    intro i _
+    rw [← Finset.mul_sum]
+  calc
+    abs (matrixQuadraticForm A x)
+        = abs (inner Real
+          ((EuclideanSpace.equiv (Fin n) Real).symm (Matrix.mulVec A x) :
+            EuclideanSpace Real (Fin n))
+          (WithLp.toLp 2 x : EuclideanSpace Real (Fin n))) := by rw [hinner]
+    _ <= norm ((EuclideanSpace.equiv (Fin n) Real).symm (Matrix.mulVec A x) :
+          EuclideanSpace Real (Fin n)) *
+        norm (WithLp.toLp 2 x : EuclideanSpace Real (Fin n)) :=
+      abs_real_inner_le_norm _ _
+    _ = norm ((EuclideanSpace.equiv (Fin n) Real).symm (Matrix.mulVec A x) :
+          EuclideanSpace Real (Fin n)) * 1 := by rw [hxnorm]
+    _ <= norm A * 1 := by
+      exact mul_le_mul_of_nonneg_right hmul' zero_le_one
+    _ = deterministicOperatorNorm A := by
+      simp [deterministicOperatorNorm]
+
+/-- The explicit quadratic form of a unit vector is bounded above by the
+deterministic L2 operator norm. -/
+theorem matrixQuadraticForm_le_deterministicOperatorNorm {n : Nat}
+    (A : Matrix (Fin n) (Fin n) Real) {x : Fin n -> Real}
+    (hx : IsUnitVector x) :
+    matrixQuadraticForm A x <= deterministicOperatorNorm A :=
+  (le_abs_self (matrixQuadraticForm A x)).trans
+    (abs_matrixQuadraticForm_le_deterministicOperatorNorm A hx)
+
 /-- The ordered lambda-max endpoint is attained by an explicit unit
 eigenvector in HighDimProb's quadratic-form convention. -/
 private theorem exists_unitVector_matrixQuadraticForm_eq_lambdaMaxOrdered

HighDimProbJudge/RandomMatrix/TraceExpUse.lean

@@ -129,6 +129,7 @@ open scoped MatrixOrder Matrix.Norms.Operator
 #check HighDimProb.varianceProxyNormBound_of_centeredSquareChain_statement
 #check HighDimProb.deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement
 #check HighDimProb.varianceProxyNormBound_of_centeredSquareChain_of_normMono
+#check HighDimProb.deterministicMatrixVarianceProxyNorm_mono_of_matrixLE
 #check HighDimProb.varianceProxyNormBound_of_centeredSquareChain
 #check HighDimProb.varianceProxyNormBound_of_centeredSquareChain_expansion
 #check HighDimProb.traceMatrixExp_le_rank_exp_lambdaMax_statement

HighDimProbJudge/RandomMatrix/VarianceProxyUse.lean

@@ -58,6 +58,9 @@ import HighDimProb.RandomMatrix
 #check HighDimProb.matrixLE_add_left
 #check HighDimProb.matrixLE_add_right
 #check HighDimProb.matrixLE_smul_of_nonneg
+#check HighDimProb.posSemidef_of_isPSDMatrix
+#check HighDimProb.matrix_nonneg_of_isPSDMatrix
+#check HighDimProb.matrix_le_of_matrixLE
 #check HighDimProb.isSelfAdjointMatrix_matrixSquare_of_isSelfAdjointMatrix
 #check HighDimProb.matrixQuadraticForm_matrixSquare_eq_matVecSqNorm_of_selfAdjoint
 #check HighDimProb.isPSD_matrixSquare_of_selfAdjoint

HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean

@@ -56,6 +56,7 @@ variable (mHist : Fin m -> MeasurableSpace Omega)
 #check varianceProxyNormBound_of_centeredSquareChain_statement
 #check deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement
 #check varianceProxyNormBound_of_centeredSquareChain_of_normMono
+#check deterministicMatrixVarianceProxyNorm_mono_of_matrixLE
 #check traceMatrixExp_le_rank_exp_lambdaMax_statement
 #check traceMatrixExp_le_supportDim_exp_lambdaMax_statement
 #check matrixExpSupportDomination_identity_statement

HighDimProbTest/RandomMatrixVarianceProxyAPI.lean

@@ -69,6 +69,9 @@ variable (hRnonneg : 0 <= R)
 #check matrixLE_add_left
 #check matrixLE_add_right
 #check matrixLE_smul_of_nonneg
+#check posSemidef_of_isPSDMatrix
+#check matrix_nonneg_of_isPSDMatrix
+#check matrix_le_of_matrixLE
 #check randomMatrixSquare
 #check randomMatrixSquare_apply
 #check randomMatrixSquare_neg

docs/JudgeSystem.md

@@ -65,8 +65,9 @@ theorems or typed statements without relying on local test internals.
   nonnegativity bridges, random self-adjoint trace-exp moment nonnegativity,
   real/lintegral bridge theorem, natural-state Tropp/trace-MGF route checks,
   the hardbone matrix-exp/log normalization theorem, the proved matrix log/order
-  bridge, centered-square provider/norm-monotonicity contract APIs, and
-  remaining typed statement APIs.
+  bridge, centered-square provider/norm-monotonicity contract APIs including
+  `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE`, and remaining typed
+  statement APIs.
 - `HighDimProbJudge/RandomMatrix/LaplaceUse.lean`: matrix Laplace RHS and
   lintegral RHS vocabulary, trace-exp threshold events, MB-S5 conditional
   Markov/Laplace bridge APIs, MB-S6 explicit-dominance conditional wrappers,