Add PSD nullspace converse bridge

HighDimProb/Examples/RandomMatrix/KernelNullspaceUsage.lean

@@ -2,15 +2,15 @@ import HighDimProb.Examples.RandomMatrix.RankOnePSDUsage
 import HighDimProb.Examples.RandomMatrix.NTKGramDecompositionUsage
 import HighDimProb.Examples.RandomMatrix.RandomFeatureKernelUsage
 import HighDimProb.Examples.RandomMatrix.GradientCovarianceUsage
+import HighDimProb.RandomMatrix.Spectral
 
 /-!
 # Kernel nullspace usage example
 
 This examples-only file introduces nullspace and invisible-direction vocabulary
 for kernel, NTK Gram, random-feature, and gradient covariance matrices. It
-keeps the vocabulary deterministic and conservative. Hard PSD converses such as
-`x^T A x = 0` implying `A x = 0` are exposed as local adapter assumptions
-instead of being promoted to core.
+keeps the vocabulary deterministic and conservative. The PSD nullspace converse
+is supplied by the core bridge in `HighDimProb.RandomMatrix.Spectral`.
 -/
 
 namespace HighDimProb.Examples.RandomMatrix.KernelNullspaceUsage
@@ -72,6 +72,20 @@ theorem matrixQuadraticForm_eq_sum_mul_matrixAction {n : Nat}
   intro j _hj
   ring
 
+/-- The examples-local `matrixAction` is Mathlib's matrix-vector
+multiplication.
+
+Formula reference: the PSD nullspace converse is stated for the usual matrix
+action `A x`; see
+https://math.stackexchange.com/questions/3918031/prove-that-if-xtax-0-rightarrow-ax-0 .
+-/
+theorem matrixAction_eq_mulVec {n : Nat}
+    (A : Matrix (Fin (n + 1)) (Fin (n + 1)) Real)
+    (x : Fin (n + 1) -> Real) :
+    matrixAction A x = Matrix.mulVec A x := by
+  ext i
+  simp [matrixAction, Matrix.mulVec, dotProduct]
+
 /-- If `A x = 0`, then `x^T A x = 0`. -/
 theorem quadraticNullDirection_of_invisible {n : Nat}
     {A : Matrix (Fin (n + 1)) (Fin (n + 1)) Real}
@@ -93,6 +107,59 @@ theorem randomQuadraticNullDirection_of_invisible {Omega : Type*}
   intro omega
   exact quadraticNullDirection_of_invisible (h omega)
 
+/-- PSD nullspace converse for the examples-local invisible-direction
+vocabulary, using Mathlib `Matrix.PosSemidef`.
+
+Formula reference: a real symmetric positive semidefinite matrix with
+`x^T A x = 0` sends `x` to zero; see
+https://en.wikipedia.org/wiki/Definite_matrix#Square_root .
+-/
+theorem invisible_of_quadraticNull_of_posSemidef {n : Nat}
+    {A : Matrix (Fin (n + 1)) (Fin (n + 1)) Real}
+    {x : Fin (n + 1) -> Real}
+    (hPSD : A.PosSemidef)
+    (hNull : KernelQuadraticNullDirection A x) :
+    KernelInvisibleDirection A x := by
+  unfold KernelQuadraticNullDirection at hNull
+  unfold KernelInvisibleDirection
+  rw [matrixAction_eq_mulVec]
+  exact matrix_mulVec_eq_zero_of_posSemidef_quadraticForm_eq_zero hPSD hNull
+
+/-- PSD nullspace converse for the examples-local vocabulary, using
+HighDimProb's explicit `IsPSDMatrix` predicate. -/
+theorem invisible_of_quadraticNull_of_psd {n : Nat}
+    {A : Matrix (Fin (n + 1)) (Fin (n + 1)) Real}
+    {x : Fin (n + 1) -> Real}
+    (hPSD : IsPSDMatrix A)
+    (hNull : KernelQuadraticNullDirection A x) :
+    KernelInvisibleDirection A x := by
+  unfold KernelQuadraticNullDirection at hNull
+  unfold KernelInvisibleDirection
+  rw [matrixAction_eq_mulVec]
+  exact matrix_mulVec_eq_zero_of_isPSDMatrix_quadraticForm_eq_zero hPSD hNull
+
+/-- Pointwise random version of the Mathlib-PSD nullspace converse. -/
+theorem randomInvisible_of_quadraticNull_of_posSemidef {Omega : Type*}
+    [MeasurableSpace Omega] {n : Nat}
+    {A : RandomMatrix Omega (n + 1) (n + 1)}
+    {x : Fin (n + 1) -> Real}
+    (hPSD : forall omega, Matrix.PosSemidef (A omega))
+    (hNull : RandomKernelQuadraticNullDirection A x) :
+    RandomKernelInvisibleDirection A x := by
+  intro omega
+  exact invisible_of_quadraticNull_of_posSemidef (hPSD omega) (hNull omega)
+
+/-- Pointwise random version of the explicit-PSD nullspace converse. -/
+theorem randomInvisible_of_quadraticNull_of_psd {Omega : Type*}
+    [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} {n : Nat}
+    {A : RandomMatrix Omega (n + 1) (n + 1)}
+    {x : Fin (n + 1) -> Real}
+    (hPSD : RandomPSDMatrix P A)
+    (hNull : RandomKernelQuadraticNullDirection A x) :
+    RandomKernelInvisibleDirection A x := by
+  intro omega
+  exact invisible_of_quadraticNull_of_psd (hPSD omega) (hNull omega)
+
 /-- A direction orthogonal to a feature vector. -/
 def OrthogonalToFeature {n : Nat}
     (v : RankOneVector n) (x : Fin (n + 1) -> Real) : Prop :=
@@ -148,17 +215,25 @@ theorem gradientOuter_invisible_of_orthogonal {n : Nat}
   simpa [gradientOuter_eq_rankOneOuter] using
     rankOneOuter_invisible_of_orthogonal (v := g) (x := x) h
 
-/-- Example-local adapter for the hard PSD converse.
+/-- Example-local adapter for the PSD converse.
 
 For PSD matrices the mathematical statement is that `x^T A x = 0` should
-force `A x = 0`. The current example layer records it as a named assumption
-waiting for future core support instead of proving a full PSD nullspace theory. -/
+force `A x = 0`. This predicate is kept as compatibility vocabulary for older
+examples; `psdQuadraticNullImpliesInvisible_of_core` below supplies it from the
+core PSD nullspace bridge. -/
 def PSDQuadraticNullImpliesInvisible {n : Nat}
     (A : Matrix (Fin (n + 1)) (Fin (n + 1)) Real) : Prop :=
   IsPSDMatrix A ->
     forall x : Fin (n + 1) -> Real,
       KernelQuadraticNullDirection A x -> KernelInvisibleDirection A x
 
+/-- The core PSD nullspace bridge supplies the examples-local adapter. -/
+theorem psdQuadraticNullImpliesInvisible_of_core {n : Nat}
+    (A : Matrix (Fin (n + 1)) (Fin (n + 1)) Real) :
+    PSDQuadraticNullImpliesInvisible A := by
+  intro hPSD x hNull
+  exact invisible_of_quadraticNull_of_psd hPSD hNull
+
 /-- Use the local PSD-nullspace adapter to turn a quadratic-null direction into
 an invisible direction. -/
 theorem invisible_of_quadraticNull_of_psd_adapter {n : Nat}

HighDimProb/RandomMatrix/Assumptions.lean

@@ -94,19 +94,18 @@ def BoundedOperatorNorm {Omega : Type*} [MeasurableSpace Omega] {m n : Nat}
 
 /--
 A pointwise squared-vector-norm bound gives an operator-norm bound for the
-rank-one random matrix `omega |-> X(omega) X(omega)^T`.
+named rank-one random matrix `rankOneRandomMatrix X`.
 
 Formula reference: the deterministic ingredient is
 `||v v^T||op <= ||v||_2^2` for a rank-one outer product; see
 https://en.wikipedia.org/wiki/Outer_product and
 https://en.wikipedia.org/wiki/Operator_norm
 -/
-theorem BoundedOperatorNorm_rankOne_of_sqNorm_bound {Omega : Type*}
+theorem BoundedOperatorNorm_rankOneRandomMatrix_of_sqNorm_bound {Omega : Type*}
     [MeasurableSpace Omega] {n : Nat}
-    (X : Omega -> Fin n -> Real) (R : Real)
-    (_hR : 0 <= R)
+    (X : RandomVector Omega n) (R : Real)
     (hX : forall omega, vectorSqNorm (X omega) <= R) :
-    BoundedOperatorNorm (fun omega i j => X omega i * X omega j) R := by
+    BoundedOperatorNorm (rankOneRandomMatrix X) R := by
   intro omega
   exact (rankOneOperatorNorm_le_vectorSqNorm (X omega)).trans (hX omega)
 
@@ -152,23 +151,22 @@ def PointwiseOperatorNormBound {Omega : Type*} [MeasurableSpace Omega]
   forall i, BoundedOperatorNorm (A i) R
 
 /--
-Family version of the rank-one operator-norm bridge: if every vector sample has
-`vectorSqNorm <= R`, then the associated rank-one matrix family is pointwise
-operator-norm bounded by `R`.
+Family version of the named rank-one operator-norm bridge: if every vector
+sample has `vectorSqNorm <= R`, then the associated rank-one matrix family is
+pointwise operator-norm bounded by `R`.
 
 Formula reference: this packages the outer-product bound
 `||v v^T||op <= ||v||_2^2`; see
 https://en.wikipedia.org/wiki/Outer_product and
 https://en.wikipedia.org/wiki/Operator_norm
 -/
-theorem PointwiseOperatorNormBound_rankOne_of_sqNorm_bound {Omega : Type*}
+theorem PointwiseOperatorNormBound_rankOneRandomMatrix_of_sqNorm_bound {Omega : Type*}
     [MeasurableSpace Omega] {I : Type*} {n : Nat}
-    (X : I -> Omega -> Fin n -> Real) (R : Real)
-    (hR : 0 <= R)
+    (X : I -> RandomVector Omega n) (R : Real)
     (hX : forall i omega, vectorSqNorm (X i omega) <= R) :
-    PointwiseOperatorNormBound (fun i omega a b => X i omega a * X i omega b) R := by
+    PointwiseOperatorNormBound (fun i => rankOneRandomMatrix (X i)) R := by
   intro i
-  exact BoundedOperatorNorm_rankOne_of_sqNorm_bound (X i) R hR (hX i)
+  exact BoundedOperatorNorm_rankOneRandomMatrix_of_sqNorm_bound (X i) R (hX i)
 
 /--
 Family version of the centered operator-norm bridge under an explicit bound on

HighDimProb/RandomMatrix/Basic.lean

@@ -64,6 +64,24 @@ theorem matrixEntry_apply {Omega : Type*} [MeasurableSpace Omega] {m n : Nat}
     matrixEntry A i j omega = A omega i j :=
   rfl
 
+/--
+Deterministic rank-one self outer-product matrix associated to a vector.
+
+Formula reference: the outer product has entries `x_i * x_j`; see
+https://en.wikipedia.org/wiki/Outer_product .
+-/
+def rankOneMatrix {n : Nat} (x : Fin n -> Real) : Matrix (Fin n) (Fin n) Real :=
+  fun i j => x i * x j
+
+/--
+Formula reference: this unfolds the rank-one outer-product entry `x_i * x_j`;
+see https://en.wikipedia.org/wiki/Outer_product .
+-/
+@[simp]
+theorem rankOneMatrix_apply {n : Nat} (x : Fin n -> Real) (i j : Fin n) :
+    rankOneMatrix x i j = x i * x j :=
+  rfl
+
 /--
 Rank-one self outer-product random matrix associated to a random vector.
 
@@ -75,7 +93,7 @@ https://en.wikipedia.org/wiki/Random_vector .
 -/
 def rankOneRandomMatrix {Omega : Type*} [MeasurableSpace Omega] {n : Nat}
     (X : RandomVector Omega n) : RandomMatrix Omega n n :=
-  fun omega i j => X omega i * X omega j
+  fun omega => rankOneMatrix (X omega)
 
 /--
 Formula reference: this unfolds the rank-one outer-product entry

HighDimProb/RandomMatrix/OperatorNorm.lean

@@ -109,18 +109,18 @@ https://en.wikipedia.org/wiki/Operator_norm
 -/
 theorem rankOneOperatorNorm_le_vectorSqNorm {n : Nat}
     (v : Fin n -> Real) :
-    deterministicOperatorNorm (fun i j : Fin n => v i * v j) <= vectorSqNorm v := by
+    deterministicOperatorNorm (rankOneMatrix v) <= vectorSqNorm v := by
   rw [deterministicOperatorNorm, Matrix.l2_opNorm_def]
   refine ContinuousLinearMap.opNorm_le_bound _ (vectorSqNorm_nonneg v) ?_
   intro y
   have happly :
       (((Matrix.toEuclideanLin (𝕜 := Real) (m := Fin n) (n := Fin n)).trans
             LinearMap.toContinuousLinearMap)
-          (fun i j : Fin n => v i * v j) y) =
+          (rankOneMatrix v) y) =
         (inner Real (WithLp.toLp 2 v : EuclideanSpace Real (Fin n)) y) •
           (WithLp.toLp 2 v : EuclideanSpace Real (Fin n)) := by
     ext i
-    simp [Matrix.toLpLin_apply, Matrix.mulVec, dotProduct, inner]
+    simp [rankOneMatrix, Matrix.toLpLin_apply, Matrix.mulVec, dotProduct, inner]
     rw [Finset.sum_mul]
     apply Finset.sum_congr rfl
     intro j _

HighDimProb/RandomMatrix/Spectral.lean

@@ -380,6 +380,67 @@ 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
+forces the vector into the kernel; one proof uses the PSD square root, see
+https://en.wikipedia.org/wiki/Definite_matrix#Square_root .  This theorem is a
+thin wrapper over Mathlib's `Matrix.PosSemidef.dotProduct_mulVec_zero_iff`. -/
+theorem matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_posSemidef {n : Nat}
+    {A : Matrix (Fin n) (Fin n) Real} (hA : A.PosSemidef)
+    (x : Fin n -> Real) :
+    matrixQuadraticForm A x = 0 <-> Matrix.mulVec A x = 0 := by
+  have h := hA.dotProduct_mulVec_zero_iff x
+  simpa [matrixQuadraticForm, dotProduct, Matrix.mulVec,
+    Finset.mul_sum, Finset.sum_mul, mul_assoc] using h
+
+/-- One-way PSD nullspace converse from a zero HighDimProb quadratic form. -/
+theorem matrix_mulVec_eq_zero_of_posSemidef_quadraticForm_eq_zero {n : Nat}
+    {A : Matrix (Fin n) (Fin n) Real} (hA : A.PosSemidef)
+    {x : Fin n -> Real} (hx : matrixQuadraticForm A x = 0) :
+    Matrix.mulVec A x = 0 :=
+  (matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_posSemidef hA x).mp hx
+
+/-- Explicit-PSD version of the PSD nullspace iff.
+
+Formula reference: the statement is the usual PSD nullspace converse for
+symmetric positive semidefinite real matrices; see
+https://math.stackexchange.com/questions/3918031/prove-that-if-xtax-0-rightarrow-ax-0 .
+-/
+theorem matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_isPSDMatrix {n : Nat}
+    {A : Matrix (Fin n) (Fin n) Real} (hA : IsPSDMatrix A)
+    (x : Fin n -> Real) :
+    matrixQuadraticForm A x = 0 <-> Matrix.mulVec A x = 0 :=
+  matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_posSemidef
+    (posSemidef_of_isPSDMatrix hA) x
+
+/-- One-way explicit-PSD nullspace converse from a zero HighDimProb quadratic
+form. -/
+theorem matrix_mulVec_eq_zero_of_isPSDMatrix_quadraticForm_eq_zero {n : Nat}
+    {A : Matrix (Fin n) (Fin n) Real} (hA : IsPSDMatrix A)
+    {x : Fin n -> Real} (hx : matrixQuadraticForm A x = 0) :
+    Matrix.mulVec A x = 0 :=
+  (matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_isPSDMatrix hA x).mp hx
+
 /-- Scalar-matrix quadratic form over an explicit unit vector.
 
 This is the small algebraic bridge needed to turn a Loewner-order upper bound

HighDimProbJudge/RandomMatrix/OperatorNormUse.lean

@@ -3,8 +3,8 @@ import HighDimProb.RandomMatrix
 #check HighDimProb.isRealRandomVariable_operatorNorm
 #check HighDimProb.deterministicOperatorNorm_sub_le_add
 #check HighDimProb.rankOneOperatorNorm_le_vectorSqNorm
-#check HighDimProb.BoundedOperatorNorm_rankOne_of_sqNorm_bound
-#check HighDimProb.PointwiseOperatorNormBound_rankOne_of_sqNorm_bound
+#check HighDimProb.BoundedOperatorNorm_rankOneRandomMatrix_of_sqNorm_bound
+#check HighDimProb.PointwiseOperatorNormBound_rankOneRandomMatrix_of_sqNorm_bound
 #check HighDimProb.BoundedOperatorNorm_centered_of_bound_expect_bound
 #check HighDimProb.PointwiseOperatorNormBound_centered_of_bound_expect_bound
 #check HighDimProb.PointwiseOperatorNormBound_centered_of_bound_expect_bound_same
@@ -26,7 +26,7 @@ example {Omega : Type*} [MeasurableSpace Omega]
 
 example {n : Nat} (v : Fin n -> Real) :
     HighDimProb.deterministicOperatorNorm
-      (fun i j : Fin n => v i * v j) <= HighDimProb.vectorSqNorm v := by
+      (HighDimProb.rankOneMatrix v) <= HighDimProb.vectorSqNorm v := by
   exact HighDimProb.rankOneOperatorNorm_le_vectorSqNorm v
 
 example {m n : Nat} (A B : Matrix (Fin m) (Fin n) Real) :
@@ -36,11 +36,10 @@ example {m n : Nat} (A B : Matrix (Fin m) (Fin n) Real) :
 
 example {Omega : Type*} [MeasurableSpace Omega] {I : Type*} {n : Nat}
     (X : I -> Omega -> Fin n -> Real) (R : Real)
-    (hR : 0 <= R)
     (hX : forall i omega, HighDimProb.vectorSqNorm (X i omega) <= R) :
     HighDimProb.PointwiseOperatorNormBound
-      (fun i omega a b => X i omega a * X i omega b) R := by
-  exact HighDimProb.PointwiseOperatorNormBound_rankOne_of_sqNorm_bound X R hR hX
+      (fun i => HighDimProb.rankOneRandomMatrix (X i)) R := by
+  exact HighDimProb.PointwiseOperatorNormBound_rankOneRandomMatrix_of_sqNorm_bound X R hX
 
 example {Omega : Type*} [MeasurableSpace Omega] {I : Type*} {m n : Nat}
     (P : MeasureTheory.Measure Omega) (X : I -> HighDimProb.RandomMatrix Omega m n)

HighDimProbJudge/RandomMatrix/SpectralUse.lean

@@ -31,6 +31,11 @@ import HighDimProb.RandomMatrix
 #check HighDimProb.spectralUpperBound_of_lambdaMaxPSDUpperBound
 #check HighDimProb.spectralUpperBound_of_lambdaMaxOrderedPSDUpperBound
 #check HighDimProb.matrixQuadraticForm_nonneg_of_posSemidef
+#check HighDimProb.posSemidef_of_isPSDMatrix
+#check HighDimProb.matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_posSemidef
+#check HighDimProb.matrix_mulVec_eq_zero_of_posSemidef_quadraticForm_eq_zero
+#check HighDimProb.matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_isPSDMatrix
+#check HighDimProb.matrix_mulVec_eq_zero_of_isPSDMatrix_quadraticForm_eq_zero
 #check HighDimProb.matrixQuadraticForm_smul_one_of_isUnitVector
 #check HighDimProb.rayleighUpperBound_of_spectralUpperBound
 #check HighDimProb.matrixQuadraticForm_le_lambdaMax_of_lambdaMax_sub_posSemidef
@@ -134,6 +139,39 @@ example {n : Nat} (A : Matrix (Fin n) (Fin n) Real)
     0 <= HighDimProb.matrixQuadraticForm A x := by
   exact HighDimProb.matrixQuadraticForm_nonneg_of_posSemidef hA x
 
+example {n : Nat} (A : Matrix (Fin n) (Fin n) Real)
+    (hA : HighDimProb.IsPSDMatrix A) :
+    Matrix.PosSemidef A := by
+  exact HighDimProb.posSemidef_of_isPSDMatrix hA
+
+example {n : Nat} (A : Matrix (Fin n) (Fin n) Real)
+    (x : Fin n -> Real) (hA : A.PosSemidef) :
+    HighDimProb.matrixQuadraticForm A x = 0 <->
+      Matrix.mulVec A x = 0 := by
+  exact HighDimProb.matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_posSemidef
+    hA x
+
+example {n : Nat} (A : Matrix (Fin n) (Fin n) Real)
+    (x : Fin n -> Real) (hA : A.PosSemidef)
+    (hx : HighDimProb.matrixQuadraticForm A x = 0) :
+    Matrix.mulVec A x = 0 := by
+  exact HighDimProb.matrix_mulVec_eq_zero_of_posSemidef_quadraticForm_eq_zero
+    hA hx
+
+example {n : Nat} (A : Matrix (Fin n) (Fin n) Real)
+    (x : Fin n -> Real) (hA : HighDimProb.IsPSDMatrix A) :
+    HighDimProb.matrixQuadraticForm A x = 0 <->
+      Matrix.mulVec A x = 0 := by
+  exact HighDimProb.matrixQuadraticForm_eq_zero_iff_mulVec_eq_zero_of_isPSDMatrix
+    hA x
+
+example {n : Nat} (A : Matrix (Fin n) (Fin n) Real)
+    (x : Fin n -> Real) (hA : HighDimProb.IsPSDMatrix A)
+    (hx : HighDimProb.matrixQuadraticForm A x = 0) :
+    Matrix.mulVec A x = 0 := by
+  exact HighDimProb.matrix_mulVec_eq_zero_of_isPSDMatrix_quadraticForm_eq_zero
+    hA hx
+
 example {n : Nat} (x : Fin n -> Real) (c : Real)
     (hx : HighDimProb.IsUnitVector x) :
     HighDimProb.matrixQuadraticForm