diff --git a/HighDimProb/Examples/RandomMatrix/HardboneStatementAtlasUsage.lean b/HighDimProb/Examples/RandomMatrix/HardboneStatementAtlasUsage.lean index 1e037cc..1ef0fe9 100644 --- a/HighDimProb/Examples/RandomMatrix/HardboneStatementAtlasUsage.lean +++ b/HighDimProb/Examples/RandomMatrix/HardboneStatementAtlasUsage.lean @@ -23,6 +23,7 @@ open scoped MatrixOrder Matrix.Norms.Operator #check operatorLogMonotoneOnPositiveMatrices_statement #check troppLogExpComparisonToK_of_logOrderKChain_statement #check liebTraceExpConcavity_statement +#check matrixExpLogSelfAdjointNormalization_statement #check troppMasterTraceMGFStep_of_liebJensen_statement #check troppConditionalStep_of_iIndepFun_statement #check matrixExpScaledIntegrable_of_provider_statement @@ -37,6 +38,7 @@ open scoped MatrixOrder Matrix.Norms.Operator #check bernsteinMatrixExp_le_quadratic_of_cfcLeaves #check bernsteinMatrixExp_le_quadratic #check troppLogExpComparisonToK_of_logMonotone_traceExpMono +#check matrixExpLogSelfAdjointNormalization #check troppMasterTraceMGFStep_of_liebJensen #check troppMasterTraceMGFConditionalStep_of_conditioningBridge @@ -50,6 +52,10 @@ example {n : Nat} (A : Matrix (Fin n) (Fin n) Real) (theta R : Real) : example {n : Nat} (H M K : Matrix (Fin n) (Fin n) Real) : Prop := troppLogExpComparisonToK_of_logOrderKChain_statement H M K +example {n : Nat} (A : Matrix (Fin n) (Fin n) Real) : + matrixExpLogSelfAdjointNormalization_statement A := + matrixExpLogSelfAdjointNormalization A + example {Omega : Type*} [MeasurableSpace Omega] (P : Measure Omega) [IsProbabilityMeasure P] {n : Nat} (H : Matrix (Fin n) (Fin n) Real) diff --git a/HighDimProb/RandomMatrix/HardboneStatements.lean b/HighDimProb/RandomMatrix/HardboneStatements.lean index ab29cf2..56e5e62 100644 --- a/HighDimProb/RandomMatrix/HardboneStatements.lean +++ b/HighDimProb/RandomMatrix/HardboneStatements.lean @@ -832,6 +832,17 @@ theorem troppLogExpComparisonToK_of_logMonotone_traceExpMono {n : Nat} troppLogExpComparisonToK_statement H M K := hChain hLog hTrace +/-- Matrix-log normalization for self-adjoint exponentials. + +This is a local CFC normalization leaf. It does not prove Lieb concavity, +Jensen, Golden-Thompson, conditioning, integrability propagation, variance +proxy control, or full Matrix Bernstein. -/ +theorem matrixExpLogSelfAdjointNormalization {n : Nat} + (A : Matrix (Fin n) (Fin n) Real) : + matrixExpLogSelfAdjointNormalization_statement A := by + intro hA + simpa [matrixExp] using (CFC.log_exp (a := A) hA.isSelfAdjoint) + /-- Thin consumer for the Tropp/Lieb/Jensen one-step hardbone chain. This theorem does not prove Lieb concavity, Jensen, or log-exp normalization; diff --git a/HighDimProbJudge/RandomMatrix/TraceExpUse.lean b/HighDimProbJudge/RandomMatrix/TraceExpUse.lean index dd0bb70..a78a101 100644 --- a/HighDimProbJudge/RandomMatrix/TraceExpUse.lean +++ b/HighDimProbJudge/RandomMatrix/TraceExpUse.lean @@ -99,6 +99,7 @@ open scoped MatrixOrder Matrix.Norms.Operator #check HighDimProb.liebJensenTraceExp_statement #check HighDimProb.goldenThompsonTraceExp_statement #check HighDimProb.matrixExpLogSelfAdjointNormalization_statement +#check HighDimProb.matrixExpLogSelfAdjointNormalization #check HighDimProb.troppMasterTraceMGFStep_of_liebJensen_statement #check HighDimProb.troppNaturalHistoryMeasurable_statement #check HighDimProb.troppHistoryStepIndependent_of_iIndepFun_statement diff --git a/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean b/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean index 95686d5..219a346 100644 --- a/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean +++ b/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean @@ -57,6 +57,7 @@ variable (mHist : Fin m -> MeasurableSpace Omega) #check bernsteinMatrixExp_le_quadratic_of_spectrum_cfcOrder #check bernsteinMatrixExp_le_quadratic_of_cfcChain_spectrum #check troppLogExpComparisonToK_of_logMonotone_traceExpMono +#check matrixExpLogSelfAdjointNormalization #check troppMasterTraceMGFStep_of_liebJensen #check troppMasterTraceMGFConditionalStep_of_conditioningBridge @@ -114,3 +115,7 @@ example : example : bernsteinMatrixExp_le_quadratic_statement A theta R := bernsteinMatrixExp_le_quadratic A theta R + +example : + matrixExpLogSelfAdjointNormalization_statement A := + matrixExpLogSelfAdjointNormalization A diff --git a/docs/JudgeSystem.md b/docs/JudgeSystem.md index 2851c9b..a3ab8f9 100644 --- a/docs/JudgeSystem.md +++ b/docs/JudgeSystem.md @@ -64,7 +64,8 @@ theorems or typed statements without relying on local test internals. explicit hypotheses, self-adjoint matrix-exponential PSD and trace nonnegativity bridges, random self-adjoint trace-exp moment nonnegativity, real/lintegral bridge theorem, natural-state Tropp/trace-MGF route checks, - and remaining typed statement APIs. + the hardbone matrix-exp/log normalization theorem, and remaining typed + statement APIs. - `HighDimProbJudge/RandomMatrix/LaplaceUse.lean`: matrix Laplace RHS and lintegral RHS vocabulary, trace-exp threshold events, MB-S5 conditional Markov/Laplace bridge APIs, MB-S6 explicit-dominance conditional wrappers, diff --git a/docs/RandomMatrixAPI.md b/docs/RandomMatrixAPI.md index f0bcfd9..2c673cc 100644 --- a/docs/RandomMatrixAPI.md +++ b/docs/RandomMatrixAPI.md @@ -82,6 +82,7 @@ Tropp/Lieb/Golden-Thompson chain: - `liebJensenTraceExp_statement` - `goldenThompsonTraceExp_statement` - `matrixExpLogSelfAdjointNormalization_statement` +- `matrixExpLogSelfAdjointNormalization` - `troppMasterTraceMGFStep_of_liebJensen_statement` Conditioning / independence chain: diff --git a/docs/Status.md b/docs/Status.md index ab5c807..634359c 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 matrix-exp/log normalization leaf: + +- `matrixExpLogSelfAdjointNormalization` + Example-layer wrappers: - `sampleCovariance_quadraticForm_tail_usage` @@ -114,7 +118,10 @@ 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 local matrix-exp/log normalization leaf is now proved by + `matrixExpLogSelfAdjointNormalization`; it is only the pointwise CFC + normalization consumed by the Tropp/Lieb one-step chain. 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,7 +141,11 @@ 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`. -- Next safe hardbone task: `RM-HB12-select-next-hardbone-proof-leaf`. +- Completed hardbone proof leaf: + `RM-HB12-matrix-exp-log-selfadjoint-normalization-leaf`. +- Next safe hardbone task: select another smallest theorem-backed proof leaf + among the remaining log/order, Tropp/Lieb, integrability, variance-proxy, or + dimension/rank blockers. ## Verification diff --git a/docs/TODO.md b/docs/TODO.md index 7f04f70..15459e9 100644 --- a/docs/TODO.md +++ b/docs/TODO.md @@ -6,14 +6,17 @@ This is the active short list. Old completed task logs were collapsed into ## Active RandomMatrix Work - Select the next smallest theorem-backed hardbone proof leaf with a read-only - Mathlib/API audit before editing Lean. + Mathlib/API audit before editing Lean; the local + `matrixExpLogSelfAdjointNormalization` leaf is now done. - Keep the Matrix Bernstein under-primitives API honest: wrappers may use Tropp/provider assumptions explicitly, but should not claim missing Tropp/Lieb, Golden-Thompson, trace-MGF, or full Matrix Bernstein proofs. - Continue reducing repeated optimized-RHS formulas through shared helpers in `ConcentrationStatements.lean`. - 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`. -- Next RandomMatrix hardbone task: - `RM-HB12-select-next-hardbone-proof-leaf`. +- Completed RandomMatrix hardbone proof leaf: + `RM-HB12-matrix-exp-log-selfadjoint-normalization-leaf`. +- Next RandomMatrix hardbone task: choose the next smallest remaining proof + leaf after a fresh read-only Mathlib/API audit. ## Active Documentation Work diff --git a/docs/TestPlan.md b/docs/TestPlan.md index 9d51701..01aa975 100644 --- a/docs/TestPlan.md +++ b/docs/TestPlan.md @@ -34,7 +34,7 @@ git diff --check `HighDimProbJudge/RandomMatrix/TraceExpUse.lean`; example modules are covered through `lake build HighDimProb.Examples`. - RandomMatrix hardbone statement-target checks, including the proved Bernstein - CFC hardbone leaf, are covered in + CFC hardbone leaf and the proved matrix-exp/log normalization leaf, are covered in `HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean`, `HighDimProbJudge/RandomMatrix/TraceExpUse.lean`, and the `HardboneStatementAtlasUsage` example. diff --git a/docs/TheoremAtlas.md b/docs/TheoremAtlas.md index 5f1dc87..d853033 100644 --- a/docs/TheoremAtlas.md +++ b/docs/TheoremAtlas.md @@ -49,7 +49,9 @@ The preferred optimized Matrix Bernstein wrappers use 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. +assumptions explicit. The local matrix-exp/log normalization leaf is proved as +`matrixExpLogSelfAdjointNormalization`; it supplies only the pointwise CFC +normalization needed by the Tropp/Lieb one-step chain. ## Not Yet Proved @@ -59,8 +61,8 @@ assumptions explicit. - Natural history measurability, independence conditioning, 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 - dimension/rank refinements. + Tropp/Lieb concavity/Jensen, conditioning, integrability, variance-proxy + sharpening, and dimension/rank refinements. - A public-friendly Matrix Bernstein wrapper directly over the natural-state route.