Add centered operator norm boundedness bridge

HighDimProb/RandomMatrix/Assumptions.lean

@@ -110,6 +110,41 @@ theorem BoundedOperatorNorm_rankOne_of_sqNorm_bound {Omega : Type*}
   intro omega
   exact (rankOneOperatorNorm_le_vectorSqNorm (X omega)).trans (hX omega)
 
+/--
+If a random matrix and its deterministic entrywise expectation have explicit
+operator-norm bounds, then the centered random matrix is bounded by the sum of
+those two bounds.
+
+This is only an algebraic triangle-inequality wrapper around the existing
+`matrixExpect` / `centeredRandomMatrix` vocabulary. It does not prove
+entrywise integrability, measurability, or any contraction theorem bounding
+`||E X||op` from the pointwise bound on `X`; the expectation norm bound is an
+explicit hypothesis.
+
+Formula reference: centering uses `X(omega) - E X`, and the proof is the
+operator-norm triangle inequality `||X(omega) - E X|| <= ||X(omega)|| +
+||E X||`; see https://en.wikipedia.org/wiki/Operator_norm and the sample
+covariance/expectation background at
+https://en.wikipedia.org/wiki/Sample_mean_and_covariance
+-/
+theorem BoundedOperatorNorm_centered_of_bound_expect_bound {Omega : Type*}
+    [MeasurableSpace Omega] {m n : Nat}
+    (P : Measure Omega) (X : RandomMatrix Omega m n) (R Rexp : Real)
+    (hX : BoundedOperatorNorm X R)
+    (hExp : deterministicOperatorNorm (matrixExpect P X) <= Rexp) :
+    BoundedOperatorNorm (centeredRandomMatrix P X) (R + Rexp) := by
+  intro omega
+  have hTri :
+      deterministicOperatorNorm (X omega - matrixExpect P X) <=
+        deterministicOperatorNorm (X omega) +
+          deterministicOperatorNorm (matrixExpect P X) :=
+    deterministicOperatorNorm_sub_le_add (X omega) (matrixExpect P X)
+  have hBound :
+      deterministicOperatorNorm (X omega) +
+          deterministicOperatorNorm (matrixExpect P X) <= R + Rexp :=
+    add_le_add (hX omega) hExp
+  exact hTri.trans hBound
+
 /-- 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)
@@ -135,6 +170,47 @@ theorem PointwiseOperatorNormBound_rankOne_of_sqNorm_bound {Omega : Type*}
   intro i
   exact BoundedOperatorNorm_rankOne_of_sqNorm_bound (X i) R hR (hX i)
 
+/--
+Family version of the centered operator-norm bridge under an explicit bound on
+each deterministic expectation.
+
+This is the family form of the algebraic wrapper above. It intentionally keeps
+the expectation operator-norm bound as a hypothesis and does not establish
+integrability or expectation contraction.
+
+Formula reference: this packages the triangle-bound route
+`||X_i(omega) - E X_i|| <= ||X_i(omega)|| + ||E X_i||`; see
+https://en.wikipedia.org/wiki/Operator_norm and
+https://en.wikipedia.org/wiki/Sample_mean_and_covariance
+-/
+theorem PointwiseOperatorNormBound_centered_of_bound_expect_bound {Omega : Type*}
+    [MeasurableSpace Omega] {I : Type*} {m n : Nat}
+    (P : Measure Omega) (X : I -> RandomMatrix Omega m n) (R Rexp : Real)
+    (hX : PointwiseOperatorNormBound X R)
+    (hExp : forall i, deterministicOperatorNorm (matrixExpect P (X i)) <= Rexp) :
+    PointwiseOperatorNormBound (fun i => centeredRandomMatrix P (X i)) (R + Rexp) := by
+  intro i
+  exact BoundedOperatorNorm_centered_of_bound_expect_bound P (X i) R Rexp
+    (hX i) (hExp i)
+
+/--
+Same-radius centered operator-norm wrapper: if both `X_i(omega)` and
+`E X_i` are bounded by `R`, then the centered family is bounded by `R + R`.
+
+This remains an explicit-bound wrapper; the hypothesis on `E X_i` is not
+derived from the pointwise bound on `X_i`.
+
+Formula reference: this is the special case `R_exp = R` of the operator-norm
+triangle inequality; see https://en.wikipedia.org/wiki/Operator_norm
+-/
+theorem PointwiseOperatorNormBound_centered_of_bound_expect_bound_same {Omega : Type*}
+    [MeasurableSpace Omega] {I : Type*} {m n : Nat}
+    (P : Measure Omega) (X : I -> RandomMatrix Omega m n) (R : Real)
+    (hX : PointwiseOperatorNormBound X R)
+    (hExp : forall i, deterministicOperatorNorm (matrixExpect P (X i)) <= R) :
+    PointwiseOperatorNormBound (fun i => centeredRandomMatrix P (X i)) (R + R) := by
+  exact PointwiseOperatorNormBound_centered_of_bound_expect_bound P X R R hX hExp
+
 /-- 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,21 @@ theorem deterministicOperatorNorm_apply {m n : Nat}
     deterministicOperatorNorm A = norm A :=
   rfl
 
+/--
+The deterministic operator norm satisfies the triangle inequality for
+subtraction.
+
+Formula reference: this is the norm triangle inequality
+`||A - B|| <= ||A|| + ||B||` for the matrix norm induced by the Euclidean
+operator norm; see https://en.wikipedia.org/wiki/Operator_norm and
+https://en.wikipedia.org/wiki/Matrix_norm
+-/
+theorem deterministicOperatorNorm_sub_le_add {m n : Nat}
+    (A B : Matrix (Fin m) (Fin n) Real) :
+    deterministicOperatorNorm (A - B) <=
+      deterministicOperatorNorm A + deterministicOperatorNorm B := by
+  simpa [deterministicOperatorNorm] using norm_sub_le A B
+
 /--
 Rank-one self-outer products have operator norm bounded by the squared
 Euclidean norm of the vector.

HighDimProbJudge/RandomMatrix/OperatorNormUse.lean

@@ -1,9 +1,13 @@
 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_centered_of_bound_expect_bound
+#check HighDimProb.PointwiseOperatorNormBound_centered_of_bound_expect_bound
+#check HighDimProb.PointwiseOperatorNormBound_centered_of_bound_expect_bound_same
 
 #check
   (HighDimProb.isRealRandomVariable_operatorNorm :
@@ -25,10 +29,26 @@ example {n : Nat} (v : Fin n -> Real) :
       (fun i j : Fin n => v i * v j) <= HighDimProb.vectorSqNorm v := by
   exact HighDimProb.rankOneOperatorNorm_le_vectorSqNorm v
 
+example {m n : Nat} (A B : Matrix (Fin m) (Fin n) Real) :
+    HighDimProb.deterministicOperatorNorm (A - B) <=
+      HighDimProb.deterministicOperatorNorm A + HighDimProb.deterministicOperatorNorm B := by
+  exact HighDimProb.deterministicOperatorNorm_sub_le_add A B
+
 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
+
+example {Omega : Type*} [MeasurableSpace Omega] {I : Type*} {m n : Nat}
+    (P : MeasureTheory.Measure Omega) (X : I -> HighDimProb.RandomMatrix Omega m n)
+    (R Rexp : Real)
+    (hX : HighDimProb.PointwiseOperatorNormBound X R)
+    (hExp : forall i,
+      HighDimProb.deterministicOperatorNorm (HighDimProb.matrixExpect P (X i)) <= Rexp) :
+    HighDimProb.PointwiseOperatorNormBound
+      (fun i => HighDimProb.centeredRandomMatrix P (X i)) (R + Rexp) := by
+  exact HighDimProb.PointwiseOperatorNormBound_centered_of_bound_expect_bound
+    P X R Rexp hX hExp

HighDimProbTest/RandomMatrixAssumptionsAPI.lean

@@ -8,6 +8,7 @@ variable {P : Measure Omega} [IsProbabilityMeasure P]
 variable {I : Type*}
 variable {m n : Nat}
 variable (A : RandomMatrix Omega m n)
+variable (B : I -> RandomMatrix Omega m n)
 variable (X : I -> Omega -> Fin n -> Real)
 variable (K R : Real)
 
@@ -19,6 +20,9 @@ variable (K R : Real)
 #check CenteredEntries
 #check BoundedOperatorNorm_rankOne_of_sqNorm_bound
 #check PointwiseOperatorNormBound_rankOne_of_sqNorm_bound
+#check BoundedOperatorNorm_centered_of_bound_expect_bound
+#check PointwiseOperatorNormBound_centered_of_bound_expect_bound
+#check PointwiseOperatorNormBound_centered_of_bound_expect_bound_same
 
 #check (SubGaussianEntriesOrlicz P A K : Prop)
 #check (SubGaussianEntriesTail P A K : Prop)
@@ -32,3 +36,18 @@ variable (K R : Real)
   (forall i omega, vectorSqNorm (X i omega) <= R) ->
   PointwiseOperatorNormBound
     (fun i omega a b => X i omega a * X i omega b) R)
+#check (BoundedOperatorNorm_centered_of_bound_expect_bound
+  (P := P) (X := A) (R := R) (Rexp := K) :
+  BoundedOperatorNorm A R ->
+  deterministicOperatorNorm (matrixExpect P A) <= K ->
+  BoundedOperatorNorm (centeredRandomMatrix P A) (R + K))
+#check (PointwiseOperatorNormBound_centered_of_bound_expect_bound
+  (P := P) (X := B) (R := R) (Rexp := K) :
+  PointwiseOperatorNormBound B R ->
+  (forall i, deterministicOperatorNorm (matrixExpect P (B i)) <= K) ->
+  PointwiseOperatorNormBound (fun i => centeredRandomMatrix P (B i)) (R + K))
+#check (PointwiseOperatorNormBound_centered_of_bound_expect_bound_same
+  (P := P) (X := B) (R := R) :
+  PointwiseOperatorNormBound B R ->
+  (forall i, deterministicOperatorNorm (matrixExpect P (B i)) <= R) ->
+  PointwiseOperatorNormBound (fun i => centeredRandomMatrix P (B i)) (R + R))

HighDimProbTest/RandomMatrixConcentrationAPI.lean

@@ -126,6 +126,16 @@ variable (R sigma2 c c1 c2 t bound K : Real)
 #check (PointwiseOperatorNormBound B R : Prop)
 #check (UniformOperatorNormBound B R : Prop)
 #check (AeOperatorNormBound P B R : Prop)
+#check (BoundedOperatorNorm_centered_of_bound_expect_bound
+  (P := P) (X := A) (R := R) (Rexp := c) :
+  BoundedOperatorNorm A R ->
+  deterministicOperatorNorm (matrixExpect P A) <= c ->
+  BoundedOperatorNorm (centeredRandomMatrix P A) (R + c))
+#check (PointwiseOperatorNormBound_centered_of_bound_expect_bound
+  (P := P) (X := B) (R := R) (Rexp := c) :
+  PointwiseOperatorNormBound B R ->
+  (forall i, deterministicOperatorNorm (matrixExpect P (B i)) <= c) ->
+  PointwiseOperatorNormBound (fun i => centeredRandomMatrix P (B i)) (R + c))
 #check (randomMatrixSum B : RandomMatrix Omega n n)
 #check (MatrixVarianceProxy P B : Matrix (Fin n) (Fin n) Real)
 #check (matrixVarianceProxy P B : Matrix (Fin n) (Fin n) Real)

HighDimProbTest/RandomMatrixOperatorNormAPI.lean

@@ -34,6 +34,7 @@ variable (hA : IsRandomMatrix P A)
 #check instOpensMeasurableSpaceMatrixL2Operator
 #check deterministicOperatorNorm
 #check deterministicOperatorNorm_apply
+#check deterministicOperatorNorm_sub_le_add
 #check rankOneOperatorNorm_le_vectorSqNorm
 #check matVecSqNorm
 #check matVecSqNorm_apply
@@ -65,6 +66,8 @@ variable (hA : IsRandomMatrix P A)
 #check (IsUnitVector x : Prop)
 #check (unitSphere n : Set (Fin n -> Real))
 #check (deterministicOperatorNorm M : Real)
+#check (deterministicOperatorNorm_sub_le_add M M :
+  deterministicOperatorNorm (M - M) <= deterministicOperatorNorm M + deterministicOperatorNorm M)
 #check (rankOneOperatorNorm_le_vectorSqNorm v :
   deterministicOperatorNorm (fun i j : Fin n => v i * v j) <= vectorSqNorm v)
 #check (matVecSqNorm M x : Real)

docs/AbstractionLog.md

@@ -1216,3 +1216,20 @@
 - 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.
+
+## RM centered operator-norm boundedness bridge
+
+- Concrete version chosen: prove the deterministic triangle inequality for the
+  existing `deterministicOperatorNorm`, then package it for `centeredRandomMatrix`
+  using an explicit bound on `matrixExpect P X`.
+- Assumption decision: the wrappers require both the pointwise bound on `X` and
+  the deterministic operator-norm bound on `E X`; they do not infer expectation
+  contraction from boundedness.
+- Layering decision: this remains an algebraic boundedness bridge over the
+  current entrywise expectation vocabulary.  It deliberately does not prove
+  entrywise integrability or vector-to-rank-one measurability.
+- Review decision: independent code review approved the change; architectural
+  review flagged the risk that centered APIs can look analytically stronger than
+  they are, so Lean comments and docs now state the explicit-bound-only boundary.
+- Future upgrade path: next handle vector-to-rank-one matrix measurability /
+  integrability as a separate concept cluster, then PSD nullspace converse.

docs/BookProgress.md

@@ -993,4 +993,25 @@ squared-norm bounds into `BoundedOperatorNorm` and
 
 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.
+Matrix Bernstein tail theorem. Next safe task: RM-vector-to-matrix-measurability-integrability.
+
+## RM centered operator-norm prerequisite progress
+
+The centered boundedness slice for covariance-style RandomMatrix examples is
+proved:
+
+```lean
+deterministicOperatorNorm_sub_le_add
+BoundedOperatorNorm_centered_of_bound_expect_bound
+PointwiseOperatorNormBound_centered_of_bound_expect_bound
+PointwiseOperatorNormBound_centered_of_bound_expect_bound_same
+```
+
+The deterministic lemma packages the matrix operator-norm triangle inequality
+`||A - B||op <= ||A||op + ||B||op`.  The random-matrix wrappers apply this to
+`centeredRandomMatrix P X` under an explicit bound on
+`deterministicOperatorNorm (matrixExpect P X)`.  This is not an expectation
+contraction theorem and does not prove entrywise integrability or
+vector-to-rank-one measurability.
+
+Next safe task: RM-vector-to-matrix-measurability-integrability.

docs/MatrixBernsteinProofPlan.md

@@ -41,7 +41,13 @@ 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: `RM-centered-operator-norm-bound`.
+Next safe task: `RM-vector-to-matrix-measurability-integrability`.
+
+RM prerequisite update: the centered operator-norm bridge is now proved via
+`deterministicOperatorNorm_sub_le_add` and the explicit-expectation-bound
+wrappers in `Assumptions.lean`.  It does not prove vector-to-matrix
+measurability/integrability, PSD nullspace converse, or expectation contraction.
+
 ## Target Theorem
 
 For a finite family of independent centered self-adjoint random matrices

docs/MatrixConcentrationPlan.md

@@ -22,7 +22,13 @@ compatibility APIs around the bounded-Bernstein lintegral Laplace route:
 `matrixBernsteinTraceMGFToLaplaceContract_statement` and
 `matrixBernsteinTraceMGFToLaplaceContract_under_primitives_statement`.
 
-Next safe task: `RM-centered-operator-norm-bound`.
+Next safe task: `RM-vector-to-matrix-measurability-integrability`.
+
+RM prerequisite update: the centered operator-norm bridge is now proved via
+`deterministicOperatorNorm_sub_le_add` and the explicit-expectation-bound
+wrappers in `Assumptions.lean`.  It does not prove vector-to-matrix
+measurability/integrability, PSD nullspace converse, or expectation contraction.
+
 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

@@ -43,7 +43,13 @@ mainline. It is documentation only; theorem status is not upgraded here.
   `rankOneOperatorNorm_le_vectorSqNorm`,
   `BoundedOperatorNorm_rankOne_of_sqNorm_bound`, and
   `PointwiseOperatorNormBound_rankOne_of_sqNorm_bound`.
-- Next safe task: `RM-centered-operator-norm-bound`.
+- Proved centered operator-norm prerequisite bridge under an explicit expectation
+  operator-norm bound:
+  `deterministicOperatorNorm_sub_le_add`,
+  `BoundedOperatorNorm_centered_of_bound_expect_bound`,
+  `PointwiseOperatorNormBound_centered_of_bound_expect_bound`, and
+  `PointwiseOperatorNormBound_centered_of_bound_expect_bound_same`.
+- Next safe task: `RM-vector-to-matrix-measurability-integrability`.
 
 ## `HighDimProb/RandomMatrix/SelfAdjoint.lean`
 
@@ -101,6 +107,7 @@ mainline. It is documentation only; theorem status is not upgraded here.
 - `deterministicOperatorNorm`: def, deterministic matrix operator norm using the
   same scoped L2 convention.
 - `deterministicOperatorNorm_apply`: theorem, definitional bridge.
+- `deterministicOperatorNorm_sub_le_add`: theorem, deterministic triangle bound.
 - `rankOneOperatorNorm_le_vectorSqNorm`: theorem, `||v vᵀ||op <= ||v||₂²`.
 - `matVecSqNorm`: def.
 - `randomMatVecSqNorm`: def.
@@ -115,9 +122,16 @@ mainline. It is documentation only; theorem status is not upgraded here.
   matrix.
 - `BoundedOperatorNorm_rankOne_of_sqNorm_bound`: theorem, rank-one pointwise
   wrapper from vector squared-norm bounds.
+- `BoundedOperatorNorm_centered_of_bound_expect_bound`: theorem, centered
+  wrapper from a pointwise bound plus an explicit expectation operator-norm
+  bound.
 - `PointwiseOperatorNormBound`: def, indexed pointwise operator-norm bound.
 - `PointwiseOperatorNormBound_rankOne_of_sqNorm_bound`: theorem, indexed
   rank-one wrapper from vector squared-norm bounds.
+- `PointwiseOperatorNormBound_centered_of_bound_expect_bound`: theorem, indexed
+  centered wrapper with explicit expectation bound.
+- `PointwiseOperatorNormBound_centered_of_bound_expect_bound_same`: theorem,
+  same-radius centered wrapper.
 - `UniformOperatorNormBound`: abbrev.
 - `AeOperatorNormBound`: def.
 
@@ -386,10 +400,7 @@ mainline. It is documentation only; theorem status is not upgraded here.
 
 ## Next Safe Task
 
-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.
+RM-vector-to-matrix-measurability-integrability: next prove or isolate the entrywise measurability / integrability bridge from vector random variables to rank-one random matrices. Do not prove PSD nullspace converse, lambda-max/operator-norm Matrix Bernstein tails, Tropp/Lieb, Bernstein CFC, Golden-Thompson, or the full Matrix Bernstein theorem in that stage.
 
 ## MB-S9 Matrix Bernstein Trace-MGF Under Primitives API
 
@@ -413,4 +424,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: RM-centered-operator-norm-bound.
+- Next safe task: RM-vector-to-matrix-measurability-integrability.