Add rank-one operator norm boundedness bridge

HighDimProb/RandomMatrix/Assumptions.lean

@@ -92,12 +92,49 @@ def BoundedOperatorNorm {Omega : Type*} [MeasurableSpace Omega] {m n : Nat}
     (A : RandomMatrix Omega m n) (R : Real) : Prop :=
   forall omega, operatorNorm A omega <= R
 
+/--
+A pointwise squared-vector-norm bound gives an operator-norm bound for the
+rank-one random matrix `omega |-> X(omega) X(omega)^T`.
+
+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*}
+    [MeasurableSpace Omega] {n : Nat}
+    (X : Omega -> Fin n -> Real) (R : Real)
+    (_hR : 0 <= R)
+    (hX : forall omega, vectorSqNorm (X omega) <= R) :
+    BoundedOperatorNorm (fun omega i j => X omega i * X omega j) R := by
+  intro omega
+  exact (rankOneOperatorNorm_le_vectorSqNorm (X omega)).trans (hX omega)
+
 /-- Pointwise uniform operator-norm bound for a matrix family. -/
 def PointwiseOperatorNormBound {Omega : Type*} [MeasurableSpace Omega]
     {I : Type*} {m n : Nat} (A : I -> RandomMatrix Omega m n)
     (R : Real) : Prop :=
   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`.
+
+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*}
+    [MeasurableSpace Omega] {I : Type*} {n : Nat}
+    (X : I -> Omega -> Fin n -> Real) (R : Real)
+    (hR : 0 <= R)
+    (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
+  intro i
+  exact BoundedOperatorNorm_rankOne_of_sqNorm_bound (X i) R hR (hX i)
+
 /-- Alias emphasizing that the uniform bound is pointwise, not a.e. -/
 abbrev UniformOperatorNormBound {Omega : Type*} [MeasurableSpace Omega]
     {I : Type*} {m n : Nat} (A : I -> RandomMatrix Omega m n)

HighDimProb/RandomMatrix/OperatorNorm.lean

@@ -82,6 +82,48 @@ theorem deterministicOperatorNorm_apply {m n : Nat}
     deterministicOperatorNorm A = norm A :=
   rfl
 
+/--
+Rank-one self-outer products have operator norm bounded by the squared
+Euclidean norm of the vector.
+
+Formula reference: for the outer product `v vᵀ`, multiplication sends
+`x` to `<v, x> v`; Cauchy--Schwarz gives
+`||<v, x> v||₂ <= ||v||₂^2 ||x||₂`, hence the induced operator-norm bound.
+See https://en.wikipedia.org/wiki/Outer_product and
+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
+  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) =
+        (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]
+    rw [Finset.sum_mul]
+    apply Finset.sum_congr rfl
+    intro j _
+    ring
+  rw [happly]
+  calc
+    ‖(inner Real (WithLp.toLp 2 v : EuclideanSpace Real (Fin n)) y) •
+          (WithLp.toLp 2 v : EuclideanSpace Real (Fin n))‖
+        = |inner Real (WithLp.toLp 2 v : EuclideanSpace Real (Fin n)) y| *
+            ‖(WithLp.toLp 2 v : EuclideanSpace Real (Fin n))‖ := by
+          rw [norm_smul, Real.norm_eq_abs]
+    _ <= ‖(WithLp.toLp 2 v : EuclideanSpace Real (Fin n))‖ * ‖y‖ *
+            ‖(WithLp.toLp 2 v : EuclideanSpace Real (Fin n))‖ := by
+          exact mul_le_mul_of_nonneg_right (abs_real_inner_le_norm _ _) (norm_nonneg _)
+    _ = vectorSqNorm v * ‖y‖ := by
+          rw [vectorSqNorm_eq_norm_sq_toLp]
+          ring
+
 /--
 Squared Euclidean norm of the deterministic matrix-vector product.
 

HighDimProbJudge/RandomMatrix/OperatorNormUse.lean

@@ -1,6 +1,9 @@
 import HighDimProb.RandomMatrix
 
 #check HighDimProb.isRealRandomVariable_operatorNorm
+#check HighDimProb.rankOneOperatorNorm_le_vectorSqNorm
+#check HighDimProb.BoundedOperatorNorm_rankOne_of_sqNorm_bound
+#check HighDimProb.PointwiseOperatorNormBound_rankOne_of_sqNorm_bound
 
 #check
   (HighDimProb.isRealRandomVariable_operatorNorm :
@@ -16,3 +19,16 @@ example {Omega : Type*} [MeasurableSpace Omega]
     (hA : HighDimProb.IsRandomMatrix P A) :
     HighDimProb.IsRealRandomVariable P (HighDimProb.operatorNorm A) := by
   exact HighDimProb.isRealRandomVariable_operatorNorm hA
+
+example {n : Nat} (v : Fin n -> Real) :
+    HighDimProb.deterministicOperatorNorm
+      (fun i j : Fin n => v i * v j) <= HighDimProb.vectorSqNorm v := by
+  exact HighDimProb.rankOneOperatorNorm_le_vectorSqNorm v
+
+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

HighDimProbTest/ExamplesAPI.lean

@@ -13,3 +13,12 @@ import HighDimProb.Examples.RandomMatrix.NTKGramDecompositionUsage
 import HighDimProb.Examples.RandomMatrix.NTKGramUsage
 import HighDimProb.Examples.RandomMatrix.RandomFeatureKernelUsage
 import HighDimProb.Examples.RandomMatrix.RankOnePSDUsage
+
+open HighDimProb
+open HighDimProb.Examples.RandomMatrix.RankOnePSDUsage
+
+variable {rankOneN : Nat}
+variable (rankOneV : RankOneVector rankOneN)
+
+#check (rankOneOperatorNorm_le_vectorSqNorm rankOneV :
+  deterministicOperatorNorm (rankOneOuter rankOneV) <= vectorSqNorm rankOneV)

HighDimProbTest/RandomMatrixAssumptionsAPI.lean

@@ -5,20 +5,30 @@ open HighDimProb
 
 variable {Omega : Type*} [MeasurableSpace Omega]
 variable {P : Measure Omega} [IsProbabilityMeasure P]
+variable {I : Type*}
 variable {m n : Nat}
 variable (A : RandomMatrix Omega m n)
-variable (K : Real)
+variable (X : I -> Omega -> Fin n -> Real)
+variable (K R : Real)
 
 #check SubGaussianEntriesOrlicz
 #check SubGaussianEntriesTail
 #check SubGaussianRowsOrlicz
 #check IsotropicRowsSecondMoment
 #check IsotropicRowsCovariance
 #check CenteredEntries
+#check BoundedOperatorNorm_rankOne_of_sqNorm_bound
+#check PointwiseOperatorNormBound_rankOne_of_sqNorm_bound
 
 #check (SubGaussianEntriesOrlicz P A K : Prop)
 #check (SubGaussianEntriesTail P A K : Prop)
 #check (SubGaussianRowsOrlicz P A K : Prop)
 #check (IsotropicRowsSecondMoment P A : Prop)
 #check (IsotropicRowsCovariance P A : Prop)
 #check (CenteredEntries P A : Prop)
+#check (PointwiseOperatorNormBound_rankOne_of_sqNorm_bound
+  (X := X) (R := R) :
+  0 <= R ->
+  (forall i omega, vectorSqNorm (X i omega) <= R) ->
+  PointwiseOperatorNormBound
+    (fun i omega a b => X i omega a * X i omega b) R)

HighDimProbTest/RandomMatrixOperatorNormAPI.lean

@@ -5,12 +5,15 @@ open HighDimProb
 
 variable {Omega : Type*} [MeasurableSpace Omega]
 variable {P : Measure Omega} [IsProbabilityMeasure P]
+variable {I : Type*}
 variable {m n : Nat}
 variable (A : RandomMatrix Omega m n)
 variable (B C : RandomMatrix Omega n n)
 variable (M : Matrix (Fin m) (Fin n) Real)
 variable (S T : Matrix (Fin n) (Fin n) Real)
 variable (x : Fin n -> Real)
+variable (v : Fin n -> Real)
+variable (X : I -> Omega -> Fin n -> Real)
 variable (L t bound : Real)
 variable (hA : IsRandomMatrix P A)
 
@@ -31,6 +34,7 @@ variable (hA : IsRandomMatrix P A)
 #check instOpensMeasurableSpaceMatrixL2Operator
 #check deterministicOperatorNorm
 #check deterministicOperatorNorm_apply
+#check rankOneOperatorNorm_le_vectorSqNorm
 #check matVecSqNorm
 #check matVecSqNorm_apply
 #check matVecSqNorm_nonneg
@@ -61,6 +65,8 @@ variable (hA : IsRandomMatrix P A)
 #check (IsUnitVector x : Prop)
 #check (unitSphere n : Set (Fin n -> Real))
 #check (deterministicOperatorNorm M : Real)
+#check (rankOneOperatorNorm_le_vectorSqNorm v :
+  deterministicOperatorNorm (fun i j : Fin n => v i * v j) <= vectorSqNorm v)
 #check (matVecSqNorm M x : Real)
 #check (randomMatVecSqNorm A x : RealRandomVariable Omega)
 #check (sqNorm_matVec_eq_matVecSqNorm A x : forall omega, sqNorm (matVec A x) omega = matVecSqNorm (A omega) x)
@@ -77,6 +83,12 @@ variable (hA : IsRandomMatrix P A)
 #check (operatorNorm_le_of_operatorNormBoundSqStatement M L : Prop)
 #check (operatorNormBoundSq_of_operatorNorm_leStatement M L : Prop)
 #check (operatorNormMeasurabilityStatement P A : Prop)
+#check (PointwiseOperatorNormBound_rankOne_of_sqNorm_bound
+  (X := X) (R := L) :
+  0 <= L ->
+  (forall i omega, vectorSqNorm (X i omega) <= L) ->
+  PointwiseOperatorNormBound
+    (fun i omega a b => X i omega a * X i omega b) L)
 #check (matrixQuadraticForm_sub T S x :
   matrixQuadraticForm (T - S) x = matrixQuadraticForm T x - matrixQuadraticForm S x)
 #check (quadraticForm_le_of_matrixLE (A := S) (B := T) : MatrixLE S T -> forall x, matrixQuadraticForm S x <= matrixQuadraticForm T x)

docs/AbstractionLog.md

@@ -1199,3 +1199,20 @@
 - Remaining upgrade path: prove matrix Laplace / trace-mgf inequalities and
   spectral/operator-norm tail reductions using this trace-exp positivity
   bridge as infrastructure.
+
+## RM rank-one operator-norm boundedness bridge
+
+- Concrete version chosen: prove the rank-one self-outer-product bound directly
+  against `deterministicOperatorNorm` instead of introducing a new rank-one
+  matrix object or changing the matrix norm convention.
+- Proof-pattern decision: view `v vᵀ` as the linear map `x ↦ <v, x> v` and use
+  Cauchy--Schwarz plus `ContinuousLinearMap.opNorm_le_bound` under Mathlib's
+  scoped L2 operator norm.
+- Assumption decision: the random wrappers consume an explicit pointwise
+  `vectorSqNorm <= R` hypothesis and keep the nonnegative-radius argument
+  visible, rather than inferring expectation or centered bounds.
+- Comment/source decision: Lean comments include public operator-norm and outer
+  product URLs so readers can verify the mathematical formula.
+- Future upgrade path: next add the centered operator-norm triangle wrapper;
+  then handle vector-to-rank-one measurability/integrability and PSD nullspace
+  converse as separate concept clusters.

docs/BookProgress.md

@@ -973,3 +973,24 @@ finite-family Tropp typed primitive into the high-level bounded trace-MGF
 statement. The finite-family Tropp primitive, Bernstein CFC primitive, Lieb,
 Golden-Thompson, and Matrix Bernstein tail theorem remain unproved.
 Next safe task: MB-S9-trace-mgf-to-laplace-tail-contract.
+
+## RM rank-one operator-norm prerequisite progress
+
+The first rank-one prerequisite slice for covariance-style RandomMatrix examples
+is proved:
+
+```lean
+rankOneOperatorNorm_le_vectorSqNorm
+BoundedOperatorNorm_rankOne_of_sqNorm_bound
+PointwiseOperatorNormBound_rankOne_of_sqNorm_bound
+```
+
+The deterministic lemma proves the finite-dimensional bound
+`||v vᵀ||op <= ||v||₂²` using the existing `deterministicOperatorNorm` /
+Mathlib L2 operator-norm convention. The wrappers turn pointwise vector
+squared-norm bounds into `BoundedOperatorNorm` and
+`PointwiseOperatorNormBound` for rank-one random matrices.
+
+This is not a centered summand bound, not a vector-to-matrix
+measurability/integrability bridge, not a PSD nullspace converse, and not a
+Matrix Bernstein tail theorem. Next safe task: RM-centered-operator-norm-bound.

docs/MatrixBernsteinProofPlan.md

@@ -41,7 +41,7 @@ Tropp/Lieb, Golden-Thompson, the Bernstein CFC primitive, the `t = 0` endpoint
 for the optimized wrapper, lambda-max/operator-norm Matrix Bernstein tails, or
 the full Matrix Bernstein tail theorem.
 
-Next safe task: `MB-S9-lambda-max-operator-norm-bridge-contract`.
+Next safe task: `RM-centered-operator-norm-bound`.
 ## Target Theorem
 
 For a finite family of independent centered self-adjoint random matrices

docs/MatrixConcentrationPlan.md

@@ -22,7 +22,7 @@ compatibility APIs around the bounded-Bernstein lintegral Laplace route:
 `matrixBernsteinTraceMGFToLaplaceContract_statement` and
 `matrixBernsteinTraceMGFToLaplaceContract_under_primitives_statement`.
 
-Next safe task: `MB-S9-lambda-max-operator-norm-bridge-contract`.
+Next safe task: `RM-centered-operator-norm-bound`.
 Stage MC1 starts the matrix concentration branch after the scalar concentration
 closeout. It adds the assumption vocabulary, explicit matrix order vocabulary,
 matrix expectation wrappers, and typed theorem-statement layer needed before

docs/RandomMatrixAPI.md

@@ -39,7 +39,11 @@ mainline. It is documentation only; theorem status is not upgraded here.
 - Its RHS is:
   `ENNReal.ofReal ((n + 1 : Real) * Real.exp (-(t ^ 2 / (2 * sigmaSq + (2 / 3) * R * t))))`.
 - Lambda-max/operator-norm Matrix Bernstein tail theorem remains unproved.
-- Next safe task: `MB-S9-lambda-max-operator-norm-bridge-contract`.
+- Proved rank-one operator-norm prerequisite bridge:
+  `rankOneOperatorNorm_le_vectorSqNorm`,
+  `BoundedOperatorNorm_rankOne_of_sqNorm_bound`, and
+  `PointwiseOperatorNormBound_rankOne_of_sqNorm_bound`.
+- Next safe task: `RM-centered-operator-norm-bound`.
 
 ## `HighDimProb/RandomMatrix/SelfAdjoint.lean`
 
@@ -91,6 +95,32 @@ mainline. It is documentation only; theorem status is not upgraded here.
 - `lambdaMax_le_iff_quadraticForm_le_statement`: typed statement.
 - `operatorNorm_eq_max_abs_lambda_statement`: typed statement.
 
+## `HighDimProb/RandomMatrix/OperatorNorm.lean`
+
+- `operatorNorm`: def, random-matrix operator norm as a real random variable.
+- `deterministicOperatorNorm`: def, deterministic matrix operator norm using the
+  same scoped L2 convention.
+- `deterministicOperatorNorm_apply`: theorem, definitional bridge.
+- `rankOneOperatorNorm_le_vectorSqNorm`: theorem, `||v vᵀ||op <= ||v||₂²`.
+- `matVecSqNorm`: def.
+- `randomMatVecSqNorm`: def.
+- `OperatorNormBoundSq`: def.
+- `operatorNorm_le_of_operatorNormBoundSq`: theorem.
+- `operatorNormBoundSq_of_operatorNorm_le`: theorem.
+- `isRealRandomVariable_operatorNorm`: theorem.
+
+## `HighDimProb/RandomMatrix/Assumptions.lean`
+
+- `BoundedOperatorNorm`: def, pointwise operator-norm bound for one random
+  matrix.
+- `BoundedOperatorNorm_rankOne_of_sqNorm_bound`: theorem, rank-one pointwise
+  wrapper from vector squared-norm bounds.
+- `PointwiseOperatorNormBound`: def, indexed pointwise operator-norm bound.
+- `PointwiseOperatorNormBound_rankOne_of_sqNorm_bound`: theorem, indexed
+  rank-one wrapper from vector squared-norm bounds.
+- `UniformOperatorNormBound`: abbrev.
+- `AeOperatorNormBound`: def.
+
 ## `HighDimProb/RandomMatrix/MatrixOrder.lean`
 
 - `matrixQuadraticForm`: def.
@@ -356,7 +386,7 @@ mainline. It is documentation only; theorem status is not upgraded here.
 
 ## Next Safe Task
 
-MB-S9-lambda-max-operator-norm-bridge-contract: plan the bridge from the proved
+RM-centered-operator-norm-bound: plan the bridge from the proved
 one-sided optimized quadratic-form under-primitives tail to lambda-max and then
 operator-norm Matrix Bernstein tails. Do not prove Tropp/Lieb, Bernstein CFC,
 Golden-Thompson, or the full Matrix Bernstein theorem in that contract stage.
@@ -383,4 +413,4 @@ Golden-Thompson, or the full Matrix Bernstein theorem in that contract stage.
   proved in `ConcentrationStatements.lean`, with exponential-add RHS.
 - The theta-optimized scalar-RHS quadratic-form wrapper under primitives is now
   proved in `ConcentrationStatements.lean`, with Bernstein denominator RHS.
-- Next safe task: MB-S9-lambda-max-operator-norm-bridge-contract.
+- Next safe task: RM-centered-operator-norm-bound.

docs/Status.md

@@ -8,27 +8,27 @@ RandomMatrix / Matrix Bernstein mainline: MB-S9 now includes the bounded
 trace-MGF theorem under explicit primitives, the bounded real-to-lintegral
 trace-MGF bridge, the explicit-theta quadratic-form upper-tail wrappers, the
 dimension/norm scalar RHS reduction, and the theta-optimized scalar Bernstein
-denominator wrapper. The newest layer chooses
-`theta = t / (sigmaSq + R * t / 3)` via `bernsteinThetaChoice` and proves the
-conservative exponent form
-`-(t ^ 2 / (2 * sigmaSq + (2 / 3) * R * t))`.
+denominator wrapper. The current prerequisite cleanup also adds the first
+rank-one operator-norm bridge for covariance-style examples.
 
 The latest proved public theorem is:
 
-- `matrixBernsteinQuadraticFormUpperTailOptimizedScalarRHSWithBernsteinCoeff_under_primitives`
+- `PointwiseOperatorNormBound_rankOne_of_sqNorm_bound`
 
-The wrapper proves a one-sided nonempty-dimensional quadratic-form upper-tail
-bound under explicit primitive assumptions, with RHS:
-`ENNReal.ofReal ((n + 1 : Real) * Real.exp (-(t ^ 2 / (2 * sigmaSq + (2 / 3) * R * t))))`.
-Supporting scalar API includes `bernsteinThetaChoice`,
-`bernsteinThetaChoice_range`, and `bernsteinThetaChoice_exponent_eq`. It still
-does not prove lambda-max/operator-norm Matrix Bernstein tails, Tropp/Lieb, the
-Bernstein CFC primitive, Golden-Thompson, the `t = 0` endpoint for the
-optimized wrapper, or the final full Matrix Bernstein tail theorem.
+Supporting proved API also includes `rankOneOperatorNorm_le_vectorSqNorm` and
+`BoundedOperatorNorm_rankOne_of_sqNorm_bound`. These are deterministic /
+pointwise boundedness bridges only: they do not prove centered summand
+boundedness, vector-to-rank-one matrix measurability or integrability, the PSD
+nullspace converse, lambda-max/operator-norm Matrix Bernstein tails,
+Tropp/Lieb, the Bernstein CFC primitive, Golden-Thompson, the `t = 0` endpoint
+for the optimized wrapper, or the final full Matrix Bernstein tail theorem.
+The previous optimized quadratic-form theorem remains
+`matrixBernsteinQuadraticFormUpperTailOptimizedScalarRHSWithBernsteinCoeff_under_primitives`
+under explicit primitive assumptions.
 
 ## Next Safe Task
 
-- `MB-S9-lambda-max-operator-norm-bridge-contract`
+- `RM-centered-operator-norm-bound`
 
 ## Public Milestone Summary
 
@@ -140,6 +140,7 @@ Last known test status:
 - Stage V1 Lean path visualization infrastructure
 - Stage J1 HighDimProb compile-time OJ / judge suite
 - Stage J2 expanded HighDimProb judge coverage
+- Stage RM-rank-one operator-norm bound for covariance-style rank-one matrices
 
 Stage 1A implemented:
 - probability-space convention