Add vector-to-rank-one random matrix bridge

HighDimProb/RandomMatrix/Basic.lean

@@ -64,6 +64,40 @@ theorem matrixEntry_apply {Omega : Type*} [MeasurableSpace Omega] {m n : Nat}
     matrixEntry A i j omega = A omega i j :=
   rfl
 
+/--
+Rank-one self outer-product random matrix associated to a random vector.
+
+Formula reference: the outer product has entries `x_i * x_j`; see
+https://en.wikipedia.org/wiki/Outer_product .  This declaration only exposes
+the object-level vector-to-matrix map; measurability and integrability remain
+separate assumptions/bridges, matching the random-vector convention at
+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
+
+/--
+Formula reference: this unfolds the rank-one outer-product entry
+`X_i(omega) * X_j(omega)`; see https://en.wikipedia.org/wiki/Outer_product .
+-/
+@[simp]
+theorem rankOneRandomMatrix_apply {Omega : Type*} [MeasurableSpace Omega] {n : Nat}
+    (X : RandomVector Omega n) (omega : Omega) (i j : Fin n) :
+    rankOneRandomMatrix X omega i j = X omega i * X omega j :=
+  rfl
+
+/--
+Formula reference: the matrix entry of a rank-one outer product is the product
+of the corresponding vector coordinates; see
+https://en.wikipedia.org/wiki/Outer_product .
+-/
+@[simp]
+theorem matrixEntry_rankOneRandomMatrix {Omega : Type*} [MeasurableSpace Omega]
+    {n : Nat} (X : RandomVector Omega n) (i j : Fin n) (omega : Omega) :
+    matrixEntry (rankOneRandomMatrix X) i j omega = X omega i * X omega j :=
+  rfl
+
 /--
 Entries of an `IsRandomMatrix` are real random variables.
 
@@ -77,6 +111,22 @@ theorem isRealRandomVariable_matrixEntry {Omega : Type*} [MeasurableSpace Omega]
     IsRealRandomVariable P (matrixEntry A i j) :=
   hA i j
 
+/--
+Rank-one self outer products of random vectors are random matrices.
+
+Formula reference: each entry is the product `X_i * X_j`; measurability follows
+from closure of measurable real functions under multiplication.  See
+https://en.wikipedia.org/wiki/Outer_product and
+https://en.wikipedia.org/wiki/Measurable_function .
+-/
+theorem isRandomMatrix_rankOneRandomMatrix {Omega : Type*} [MeasurableSpace Omega]
+    {P : Measure Omega} {n : Nat} {X : RandomVector Omega n}
+    (hX : IsRandomVector P X) :
+    IsRandomMatrix P (rankOneRandomMatrix X) := by
+  intro i j
+  dsimp [IsRealRandomVariable, IsRandomVariable, matrixEntry, rankOneRandomMatrix]
+  exact (hX i).mul (hX j)
+
 /--
 Entrywise measurability gives measurability of the matrix-valued map.
 

HighDimProb/RandomMatrix/Expectation.lean

@@ -51,6 +51,44 @@ theorem centeredRandomMatrix_apply {Omega : Type*} [MeasurableSpace Omega]
     centeredRandomMatrix P A omega i j = A omega i j - matrixExpect P A i j :=
   rfl
 
+/--
+Rank-one self outer products are entrywise integrable when every coordinate
+product is explicitly integrable.
+
+Formula reference: integrability is separate from measurability for Lebesgue
+integration; see https://en.wikipedia.org/wiki/Lebesgue_integration .  This
+bridge deliberately assumes product integrability and does not infer it from
+random-vector measurability alone.
+-/
+theorem integrableRandomMatrix_rankOneRandomMatrix_of_integrable_products
+    {Omega : Type*} [MeasurableSpace Omega] {P : Measure Omega} {n : Nat}
+    {X : RandomVector Omega n}
+    (hProd : forall i : Fin n, forall j : Fin n,
+      IntegrableRealRandomVariable P (fun omega => X omega i * X omega j)) :
+    IntegrableRandomMatrix P (rankOneRandomMatrix X) := by
+  intro i j
+  change IntegrableRealRandomVariable P (fun omega => X omega i * X omega j)
+  exact hProd i j
+
+/--
+Square-moment coordinates give entrywise integrability of the rank-one
+outer-product random matrix.
+
+Formula reference: entries of the outer product are `X_i * X_j`; see
+https://en.wikipedia.org/wiki/Outer_product .  The proof reuses Mathlib's
+`MemLp.integrable_mul`, so the second-moment hypothesis is explicit rather than
+hidden inside the random-vector measurability predicate.
+-/
+theorem integrableRandomMatrix_rankOneRandomMatrix_of_memLp_two
+    {Omega : Type*} [MeasurableSpace Omega] {P : Measure Omega} {n : Nat}
+    {X : RandomVector Omega n}
+    (hX : forall i : Fin n, MemLpRealRandomVariable P (coord X i) 2) :
+    IntegrableRandomMatrix P (rankOneRandomMatrix X) := by
+  apply integrableRandomMatrix_rankOneRandomMatrix_of_integrable_products
+  intro i j
+  change Integrable ((coord X i) * (coord X j)) P
+  exact (hX i).integrable_mul (hX j)
+
 end
 
 end HighDimProb

HighDimProbJudge/RandomMatrix/SampleCovarianceUse.lean

@@ -2,6 +2,10 @@ import HighDimProb.RandomMatrix
 
 #check HighDimProb.sampleCovariance
 #check HighDimProb.sampleCovarianceEntry
+#check HighDimProb.rankOneRandomMatrix
+#check HighDimProb.isRandomMatrix_rankOneRandomMatrix
+#check HighDimProb.integrableRandomMatrix_rankOneRandomMatrix_of_integrable_products
+#check HighDimProb.integrableRandomMatrix_rankOneRandomMatrix_of_memLp_two
 #check HighDimProb.isPSD_sampleCovariance
 #check HighDimProb.randomPSDMatrix_sampleCovariance
 #check HighDimProb.quadraticForm_sampleCovariance_eq_sum_sq
@@ -18,3 +22,17 @@ example {Omega : Type*} [MeasurableSpace Omega] {m n : Nat}
     (A : HighDimProb.RandomMatrix Omega m n) (x : Fin n -> Real) (omega : Omega) :
     0 <= HighDimProb.quadraticForm (HighDimProb.sampleCovariance A) x omega := by
   exact HighDimProb.quadraticForm_sampleCovariance_nonneg A x omega
+
+example {Omega : Type*} [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega}
+    {n : Nat} {X : HighDimProb.RandomVector Omega n}
+    (hX : HighDimProb.IsRandomVector P X) :
+    HighDimProb.IsRandomMatrix P (HighDimProb.rankOneRandomMatrix X) := by
+  exact HighDimProb.isRandomMatrix_rankOneRandomMatrix hX
+
+example {Omega : Type*} [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega}
+    {n : Nat} {X : HighDimProb.RandomVector Omega n}
+    (hProd : forall i : Fin n, forall j : Fin n,
+      HighDimProb.IntegrableRealRandomVariable P
+        (fun omega => X omega i * X omega j)) :
+    HighDimProb.IntegrableRandomMatrix P (HighDimProb.rankOneRandomMatrix X) := by
+  exact HighDimProb.integrableRandomMatrix_rankOneRandomMatrix_of_integrable_products hProd

HighDimProbTest/RandomMatrixBasicAPI.lean

@@ -7,18 +7,32 @@ variable {Omega : Type*} [MeasurableSpace Omega]
 variable {P : Measure Omega} [IsProbabilityMeasure P]
 variable {m n : Nat}
 variable (A : RandomMatrix Omega m n)
+variable (X : RandomVector Omega n)
 variable (i : Fin m) (j : Fin n)
+variable (a b : Fin n)
 variable (hA : IsRandomMatrix P A)
+variable (hX : IsRandomVector P X)
 
 #check RandomMatrix
 #check matrixEntry
 #check IsRandomMatrix
 #check matrixEntry_apply
+#check rankOneRandomMatrix
+#check rankOneRandomMatrix_apply
+#check matrixEntry_rankOneRandomMatrix
 #check isRealRandomVariable_matrixEntry
+#check isRandomMatrix_rankOneRandomMatrix
 #check instMeasurableSpaceMatrix
 #check measurable_randomMatrix_of_isRandomMatrix
 
 #check (matrixEntry A i j : RealRandomVariable Omega)
+#check (rankOneRandomMatrix X : RandomMatrix Omega n n)
+#check (rankOneRandomMatrix_apply X : forall omega a b,
+  rankOneRandomMatrix X omega a b = X omega a * X omega b)
+#check (matrixEntry_rankOneRandomMatrix X a b :
+  forall omega, matrixEntry (rankOneRandomMatrix X) a b omega = X omega a * X omega b)
 #check (isRealRandomVariable_matrixEntry hA i j :
   IsRealRandomVariable P (matrixEntry A i j))
+#check (isRandomMatrix_rankOneRandomMatrix hX :
+  IsRandomMatrix P (rankOneRandomMatrix X))
 #check (measurable_randomMatrix_of_isRandomMatrix hA : Measurable A)

HighDimProbTest/RandomMatrixVarianceProxyAPI.lean

@@ -10,13 +10,17 @@ variable {m n : Nat}
 variable (A : I -> RandomMatrix Omega n n)
 variable (X : RandomMatrix Omega n n)
 variable (Y : RandomMatrix Omega m n)
+variable (Z : RandomVector Omega n)
 variable (M V : Matrix (Fin n) (Fin n) Real)
 variable (i : I)
 variable (omega : Omega)
 variable (r cidx : Fin n)
 variable (R sigma2 c theta t : Real)
 variable (hA : forall i, IsRandomMatrix P (A i))
 variable (hX : IsRandomMatrix P X)
+variable (hProdZ : forall i : Fin n, forall j : Fin n,
+  IntegrableRealRandomVariable P (fun omega => Z omega i * Z omega j))
+variable (hZ2 : forall i : Fin n, MemLpRealRandomVariable P (coord Z i) 2)
 variable (hSA : forall i, RandomSelfAdjointMatrix P (A i))
 variable (hM : IsSelfAdjointMatrix M)
 variable (hXSA : RandomSelfAdjointMatrix P X)
@@ -35,6 +39,8 @@ variable (hAsqInt : forall i, IntegrableRandomMatrix P (randomMatrixSquare (A i)
 #check CenteredSelfAdjointRandomMatrixFamily
 #check CenteredRandomSelfAdjointMatrices
 #check IntegrableRandomMatrix
+#check integrableRandomMatrix_rankOneRandomMatrix_of_integrable_products
+#check integrableRandomMatrix_rankOneRandomMatrix_of_memLp_two
 #check BoundedOperatorNorm
 #check PointwiseOperatorNormBound
 #check UniformOperatorNormBound
@@ -115,6 +121,12 @@ variable (hAsqInt : forall i, IntegrableRandomMatrix P (randomMatrixSquare (A i)
 #check (CenteredSelfAdjointRandomMatrixFamily P A : Prop)
 #check (CenteredRandomSelfAdjointMatrices P A : Prop)
 #check (IntegrableRandomMatrix P X : Prop)
+#check (integrableRandomMatrix_rankOneRandomMatrix_of_integrable_products
+  (X := Z) hProdZ :
+  IntegrableRandomMatrix P (rankOneRandomMatrix Z))
+#check (integrableRandomMatrix_rankOneRandomMatrix_of_memLp_two
+  (X := Z) hZ2 :
+  IntegrableRandomMatrix P (rankOneRandomMatrix Z))
 #check (BoundedOperatorNorm X R : Prop)
 #check (PointwiseOperatorNormBound A R : Prop)
 #check (UniformOperatorNormBound A R : Prop)

docs/AbstractionLog.md

@@ -1231,5 +1231,23 @@
 - 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.
+- Future upgrade path: next handle PSD nullspace converse as a separate concept cluster.
+
+
+## RM vector-to-rank-one matrix measurability / integrability bridge
+
+- Concrete version chosen: introduce `rankOneRandomMatrix` in the basic random
+  matrix layer, with entries `X_i * X_j`, instead of continuing to duplicate the
+  anonymous lambda shape in downstream examples.
+- Measurability decision: prove `isRandomMatrix_rankOneRandomMatrix` from
+  `IsRandomVector` by entrywise measurable multiplication, matching the existing
+  sample-covariance proof style.
+- Integrability decision: add one explicit product-integrability bridge and one
+  square-moment bridge via `MemLp.integrable_mul`; do not infer integrability
+  from measurability alone.
+- Layering decision: keep the object/measurability bridge in `Basic.lean` and
+  integrability bridges in `Expectation.lean`, where `IntegrableRandomMatrix` is
+  defined.
+- Future upgrade path: next handle PSD nullspace converse as a separate concept
+  cluster; expectation contraction and Matrix Bernstein tails remain out of
+  scope.

docs/BookProgress.md

@@ -993,7 +993,7 @@ 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-vector-to-matrix-measurability-integrability.
+Matrix Bernstein tail theorem. Next safe task: RM-PSD-nullspace-converse.
 
 ## RM centered operator-norm prerequisite progress
 
@@ -1014,4 +1014,25 @@ The deterministic lemma packages the matrix operator-norm triangle inequality
 contraction theorem and does not prove entrywise integrability or
 vector-to-rank-one measurability.
 
-Next safe task: RM-vector-to-matrix-measurability-integrability.
+Next safe task: RM-PSD-nullspace-converse.
+
+
+## RM vector-to-rank-one matrix measurability / integrability prerequisite progress
+
+The vector-to-rank-one matrix prerequisite slice is proved:
+
+```lean
+rankOneRandomMatrix
+isRandomMatrix_rankOneRandomMatrix
+integrableRandomMatrix_rankOneRandomMatrix_of_integrable_products
+integrableRandomMatrix_rankOneRandomMatrix_of_memLp_two
+```
+
+The bridge defines the rank-one random matrix entrywise as `X_i * X_j`, proves
+entrywise measurability from `IsRandomVector`, and proves entrywise
+integrability only under explicit product-integrability assumptions or explicit
+coordinate `MemLp ... 2` assumptions.  It does not prove integrability from
+measurability alone, expectation contraction, PSD nullspace converse, or Matrix
+Bernstein tails.
+
+Next safe task: RM-PSD-nullspace-converse.

docs/MatrixBernsteinProofPlan.md

@@ -41,12 +41,16 @@ 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-vector-to-matrix-measurability-integrability`.
+Next safe task: `RM-PSD-nullspace-converse`.
 
 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.
+wrappers in `Assumptions.lean`.  The vector-to-rank-one matrix bridge is also
+proved via `rankOneRandomMatrix`, `isRandomMatrix_rankOneRandomMatrix`,
+`integrableRandomMatrix_rankOneRandomMatrix_of_integrable_products`, and
+`integrableRandomMatrix_rankOneRandomMatrix_of_memLp_two`.  It does not prove
+PSD nullspace converse, expectation contraction, or integrability from
+measurability alone.
 
 ## Target Theorem
 

docs/MatrixConcentrationPlan.md

@@ -22,12 +22,16 @@ compatibility APIs around the bounded-Bernstein lintegral Laplace route:
 `matrixBernsteinTraceMGFToLaplaceContract_statement` and
 `matrixBernsteinTraceMGFToLaplaceContract_under_primitives_statement`.
 
-Next safe task: `RM-vector-to-matrix-measurability-integrability`.
+Next safe task: `RM-PSD-nullspace-converse`.
 
 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.
+wrappers in `Assumptions.lean`.  The vector-to-rank-one matrix bridge is also
+proved via `rankOneRandomMatrix`, `isRandomMatrix_rankOneRandomMatrix`,
+`integrableRandomMatrix_rankOneRandomMatrix_of_integrable_products`, and
+`integrableRandomMatrix_rankOneRandomMatrix_of_memLp_two`.  It does not prove
+PSD nullspace converse, expectation contraction, or integrability from
+measurability alone.
 
 Stage MC1 starts the matrix concentration branch after the scalar concentration
 closeout. It adds the assumption vocabulary, explicit matrix order vocabulary,

docs/RandomMatrixAPI.md

@@ -49,7 +49,34 @@ mainline. It is documentation only; theorem status is not upgraded here.
   `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`.
+- Proved vector-to-rank-one matrix measurability/integrability bridge:
+  `rankOneRandomMatrix`, `isRandomMatrix_rankOneRandomMatrix`,
+  `integrableRandomMatrix_rankOneRandomMatrix_of_integrable_products`, and
+  `integrableRandomMatrix_rankOneRandomMatrix_of_memLp_two`.
+- Next safe task: `RM-PSD-nullspace-converse`.
+
+## `HighDimProb/RandomMatrix/Basic.lean`
+
+- `RandomMatrix`: abbrev, finite-dimensional real random matrix.
+- `matrixEntry`: def, entry random variable.
+- `IsRandomMatrix`: abbrev, entrywise measurability predicate.
+- `rankOneRandomMatrix`: def, vector-to-rank-one random matrix with entries
+  `X_i * X_j`.
+- `rankOneRandomMatrix_apply`: theorem.
+- `matrixEntry_rankOneRandomMatrix`: theorem.
+- `isRandomMatrix_rankOneRandomMatrix`: theorem, entrywise measurability from
+  `IsRandomVector`.
+- `measurable_randomMatrix_of_isRandomMatrix`: theorem.
+
+## `HighDimProb/RandomMatrix/Expectation.lean`
+
+- `matrixExpect`: def, entrywise matrix expectation.
+- `IntegrableRandomMatrix`: def, entrywise integrability predicate.
+- `centeredRandomMatrix`: def.
+- `integrableRandomMatrix_rankOneRandomMatrix_of_integrable_products`: theorem,
+  rank-one entrywise integrability from explicit product integrability.
+- `integrableRandomMatrix_rankOneRandomMatrix_of_memLp_two`: theorem, rank-one
+  entrywise integrability from coordinate `MemLp ... 2` assumptions.
 
 ## `HighDimProb/RandomMatrix/SelfAdjoint.lean`
 
@@ -400,7 +427,7 @@ mainline. It is documentation only; theorem status is not upgraded here.
 
 ## Next Safe Task
 
-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.
+RM-PSD-nullspace-converse: next prove or isolate the positive-semidefinite nullspace converse needed by covariance-style examples. Do not prove lambda-max/operator-norm Matrix Bernstein tails, Tropp/Lieb, Bernstein CFC, Golden-Thompson, expectation contraction, or the full Matrix Bernstein theorem in that stage.
 
 ## MB-S9 Matrix Bernstein Trace-MGF Under Primitives API
 
@@ -424,4 +451,4 @@ RM-vector-to-matrix-measurability-integrability: next prove or isolate the entry
   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-vector-to-matrix-measurability-integrability.
+- Next safe task: RM-PSD-nullspace-converse.