Compose conditional trace-MGF assumptions

HighDimProb/RandomMatrix/HardboneStatements.lean

@@ -1552,6 +1552,115 @@ theorem troppMasterTraceMGFConditionalStep_of_conditioningBridge
       (@troppCurrentRandomStep Omega mOmega m n theta X i) (K i) :=
   hChain hHist hHistIndep hCondExp hIndep i
 
+/-- Progress-first finite-family trace-MGF provider from explicit conditioning
+bridge assumptions.
+
+This theorem composes the Phase 4 conditioning bridge with the natural-state
+finite-family trace-MGF route. It deliberately consumes all hard probabilistic,
+conditional-expectation, integrability, and variance-proxy assumptions
+explicitly; those assumptions are tracked in `docs/STATEMENTS.md`. -/
+theorem traceMGFBernsteinVarianceProxyBound_of_conditioningBridge
+    {Omega : Type*} [mOmega : MeasurableSpace Omega]
+    {P : MeasureTheory.Measure Omega} [MeasureTheory.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 : 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, MeasureTheory.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) :
+    TraceMGFBernsteinVarianceProxyBound P (randomMatrixSum X) V theta R :=
+  traceMGFBernsteinVarianceProxyBound_of_naturalStateConditionalSteps
+    X K V theta R mHist
+    (fun i =>
+      troppMasterTraceMGFConditionalStep_of_conditioningBridge
+        theta X K mHist hChain hHist hHistIndep hCondExp hIndep i)
+    hHistSub hHistRand hZRand
+    (hHist hHistSub)
+    hHistSA hZSA
+    (hHistIndep hIndep)
+    hCondTraceInt hExpIntStep hExpMeanSA hExpMeanPos hSigma hRhsInt
+    hRand hSA hIndep hExpInt hTraceInt hKSA hVSA hR hRange hMGF hNorm
+
 end
 
 end HighDimProb

HighDimProbJudge/RandomMatrix/TraceExpUse.lean

@@ -146,6 +146,7 @@ example {n : Nat} (A : Matrix (Fin n) (Fin n) Real)
 #check HighDimProb.condExp_traceExp_history_add_independent_step_statement
 #check HighDimProb.troppConditionalStep_of_iIndepFun_statement
 #check HighDimProb.troppConditionalStep_of_iIndepFun
+#check HighDimProb.traceMGFBernsteinVarianceProxyBound_of_conditioningBridge
 #check HighDimProb.matrixExpScaledIntegrable_of_provider_statement
 #check HighDimProb.traceExpIntegrable_troppStateHistory_add_step_statement
 #check HighDimProb.traceExpIntegrable_troppStateHistory_add_K_statement

HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean

@@ -91,6 +91,7 @@ variable (mHist : Fin m -> MeasurableSpace Omega)
 #check troppMasterTraceMGFStep_of_liebJensen
 #check troppMasterTraceMGFStep_trace_bound_of_liebJensen_logOrder
 #check troppMasterTraceMGFConditionalStep_of_conditioningBridge
+#check traceMGFBernsteinVarianceProxyBound_of_conditioningBridge
 #check traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider
 #check varianceProxyNormBound_of_centeredSquareChain
 #check varianceProxyNormBound_of_centeredSquareChain_expansion
@@ -193,6 +194,72 @@ example :
     troppConditionalStep_of_iIndepFun_statement (P := P) theta X Kfam mHist :=
   troppConditionalStep_of_iIndepFun theta X Kfam mHist
 
+example
+    (hChain : troppConditionalStep_of_iIndepFun_statement (P := P) theta X Kfam mHist)
+    (hHist : troppNaturalHistoryMeasurable_statement theta X Kfam mHist)
+    (hHistIndep : troppHistoryStepIndependent_of_iIndepFun_statement (P := P) theta X Kfam)
+    (hCondExp : forall i,
+      @condExp_traceExp_history_add_independent_step_statement
+        Omega (inferInstance : MeasurableSpace Omega) P n
+        (mHist i)
+        (@troppStateHistory Omega (inferInstance : MeasurableSpace Omega) m n theta X Kfam i)
+        (@troppCurrentRandomStep Omega (inferInstance : MeasurableSpace Omega) m n theta X i)
+        (Kfam i))
+    (hHistSub : forall i, mHist i <= (inferInstance : MeasurableSpace Omega))
+    (hHistRand : forall i,
+      @IsRandomMatrix Omega (inferInstance : MeasurableSpace Omega) n n P
+        (troppStateHistory theta X Kfam i))
+    (hZRand : forall i,
+      @IsRandomMatrix Omega (inferInstance : MeasurableSpace Omega) n n P
+        (troppCurrentRandomStep theta X i))
+    (hHistSA : forall i omega, IsSelfAdjointMatrix (troppStateHistory theta X Kfam i omega))
+    (hZSA : forall i,
+      @RandomSelfAdjointMatrix Omega (inferInstance : MeasurableSpace Omega) n P
+        (troppCurrentRandomStep theta X i))
+    (hCondTraceInt : forall i,
+      @IntegrableRealRandomVariable Omega (inferInstance : MeasurableSpace Omega) P
+        (fun omega => traceMatrixExp
+          (troppStateHistory theta X Kfam i omega +
+            troppCurrentRandomStep theta X i omega)))
+    (hExpIntStep : forall i,
+      @IntegrableRandomMatrix Omega (inferInstance : MeasurableSpace Omega) n n P
+        (fun omega => matrixExp (troppCurrentRandomStep theta X i omega)))
+    (hExpMeanSA : forall i,
+      IsSelfAdjointMatrix
+        (@matrixExpect Omega (inferInstance : MeasurableSpace Omega) n n P
+          (fun omega => matrixExp (troppCurrentRandomStep theta X i omega))))
+    (hExpMeanPos : forall i,
+      IsStrictlyPositive
+        (@matrixExpect Omega (inferInstance : MeasurableSpace Omega) n n P
+          (fun omega => matrixExp (troppCurrentRandomStep theta X i omega))))
+    (hSigma : forall i, MeasureTheory.SigmaFinite (P.trim (hHistSub i)))
+    (hRhsInt : forall i,
+      @IntegrableRealRandomVariable Omega (inferInstance : MeasurableSpace Omega) P
+        (fun omega => traceMatrixExp (troppStateHistory theta X Kfam i omega + Kfam 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 (Kfam i))
+    (hVSA : IsSelfAdjointMatrix M)
+    (hR : 0 <= R)
+    (hRange : abs theta * R < 3)
+    (hMGF : forall i,
+      MatrixLE
+        (matrixExpect P (fun omega => matrixExp (SMul.smul theta (X i omega))))
+        (matrixExp (Kfam i)))
+    (hNorm : Finset.univ.sum (fun i : Fin m => Kfam i) =
+      SMul.smul (bernsteinMGFCoeff theta R) M) :
+    TraceMGFBernsteinVarianceProxyBound P (randomMatrixSum X) M theta R :=
+  traceMGFBernsteinVarianceProxyBound_of_conditioningBridge
+    X Kfam M 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
+
 example : Prop :=
   traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider_statement
     (P := P) theta X D

docs/RandomMatrixAPI.md

@@ -183,6 +183,7 @@ Thin hardbone consumers:
 - `troppMasterTraceMGFStep_of_liebJensen`
 - `troppConditionalStep_of_iIndepFun`
 - `troppMasterTraceMGFConditionalStep_of_conditioningBridge`
+- `traceMGFBernsteinVarianceProxyBound_of_conditioningBridge`
 - `traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider`
 - `varianceProxyNormBound_of_centeredSquareChain`
 - `varianceProxyNormBound_of_centeredSquareChain_of_normMono`
@@ -204,11 +205,11 @@ Hardbone status table:
 | Real-to-CStar bridge | `realMatrixToCStarMatrix` and transport statement targets | representation map, add/sub, self-adjoint transport, and CStar-side positivity/order/strict-positivity transport from explicit complexified premises proved | exposes the CStar representation route for future operator-log monotonicity proofs | real-to-complex positivity/order premises and unconditional log-back transport remain open |
 | Log/order-to-`K` | `troppLogExpComparisonToK_of_logOrderKChain_statement` | typed-prop | `troppLogExpComparisonToK_of_logMonotone_traceExpMono` | trace-exp monotonicity plus the explicit log/order bridge inputs |
 | Tropp/Lieb/GT one-step | `troppMasterTraceMGFStep_of_liebJensen_statement` | typed-prop plus progress-first composition consumer | `troppMasterTraceMGFStep_of_liebJensen`; `troppMasterTraceMGFStep_trace_bound_of_liebJensen_logOrder` composes the one-step primitive with the log/order-to-`K` bridge | Lieb concavity, probability-measure Jensen, log-exp normalization, operator-log/log-domain input, trace-exp monotonicity; Golden-Thompson is separate |
-| Conditioning / independence | `troppConditionalStep_of_iIndepFun_statement` | proven by `troppConditionalStep_of_iIndepFun` | `troppMasterTraceMGFConditionalStep_of_conditioningBridge` | thin forwarder only; generated histories, history/current-step independence, finite-family independence, and conditional expectation reduction remain explicit premises |
+| Conditioning / independence | `troppConditionalStep_of_iIndepFun_statement` | proven by `troppConditionalStep_of_iIndepFun` | `troppMasterTraceMGFConditionalStep_of_conditioningBridge`; `traceMGFBernsteinVarianceProxyBound_of_conditioningBridge` composes this route into the finite-family trace-MGF bound | thin forwarder/composer only; generated histories, history/current-step independence, finite-family independence, conditional expectation reduction, integrability, and variance-proxy inputs remain explicit premises |
 | Trace-exp integrability | `traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider_statement` | typed-prop with proved thin consumer | `traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider` | automatic absolute domination, Golden-Thompson/product, or boundedness provider |
 | Variance proxy / centered square | `varianceProxyNormBound_of_centeredSquareChain_statement`, `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement`, `matrixSquare_centeredRandomMatrix_expectation_expansion_statement`, `centeredRankOneSquare_le_rankOneSecondMoment_statement` | centered-square expectation expansion, finite-sum MatrixLE bookkeeping, PSD Loewner-to-operator-norm monotonicity, and centered rank-one second-moment comparison proved; typed-prop chain has proved thin consumers | `matrixSquare_centeredRandomMatrix_expectation_expansion`, `matrixSecondMoment_centeredRandomMatrix_le_matrixSecondMoment`, `centeredRankOneSquare_le_rankOneSecondMoment`, `varianceProxyNormBound_of_centeredSquareChain`, `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE`, `varianceProxyNormBound_of_centeredSquareChain_of_normMono`, `varianceProxyNormBound_of_centeredSquareChain_expansion`, `sampleCovarianceVarianceProxy_sharp_of_rankOneSecondMoment`, `sampleCovarianceVarianceProxy_sharp_of_exactRowSecondMoment`, `deterministicMatrixVarianceProxyNorm_sum_le_sum`, `deterministicMatrixVarianceProxyNorm_matrixSecondMoment_rankOneRandomMatrix_le_sq_of_sqNorm_bound`, `deterministicMatrixVarianceProxyNorm_sum_matrixSecondMoment_rankOneRandomMatrix_le_sum_sq_of_sqNorm_bound`, `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two`, `sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two`, `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two_of_centeredSquareChain`, `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two`, exact-row centered-square sample-covariance wrappers and bundles, `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_integrable_four_products`, `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_memLp_four`, `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_sqNorm_bound_memLp_two`, `integrableRandomMatrix_randomMatrixSquare_centeredRankOneRandomMatrixFamily_of_memLp_four`, `integrableRandomMatrix_randomMatrixSquare_centeredRankOneRandomMatrixFamily_of_sqNorm_bound_memLp_two`, `MatrixVarianceProxyNormBound_centeredRankOneRandomMatrixFamily_of_sqNorm_bound_memLp_two` | full generic centered-square-chain providers, Tropp/Lieb, trace-MGF integrability, and full Matrix Bernstein remain explicit or open |
 | Dimension / support / effective rank | `traceMatrixExp_le_rank_exp_lambdaMax_statement`, `traceMatrixExp_le_supportDim_exp_lambdaMax_statement`, `traceMatrixExp_effectiveRank_bound_statement`, `matrixExpSupportDomination_identity_statement`, `traceMatrixExp_excess_supportDim_exp_lambdaMax_statement` | rank/support targets and effective-rank consumer proved under explicit support, PSD, lambda-max, and trace-certificate assumptions; ambient trace certificate and star-projection rank/PSD consumer proved; identity support provider target named only; excess trace bridge and supportDim consumer proved under explicit excess certificate | `traceMatrixExp_le_rank_exp_lambdaMax`, `traceMatrixExp_le_rank_exp_lambdaMax_of_isStarProjection`, `traceMatrixExp_le_supportDim_exp_lambdaMax`, `traceMatrixExp_excess_supportDim_exp_lambdaMax`, `traceMatrixExp_effectiveRank_bound`, `traceMatrixExp_effectiveRank_bound_of_ambientTraceCertificate`; deterministic helpers include `MatrixExpSupportDomination`, `MatrixExpExcessSupportDomination`, `traceMatrixExp_le_card_add_trace_support_mul_exp_sub_one_of_excessSupportDomination`, `traceMatrixExp_eq_sum_exp_eigenvalues`, `traceMatrixExp_smul_le_card_add_trace_div_mul_exp_sub_one_of_psd_lambdaMax_le`, `matrixTrace_le_card_mul_of_isPSD_lambdaMaxOrdered_le`, `matrixTrace_eq_rank_of_isStarProjection`, `isPSDMatrix_of_isStarProjection` | identity/excess support-domination providers and support-construction certificates; true effective-rank trace certificate provider beyond ambient dimension |
-| Thin consumers | `troppMasterTraceMGFConditionalStep_of_conditioningBridge` | proven | public API/test/judge/example checks | thin wrapper only; no hard fact is discharged |
+| Thin consumers | `troppMasterTraceMGFConditionalStep_of_conditioningBridge`, `traceMGFBernsteinVarianceProxyBound_of_conditioningBridge` | proven | public API/test/judge/example checks | thin wrappers only; no hard fact is discharged |
 
 Most hardbone declarations are typed `Prop` contracts, not hard theorem proofs.
 The Bernstein CFC chain is now proved by `bernsteinMatrixExp_le_quadratic`

docs/STATEMENTS.md

@@ -40,3 +40,43 @@ Non-goals for this consumer:
 - It does not prove Lieb concavity, Jensen, operator-log monotonicity,
   trace-exp monotonicity, Golden-Thompson, conditional expectation,
   integrability propagation, variance-proxy control, or full Matrix Bernstein.
+
+## RM-LIEB-S9: finite-family trace-MGF from explicit conditioning inputs
+
+Consumer theorem:
+
+- `traceMGFBernsteinVarianceProxyBound_of_conditioningBridge`
+
+This theorem composes the Phase 4 conditioning bridge with the natural-state
+finite-family trace-MGF route.  It requires the following hard facts as explicit
+premises:
+
+- `troppConditionalStep_of_iIndepFun_statement theta X K mHist`, the
+  source-level conditioning chain target.
+- `troppNaturalHistoryMeasurable_statement theta X K mHist`, used with
+  `hHistSub` to supply natural-state history measurability.
+- `troppHistoryStepIndependent_of_iIndepFun_statement theta X K`, used with
+  finite-family `iIndepFun X P` to supply history/current-step independence.
+- Per-index `condExp_traceExp_history_add_independent_step_statement`, the
+  conditional-expectation reduction from a history-measurable matrix and an
+  independent current step.
+- Natural-state side conditions for each index: history sub-sigma algebra,
+  history/current random-matrix measurability, self-adjoint history/current
+  steps, trace-exponential integrability of `H_i + Z_i`, matrix-exponential
+  integrability of `Z_i`, self-adjointness and strict positivity of the
+  matrix-exponential mean, sigma-finiteness of the trimmed history measure, and
+  trace-exponential integrability of `H_i + K_i`.
+- Finite-family Bernstein side conditions: random/self-adjoint summands,
+  finite-family independence, scaled matrix-exponential integrability,
+  full-sum trace-exponential integrability, self-adjoint comparison matrices,
+  self-adjoint variance proxy, nonnegative radius, Bernstein theta range,
+  per-index MGF Loewner comparison, and the variance-proxy normalization
+  `sum K_i = bernsteinMGFCoeff theta R • V`.
+
+Non-goals for this consumer:
+
+- It does not prove natural-history measurability, history/current-step
+  independence, finite-family independence, conditional-expectation reduction,
+  trace-exponential integrability propagation, strict positivity of the
+  matrix-exponential mean, variance-proxy control, Lieb/Jensen,
+  Golden-Thompson, or full Matrix Bernstein.