diff --git a/HighDimProb/Examples/RandomMatrix/HardboneStatementAtlasUsage.lean b/HighDimProb/Examples/RandomMatrix/HardboneStatementAtlasUsage.lean index 1e037cc..bd2c507 100644 --- a/HighDimProb/Examples/RandomMatrix/HardboneStatementAtlasUsage.lean +++ b/HighDimProb/Examples/RandomMatrix/HardboneStatementAtlasUsage.lean @@ -38,6 +38,7 @@ open scoped MatrixOrder Matrix.Norms.Operator #check bernsteinMatrixExp_le_quadratic #check troppLogExpComparisonToK_of_logMonotone_traceExpMono #check troppMasterTraceMGFStep_of_liebJensen +#check troppConditionalStep_of_iIndepFun #check troppMasterTraceMGFConditionalStep_of_conditioningBridge example (theta R : Real) : Prop := @@ -64,6 +65,15 @@ example {Omega : Type*} [MeasurableSpace Omega] (mHist : Fin m -> MeasurableSpace Omega) : Prop := troppConditionalStep_of_iIndepFun_statement (P := P) theta X K mHist +example {Omega : Type*} [MeasurableSpace Omega] + (P : Measure Omega) {m n : Nat} + (theta : Real) + (X : Fin m -> RandomMatrix Omega n n) + (K : Fin m -> Matrix (Fin n) (Fin n) Real) + (mHist : Fin m -> MeasurableSpace Omega) : + troppConditionalStep_of_iIndepFun_statement (P := P) theta X K mHist := + troppConditionalStep_of_iIndepFun theta X K mHist + example {Omega : Type*} [MeasurableSpace Omega] (P : Measure Omega) {m n : Nat} (theta R : Real) diff --git a/HighDimProb/RandomMatrix/HardboneStatements.lean b/HighDimProb/RandomMatrix/HardboneStatements.lean index ab29cf2..3696864 100644 --- a/HighDimProb/RandomMatrix/HardboneStatements.lean +++ b/HighDimProb/RandomMatrix/HardboneStatements.lean @@ -850,6 +850,24 @@ theorem troppMasterTraceMGFStep_of_liebJensen {Omega : Type*} troppMasterTraceMGFStep_statement (P := P) H Z := hChain hJensen hNormalize +/-- Thin witness for the finite-family conditioning hardbone chain. + +This theorem does not prove natural history measurability, history/current-step +independence, finite-family independence, or the conditional-expectation +reduction. It only forwards the explicit per-index conditional-expectation +provider through the statement target. -/ +theorem troppConditionalStep_of_iIndepFun + {Omega : Type*} [mOmega : MeasurableSpace Omega] + {P : MeasureTheory.Measure Omega} {m n : Nat} + (theta : Real) + (X : Fin m -> RandomMatrix Omega n n) + (K : Fin m -> Matrix (Fin n) (Fin n) Real) + (mHist : Fin m -> MeasurableSpace Omega) : + @troppConditionalStep_of_iIndepFun_statement Omega mOmega P m n + theta X K mHist := by + intro _hHist _hHistIndep hCondExp _hIndep i + exact hCondExp i + /-- Thin consumer for the Phase 4 conditioning bridge. The conclusion is one indexed conditional-step target. The proof only applies diff --git a/HighDimProbJudge/RandomMatrix/TraceExpUse.lean b/HighDimProbJudge/RandomMatrix/TraceExpUse.lean index dd0bb70..0cd7d7f 100644 --- a/HighDimProbJudge/RandomMatrix/TraceExpUse.lean +++ b/HighDimProbJudge/RandomMatrix/TraceExpUse.lean @@ -104,6 +104,7 @@ open scoped MatrixOrder Matrix.Norms.Operator #check HighDimProb.troppHistoryStepIndependent_of_iIndepFun_statement #check HighDimProb.condExp_traceExp_history_add_independent_step_statement #check HighDimProb.troppConditionalStep_of_iIndepFun_statement +#check HighDimProb.troppConditionalStep_of_iIndepFun #check HighDimProb.matrixExpScaledIntegrable_of_provider_statement #check HighDimProb.traceExpIntegrable_troppStateHistory_add_step_statement #check HighDimProb.traceExpIntegrable_troppStateHistory_add_K_statement diff --git a/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean b/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean index 95686d5..36728b1 100644 --- a/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean +++ b/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean @@ -37,6 +37,7 @@ variable (mHist : Fin m -> MeasurableSpace Omega) #check troppHistoryStepIndependent_of_iIndepFun_statement #check condExp_traceExp_history_add_independent_step_statement #check troppConditionalStep_of_iIndepFun_statement +#check @troppConditionalStep_of_iIndepFun #check matrixExpScaledIntegrable_of_provider_statement #check traceExpIntegrable_troppStateHistory_add_step_statement #check traceExpIntegrable_troppStateHistory_add_K_statement @@ -75,6 +76,10 @@ example : Prop := example : Prop := troppConditionalStep_of_iIndepFun_statement (P := P) theta X Kfam mHist +example : + troppConditionalStep_of_iIndepFun_statement (P := P) theta X Kfam mHist := + troppConditionalStep_of_iIndepFun theta X Kfam mHist + example : Prop := traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider_statement (P := P) theta X D diff --git a/docs/RandomMatrixAPI.md b/docs/RandomMatrixAPI.md index f0bcfd9..82ed408 100644 --- a/docs/RandomMatrixAPI.md +++ b/docs/RandomMatrixAPI.md @@ -90,6 +90,7 @@ Conditioning / independence chain: - `troppHistoryStepIndependent_of_iIndepFun_statement` - `condExp_traceExp_history_add_independent_step_statement` - `troppConditionalStep_of_iIndepFun_statement` +- `troppConditionalStep_of_iIndepFun` Integrability provider chain: @@ -118,6 +119,7 @@ Thin hardbone consumers: - `bernsteinMatrixExp_le_quadratic` - `troppLogExpComparisonToK_of_logMonotone_traceExpMono` - `troppMasterTraceMGFStep_of_liebJensen` +- `troppConditionalStep_of_iIndepFun` - `troppMasterTraceMGFConditionalStep_of_conditioningBridge` Hardbone status table: @@ -128,7 +130,7 @@ Hardbone status table: | Bernstein CFC | `bernsteinMatrixExp_le_quadratic_statement` | proven by `bernsteinMatrixExp_le_quadratic` | `bernsteinMatrixExp_le_quadratic_of_cfcLeaves` documents the reusable composition | preferred `*_of_troppAssumptions` wrappers bypass pointwise CFC fields; explicit-CFC wrappers remain for compatibility | | Log/order-to-`K` | `troppLogExpComparisonToK_of_logOrderKChain_statement` | typed-prop | `troppLogExpComparisonToK_of_logMonotone_traceExpMono` | operator-log monotonicity, log domain for `matrixExp`, trace-exp monotonicity | | Tropp/Lieb/GT one-step | `troppMasterTraceMGFStep_of_liebJensen_statement` | typed-prop | `troppMasterTraceMGFStep_of_liebJensen` | Lieb concavity, probability-measure Jensen, log-exp normalization; Golden-Thompson is separate | -| Conditioning / independence | `troppConditionalStep_of_iIndepFun_statement` | typed-prop | `troppMasterTraceMGFConditionalStep_of_conditioningBridge` | generated histories, history-step independence, conditional expectation reduction | +| 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 | | Trace-exp integrability | `traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider_statement` | typed-prop | none yet | absolute domination, Golden-Thompson/product, or boundedness provider | | Variance proxy / centered square | `varianceProxyNormBound_of_centeredSquareChain_statement` | typed-prop | none yet | centered-square expansion, rank-one comparison, order/norm bookkeeping | | Dimension / support / effective rank | `traceMatrixExp_effectiveRank_bound_statement` | typed-prop | none yet | rank/support/effective-rank core theory | @@ -137,13 +139,16 @@ Hardbone status table: Most hardbone declarations are typed `Prop` contracts, not hard theorem proofs. The Bernstein CFC chain is now proved by `bernsteinMatrixExp_le_quadratic` after splitting out scalar Bernstein, spectrum localization, CFC order -transfer, and expression normalization. The remaining log/order, Tropp/Lieb, -conditioning, integrability, variance-proxy, and dimension/rank blockers stay -split into named leaves. The rank and effective-rank trace-exp +transfer, and expression normalization. The finite-family conditioning chain is +proved by `troppConditionalStep_of_iIndepFun`, but it only forwards the explicit +per-index conditional-expectation provider and does not discharge the history or +independence hypotheses. The remaining log/order, Tropp/Lieb, integrability, +variance-proxy, and dimension/rank blockers stay split into named leaves. The +rank and effective-rank trace-exp targets keep support or ambient-identity terms explicit, so zero directions are not accidentally treated as free. The thin consumers only apply explicit -statement-chain assumptions; they do not prove Lieb/Jensen, conditioning, -finite-family Tropp, or any Matrix Bernstein tail theorem. +statement-chain assumptions; they do not prove Lieb/Jensen, conditional +expectation reduction, finite-family Tropp, or any Matrix Bernstein tail theorem. ## TraceExp / Tropp Bookkeeping Surface diff --git a/docs/Status.md b/docs/Status.md index ab5c807..074793c 100644 --- a/docs/Status.md +++ b/docs/Status.md @@ -86,6 +86,10 @@ Hardbone Bernstein CFC leaf: - `bernsteinMatrixExp_le_quadratic_of_cfcLeaves` - `bernsteinMatrixExp_le_quadratic` +Hardbone conditioning bridge leaf: + +- `troppConditionalStep_of_iIndepFun` + Example-layer wrappers: - `sampleCovariance_quadraticForm_tail_usage` @@ -114,7 +118,11 @@ Example modules: typed statement targets. The Bernstein CFC route is now proved through `bernsteinMatrixExp_le_quadratic`, reusing scalar Bernstein, spectrum localization, Bernstein-specific CFC order transfer, and CFC expression - normalization. The preferred optimized Matrix Bernstein assumption bundles + normalization. The 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 + assumption bundles are now `MatrixBernsteinPositiveSideTroppAssumptions` and `MatrixBernsteinNegativeSideTroppAssumptions`, which expose Tropp/Lieb primitives but not pointwise CFC fields. The older explicit-CFC bundles and @@ -134,6 +142,8 @@ Example modules: assumptions onto the named negative sample-covariance family; they do not prove exponential integrability, trace-exponential integrability, or CFC. - Completed hardbone wrapper task: `RM-HB-sample-covariance-cfc-free-wrapper-contract`. +- Completed hardbone proof leaf: + `RM-HB12-tropp-conditional-step-of-iindepfun-bridge-leaf`. - Next safe hardbone task: `RM-HB12-select-next-hardbone-proof-leaf`. ## Verification diff --git a/docs/TODO.md b/docs/TODO.md index 7f04f70..807d52e 100644 --- a/docs/TODO.md +++ b/docs/TODO.md @@ -12,6 +12,8 @@ This is the active short list. Old completed task logs were collapsed into - Keep public examples readable: name families and adapters first, then call the shared RandomMatrix API. - Completed RandomMatrix hardbone wrapper task: `RM-HB-sample-covariance-cfc-free-wrapper-contract`. +- Completed RandomMatrix hardbone proof leaf: + `RM-HB12-tropp-conditional-step-of-iindepfun-bridge-leaf`. - Next RandomMatrix hardbone task: `RM-HB12-select-next-hardbone-proof-leaf`. diff --git a/docs/TheoremAtlas.md b/docs/TheoremAtlas.md index 5f1dc87..7c14dec 100644 --- a/docs/TheoremAtlas.md +++ b/docs/TheoremAtlas.md @@ -50,16 +50,21 @@ fields in generic call sites. The sample-covariance route now also has CFC-free `_of_troppPrimitive` / `_of_troppPrimitives` wrappers that reuse `bernsteinMatrixExp_le_quadratic` while keeping Tropp/Lieb and integrability assumptions explicit. +The finite-family conditioning chain now has the thin witness +`troppConditionalStep_of_iIndepFun`; it forwards the explicit per-index +conditional-expectation provider and does not prove the history, independence, +or conditional-expectation inputs themselves. ## Not Yet Proved - Full Tropp/Lieb machinery. - Golden-Thompson route. - Full unconditional Matrix Bernstein theorem. -- Natural history measurability, independence conditioning, and trace-exp - integrability propagation for the conditional-step Tropp route. +- Natural history measurability, independence conditioning, + conditional-expectation reduction, and trace-exp integrability propagation for + the conditional-step Tropp route. - Proofs of the remaining hardbone statement targets for log/order, - Tropp/Lieb, conditioning, integrability, variance-proxy sharpening, and + Tropp/Lieb, integrability, variance-proxy sharpening, and dimension/rank refinements. - A public-friendly Matrix Bernstein wrapper directly over the natural-state route.