Thread conditional trace-MGF into tail route

HighDimProb/RandomMatrix/ConcentrationStatements.lean

@@ -27,7 +27,7 @@ covariance estimation.
 namespace HighDimProb
 
 open MeasureTheory
-open scoped BigOperators Matrix.Norms.L2Operator
+open scoped BigOperators Matrix.Norms.L2Operator MatrixOrder
 
 noncomputable section
 
@@ -5163,6 +5163,134 @@ abbrev matrixBernsteinTraceMGFToLaplaceContract_under_primitives_statement
                 ENNReal.ofReal
                   (traceMatrixExp (SMul.smul (bernsteinMGFCoeff theta R) V))
 
+/-- Progress-first composition from the S9 conditioning trace-MGF bridge to the
+quadratic-form Laplace/tail bound.
+
+This wrapper is intentionally thin.  It first obtains the finite-family
+Bernstein trace-MGF conclusion from
+`traceMGFBernsteinVarianceProxyBound_of_conditioningBridge`, then uses the
+already-proved real-to-`lintegral` bridge and the explicit tail-side
+`quadraticFormUpperTailEvent ⊆ traceExpThresholdEvent` assumption to enter the
+Laplace route.  It does not prove the tail event domination, Tropp/Lieb,
+conditional-expectation, integrability propagation, variance-proxy facts, or a
+full Matrix Bernstein theorem. -/
+theorem matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge
+    {Omega : Type*} [mOmega : MeasurableSpace Omega]
+    {P : Measure Omega} [IsProbabilityMeasure P] {m n : Nat}
+    (X : Fin m -> RandomMatrix Omega n n)
+    (K : Fin m -> Matrix (Fin n) (Fin n) Real)
+    (V : Matrix (Fin n) (Fin n) Real)
+    (theta R t : Real)
+    (mHist : Fin m -> MeasurableSpace Omega)
+    (hChain :
+      @troppConditionalStep_of_iIndepFun_statement Omega mOmega P m n
+        theta X K mHist)
+    (hHist :
+      @troppNaturalHistoryMeasurable_statement Omega mOmega m n
+        theta X K mHist)
+    (hHistIndep :
+      @troppHistoryStepIndependent_of_iIndepFun_statement Omega mOmega P m n
+        theta X K)
+    (hCondExp :
+      forall i,
+        @condExp_traceExp_history_add_independent_step_statement
+          Omega mOmega P n
+          (mHist i) (@troppStateHistory Omega mOmega m n theta X K i)
+          (@troppCurrentRandomStep Omega mOmega m n theta X i) (K i))
+    (hHistSub : forall i, mHist i <= mOmega)
+    (hHistRand :
+      forall i,
+        @IsRandomMatrix Omega mOmega n n P
+          (troppStateHistory theta X K i))
+    (hZRand :
+      forall i,
+        @IsRandomMatrix Omega mOmega n n P
+          (troppCurrentRandomStep theta X i))
+    (hHistSA :
+      forall i omega, IsSelfAdjointMatrix (troppStateHistory theta X K i omega))
+    (hZSA :
+      forall i,
+        @RandomSelfAdjointMatrix Omega mOmega n P
+          (troppCurrentRandomStep theta X i))
+    (hCondTraceInt :
+      forall i,
+        @IntegrableRealRandomVariable Omega mOmega P
+          (fun omega =>
+            traceMatrixExp
+              (troppStateHistory theta X K i omega +
+                troppCurrentRandomStep theta X i omega)))
+    (hExpIntStep :
+      forall i,
+        @IntegrableRandomMatrix Omega mOmega n n P
+          (fun omega => matrixExp (troppCurrentRandomStep theta X i omega)))
+    (hExpMeanSA :
+      forall i,
+        IsSelfAdjointMatrix
+          (@matrixExpect Omega mOmega n n P
+            (fun omega => matrixExp (troppCurrentRandomStep theta X i omega))))
+    (hExpMeanPos :
+      forall i,
+        IsStrictlyPositive
+          (@matrixExpect Omega mOmega n n P
+            (fun omega => matrixExp (troppCurrentRandomStep theta X i omega))))
+    (hSigma : forall i, SigmaFinite (P.trim (hHistSub i)))
+    (hRhsInt :
+      forall i,
+        @IntegrableRealRandomVariable Omega mOmega P
+          (fun omega =>
+            traceMatrixExp (troppStateHistory theta X K i omega + K i)))
+    (hRand : forall i, IsRandomMatrix P (X i))
+    (hSA : forall i, RandomSelfAdjointMatrix P (X i))
+    (hIndep : ProbabilityTheory.iIndepFun X P)
+    (hExpInt :
+      forall i,
+        IntegrableRandomMatrix P
+          (fun omega => matrixExp (SMul.smul theta (X i omega))))
+    (hTraceInt :
+      IntegrableRealRandomVariable P
+        (traceExpIntegrand (randomMatrixSum X) theta))
+    (hKSA : forall i, IsSelfAdjointMatrix (K i))
+    (hVSA : IsSelfAdjointMatrix V)
+    (hR : 0 <= R)
+    (hRange : abs theta * R < 3)
+    (hMGF :
+      forall i,
+        MatrixLE
+          (matrixExpect P
+            (fun omega => matrixExp (SMul.smul theta (X i omega))))
+          (matrixExp (K i)))
+    (hNorm :
+      Finset.univ.sum (fun i : Fin m => K i) =
+        SMul.smul (bernsteinMGFCoeff theta R) V)
+    (hTailMeas :
+      AEMeasurable
+        (fun omega => ENNReal.ofReal
+          (traceExpIntegrand (randomMatrixSum X) theta omega)) P)
+    (hTailSubset :
+      quadraticFormUpperTailEvent (randomMatrixSum X) t ⊆
+        traceExpThresholdEvent (randomMatrixSum X) theta t) :
+    P (quadraticFormUpperTailEvent (randomMatrixSum X) t) <=
+      ENNReal.ofReal (Real.exp (-(theta * t))) *
+        ENNReal.ofReal
+          (traceMatrixExp (SMul.smul (bernsteinMGFCoeff theta R) V)) := by
+  have hTraceMGF :
+      TraceMGFBernsteinVarianceProxyBound P (randomMatrixSum X) V theta R :=
+    traceMGFBernsteinVarianceProxyBound_of_conditioningBridge
+      X K V theta R mHist hChain hHist hHistIndep hCondExp hHistSub
+      hHistRand hZRand hHistSA hZSA hCondTraceInt hExpIntStep hExpMeanSA
+      hExpMeanPos hSigma hRhsInt hRand hSA hIndep hExpInt hTraceInt hKSA
+      hVSA hR hRange hMGF hNorm
+  have hY : RandomSelfAdjointMatrix P (randomMatrixSum X) :=
+    randomSelfAdjointMatrix_sum hSA
+  have hLInt :
+      TraceMGFBernsteinVarianceProxyBoundLIntegral P (randomMatrixSum X)
+        V theta R :=
+    traceMGFBernsteinVarianceProxyBoundLIntegral_of_traceMGFBernsteinVarianceProxyBound
+      (randomMatrixSum X) V theta R hY hTraceInt hTraceMGF
+  exact
+    quadraticFormUpperTail_laplace_bound_of_traceMGFBernsteinVarianceProxyBoundLIntegral
+      (randomMatrixSum X) V theta t R hTailMeas hTailSubset hLInt
+
 /-- Typed target for the spectral-radius reduction for self-adjoint matrices.
 
 This records a future bridge between HighDimProb's deterministic L2 operator

HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean

@@ -13,6 +13,7 @@ open HighDimProb
 #check HighDimProb.matrixBernsteinTraceMGFWithBernsteinCoeff_under_troppPrimitive
 #check HighDimProb.matrixBernsteinTraceMGFToLaplaceContract_statement
 #check HighDimProb.matrixBernsteinTraceMGFToLaplaceContract_under_primitives_statement
+#check HighDimProb.matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge
 #check HighDimProb.matrixBernsteinQuadraticFormUpperTailWithBernsteinCoeff_under_primitives
 #check HighDimProb.traceMatrixExp_bernsteinMGFCoeff_matrixVarianceProxy_le_card_exp
 #check HighDimProb.matrixBernsteinQuadraticFormUpperTailScalarRHSWithBernsteinCoeff_under_primitives

HighDimProbTest/RandomMatrixConcentrationAPI.lean

@@ -118,6 +118,7 @@ variable (R theta sigma2 c c1 c2 t bound K : Real)
 #check traceMGFBernsteinVarianceProxyBound_negRandomMatrixFamily
 #check matrixBernsteinTraceMGFWithBernsteinCoeff_negRandomMatrixFamily
 #check matrixBernsteinTraceMGFWithBernsteinCoeff_under_primitives
+#check HighDimProb.matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge
 #check matrixBernsteinTraceMGFWithBernsteinCoeff_under_troppPrimitive
 #check matrixBernsteinTraceMGFToLaplaceContract_statement
 #check matrixBernsteinTraceMGFToLaplaceContract_under_primitives_statement

docs/RandomMatrixAPI.md

@@ -66,6 +66,7 @@ only consumes an explicitly supplied log-back equality.
 - `matrixBernsteinTraceMGFWithBernsteinCoeff_under_primitives`
 - `matrixBernsteinTraceMGFWithBernsteinCoeff_under_troppPrimitive`
 - `matrixBernsteinQuadraticFormUpperTailOptimizedScalarRHSWithBernsteinCoeff_under_primitives`
+- `matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge`
 - `matrixBernsteinQuadraticFormUpperTailOptimizedScalarRHSWithBernsteinCoeff_of_assumptions`
 - `matrixBernsteinQuadraticFormUpperTailOptimizedScalarRHSWithBernsteinCoeff_of_troppAssumptions`
 - `matrixBernsteinTwoSidedQuadraticFormTailOptimizedScalarRHSWithBernsteinCoeff_under_primitives`
@@ -83,8 +84,11 @@ public surface is the `*_of_troppAssumptions` family, which uses
 bookkeeping assumptions without a user-supplied CFC field. The older
 `*_of_assumptions` and `_under_primitives` names remain compatibility surfaces.
 The route still does not prove Tropp/Lieb, Golden-Thompson, trace-exp
-integrability, variance-proxy control, or a full unconditional Matrix
-Bernstein theorem.
+integrability, variance-proxy control, tail event domination, or a full unconditional Matrix
+Bernstein theorem. The conditioning-to-tail wrapper
+`matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge` is a thin
+composition from the S9 conditioning trace-MGF consumer to the existing
+quadratic-form Laplace route under an explicit tail-event subset assumption.
 
 ## Hardbone Statement Targets
 

docs/STATEMENTS.md

@@ -80,3 +80,31 @@ Non-goals for this consumer:
   trace-exponential integrability propagation, strict positivity of the
   matrix-exponential mean, variance-proxy control, Lieb/Jensen,
   Golden-Thompson, or full Matrix Bernstein.
+
+## RM-LIEB-S10: conditioning trace-MGF to explicit Laplace/tail route
+
+Consumer theorem:
+
+- `matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge`
+
+This theorem composes the S9 conditioning trace-MGF consumer with the existing
+quadratic-form Laplace route. It requires all S9 assumptions listed above, plus
+the following tail-side facts as explicit premises:
+
+- AEMeasurability of `fun omega => ENNReal.ofReal
+  (traceExpIntegrand (randomMatrixSum X) theta omega)`.
+- The event bridge `quadraticFormUpperTailEvent (randomMatrixSum X) t ⊆
+  traceExpThresholdEvent (randomMatrixSum X) theta t`.
+
+The real trace-MGF to `TraceMGFBernsteinVarianceProxyBoundLIntegral` conversion
+is provided by the existing proved bridge, using the explicit full-sum
+trace-exponential integrability and self-adjoint summand assumptions already
+required by S9.
+
+Non-goals for this consumer:
+
+- It does not prove the tail event domination, natural-history measurability,
+  independence conditioning, conditional-expectation reduction, trace-exp
+  integrability propagation, strict positivity of matrix-exponential means,
+  variance-proxy control, Lieb/Jensen, Golden-Thompson, theta optimization,
+  dimension/rank reduction, or full Matrix Bernstein.

docs/Status.md

@@ -58,6 +58,7 @@ Core Matrix Bernstein helpers:
 - `matrixBernsteinTraceMGFWithBernsteinCoeff_under_troppPrimitive`
 - `matrixBernsteinQuadraticFormUpperTailOptimizedScalarRHSWithBernsteinCoeff_of_assumptions`
 - `matrixBernsteinQuadraticFormUpperTailOptimizedScalarRHSWithBernsteinCoeff_of_troppAssumptions`
+- `matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge`
 - `matrixBernsteinTwoSidedQuadraticFormTailOptimizedScalarRHSWithBernsteinCoeff_of_assumptions`
 - `matrixBernsteinTwoSidedQuadraticFormTailOptimizedScalarRHSWithBernsteinCoeff_of_troppAssumptions`
 - `matrixBernsteinSelfAdjointOperatorNormTailOptimizedScalarRHSWithBernsteinCoeff_arbitrary_of_assumptions`
@@ -245,7 +246,10 @@ Low-level prefix/state, reindex, negative-family, nullspace/decomposition, exact
   conditioning chain now has the thin theorem witness
   `troppConditionalStep_of_iIndepFun`, which only forwards the explicit
   per-index conditional-expectation provider and does not prove history
-  measurability or independence. The preferred optimized Matrix Bernstein
+  measurability or independence. The S10 wrapper
+  `matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge` threads
+  the S9 trace-MGF consumer into the quadratic-form Laplace/tail route under an
+  explicit tail-event subset assumption. The preferred optimized Matrix Bernstein
   assumption bundles are now `MatrixBernsteinPositiveSideTroppAssumptions` and
   `MatrixBernsteinNegativeSideTroppAssumptions`, which expose Tropp/Lieb
   primitives but not pointwise CFC fields. The older explicit-CFC bundles and
@@ -366,8 +370,12 @@ Low-level prefix/state, reindex, negative-family, nullspace/decomposition, exact
   `RM-LIEB-S8-tropp-master-trace-mgf-assumption-composition-contract`, adding `troppMasterTraceMGFStep_trace_bound_of_liebJensen_logOrder` as a high-level consumer from explicit Lieb/Jensen and log/order assumptions to the one-step trace-MGF `K` bound. The hard assumptions consumed by the theorem are recorded in `docs/STATEMENTS.md`; this does not prove those assumptions.
 - Progress-first hardbone contract leaf:
   `RM-LIEB-S9-conditional-step-assumption-composition-contract`, adding `traceMGFBernsteinVarianceProxyBound_of_conditioningBridge` as a finite-family trace-MGF consumer from explicit conditioning, natural-state, integrability, and variance-proxy assumptions. The hard assumptions consumed by the theorem are recorded in `docs/STATEMENTS.md`; this does not prove those assumptions.
-- Next aggressive hardbone task:
-  `RM-LIEB-S10-trace-mgf-to-tail-assumption-composition-contract`, focused on threading the new conditional trace-MGF consumer into the downstream tail route under explicit tail-side assumptions.
+- Progress-first hardbone contract leaf:
+  `RM-LIEB-S10-trace-mgf-to-tail-assumption-composition-contract`, adding
+  `matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge` as a
+  trace-MGF-to-tail consumer under explicit tail-side assumptions. The hard
+  assumptions consumed by the theorem are recorded in `docs/STATEMENTS.md`;
+  this does not prove those assumptions or a full Matrix Bernstein theorem.
 
 ## Verification
 

docs/TODO.md

@@ -25,8 +25,8 @@ This is the active short list. Old completed task logs were collapsed into
   transfer, and PSD Loewner norm monotonicity are bridge-layer infrastructure for
   future provider compression; the compact bounded-row sample-covariance route
   remains the reader-facing surface.
-- Next RandomMatrix hardbone task:
-  `RM-LIEB-S10-trace-mgf-to-tail-assumption-composition-contract`.
+- Next RandomMatrix hardbone task: select the next provider-compression or
+  public-friendly Matrix Bernstein natural-state wrapper after S10.
 - Current strategy is progress-first: if a hard analytic ingredient is missing,
   consume it as an explicit assumption, register it in `docs/STATEMENTS.md`, and
   keep moving the high-level Tropp/Lieb trace-MGF route forward. Do not claim

docs/TestPlan.md

@@ -43,8 +43,10 @@ git diff --check
   progress-first Tropp/Lieb one-step assumption-composition consumer and the
   conditional finite-family trace-MGF assumption-composition consumer are covered in
   `HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean`,
-  `HighDimProbTest/RandomMatrixCStarBridgeAPI.lean`, and
-  `HighDimProbJudge/RandomMatrix/TraceExpUse.lean`.
+  `HighDimProbTest/RandomMatrixConcentrationAPI.lean`,
+  `HighDimProbTest/RandomMatrixCStarBridgeAPI.lean`,
+  `HighDimProbJudge/RandomMatrix/TraceExpUse.lean`, and
+  `HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean`.
 - RandomMatrix sample-covariance negative-side provider-transfer adapters, the
   compact `SampleCovarianceTailTarget` /
   `SampleCovarianceBoundedRowTroppAssumptions` route, bridge-layer exact-row

docs/TheoremAtlas.md

@@ -133,7 +133,11 @@ or conditional-expectation inputs themselves. The conditional route is now also
 composed into the finite-family Bernstein trace-MGF conclusion by
 `traceMGFBernsteinVarianceProxyBound_of_conditioningBridge`, under explicit
 natural-state, integrability, MGF, and variance-proxy assumptions recorded in
-`docs/STATEMENTS.md`.
+`docs/STATEMENTS.md`. The S10 wrapper
+`matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge` threads
+that trace-MGF conclusion into the quadratic-form Laplace/tail route under an
+explicit trace-exp threshold event subset assumption; it is not a full Matrix
+Bernstein theorem.
 
 ## Not Yet Proved