diff --git a/HighDimProb/Examples/RandomMatrix/SampleCovarianceTailUsage.lean b/HighDimProb/Examples/RandomMatrix/SampleCovarianceTailUsage.lean index 8199668..f5093b9 100644 --- a/HighDimProb/Examples/RandomMatrix/SampleCovarianceTailUsage.lean +++ b/HighDimProb/Examples/RandomMatrix/SampleCovarianceTailUsage.lean @@ -104,6 +104,31 @@ theorem sampleCovariance_quadraticForm_tail_usage h.traceExpIntegrable h.radiusPositive h.deviationPositive h.troppPrimitive + +/-- Example-level exact-row centered-square-chain quadratic-form tail usage. + +This demonstrates the core assumption bundle +`SampleCovarianceExactRowCenteredSquareTroppAssumptions` directly, rather than +copying its long field list into an example-local structure. The generic +centered-square chain, Tropp primitive, and analytic assumptions remain fields +of that core bundle. -/ +theorem sampleCovariance_exactRow_centeredSquare_quadraticForm_tail_usage + {Omega : Type*} [MeasurableSpace Omega] {P : Measure Omega} + [IsProbabilityMeasure P] {m n : Nat} + (A : RandomMatrix Omega m (n + 1)) + (R t : Real) + (Rvar : Fin m -> Real) + (h : SampleCovarianceExactRowCenteredSquareTroppAssumptions + (P := P) A R t Rvar) : + P (quadraticFormUpperTailEvent + (centeredRandomMatrix P (sampleCovariance A)) t) <= + sampleCovarianceQuadraticFormTailRHS + (m := m) (n := n + 1) R t + (rowSqNormVarianceProxyNormRHS Rvar) := by + exact + sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppAssumptions + (P := P) A R t Rvar h + /-- Assumptions needed by the public conditional sample-covariance operator-norm tail wrapper. @@ -195,6 +220,32 @@ theorem sampleCovariance_operatorNorm_tail_usage h.negativeRadiusPositive h.troppPrimitiveNeg + +/-- Example-level exact-row centered-square-chain operator-norm tail usage. + +This demonstrates the two-sided core bundle +`SampleCovarianceExactRowCenteredSquareTwoSidedTroppAssumptions`. It adds no +new mathematics; it only routes the bundled assumptions to the public core +wrapper. -/ +theorem sampleCovariance_exactRow_centeredSquare_operatorNorm_tail_usage + {Omega : Type*} [MeasurableSpace Omega] {P : Measure Omega} + [IsProbabilityMeasure P] {m n : Nat} + (A : RandomMatrix Omega m (n + 1)) + (R Rneg t : Real) + (Rvar RvarNeg : Fin m -> Real) + (h : SampleCovarianceExactRowCenteredSquareTwoSidedTroppAssumptions + (P := P) A R Rneg t Rvar RvarNeg) : + P (SelfAdjointOperatorNormTailEvent + (centeredRandomMatrix P (sampleCovariance A)) t) <= + sampleCovarianceQuadraticFormTailRHS + (m := m) (n := n + 1) R t (rowSqNormVarianceProxyNormRHS Rvar) + + sampleCovarianceQuadraticFormTailRHS + (m := m) (n := n + 1) Rneg t + (rowSqNormVarianceProxyNormRHS RvarNeg) := by + exact + sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppAssumptions + (P := P) A R Rneg t Rvar RvarNeg h + end end HighDimProb.Examples.RandomMatrix.SampleCovarianceTailUsage diff --git a/HighDimProb/Examples/RandomMatrix/StatementRoutes.lean b/HighDimProb/Examples/RandomMatrix/StatementRoutes.lean index 62cbdd1..6c9142a 100644 --- a/HighDimProb/Examples/RandomMatrix/StatementRoutes.lean +++ b/HighDimProb/Examples/RandomMatrix/StatementRoutes.lean @@ -39,6 +39,8 @@ obligations without creating another core sample-covariance API. -/ #check sampleCovariance_operatorNorm_tail_usage +#check sampleCovariance_exactRow_centeredSquare_quadraticForm_tail_usage +#check sampleCovariance_exactRow_centeredSquare_operatorNorm_tail_usage /-! ## Rank-one covariance and Gram routes diff --git a/HighDimProbTest/ExamplesAPI.lean b/HighDimProbTest/ExamplesAPI.lean index 30589da..5d41040 100644 --- a/HighDimProbTest/ExamplesAPI.lean +++ b/HighDimProbTest/ExamplesAPI.lean @@ -10,6 +10,8 @@ through `HighDimProb.Examples`. #check HighDimProb.Examples.RandomMatrix.SampleCovarianceUsage.sampleCovariance_psd_usage #check HighDimProb.Examples.RandomMatrix.SampleCovarianceTailUsage.sampleCovariance_quadraticForm_tail_usage #check HighDimProb.Examples.RandomMatrix.SampleCovarianceTailUsage.sampleCovariance_operatorNorm_tail_usage +#check HighDimProb.Examples.RandomMatrix.SampleCovarianceTailUsage.sampleCovariance_exactRow_centeredSquare_quadraticForm_tail_usage +#check HighDimProb.Examples.RandomMatrix.SampleCovarianceTailUsage.sampleCovariance_exactRow_centeredSquare_operatorNorm_tail_usage #check HighDimProb.Examples.RandomMatrix.RankOneMatrixBernsteinPipelineUsage.rankOnePipeline_quadraticForm_tail_optimized_under_primitives #check HighDimProb.Examples.RandomMatrix.RandomFeatureKernelUsage.randomFeatureKernel_quadraticForm_tail_optimized_under_primitives #check HighDimProb.Examples.RandomMatrix.NTKGramUsage.ntkGram_quadraticForm_tail_optimized_under_primitives diff --git a/docs/JudgeSystem.md b/docs/JudgeSystem.md index b1e57f4..c60624b 100644 --- a/docs/JudgeSystem.md +++ b/docs/JudgeSystem.md @@ -337,7 +337,8 @@ python scripts/judge_policy_check.py adapters, the explicit-CFC sample-covariance wrappers, the CFC-free `_of_troppPrimitive` / `_of_troppPrimitives` sample-covariance wrappers, and the opposite-parameter sample-covariance exp/trace/CFC provider-transfer - adapters. + adapters. Example API checks cover the exact-row centered-square bundle usage + wrappers through `StatementRoutes`. - The checks are import-boundary/API checks only; they do not prove exponential/trace integrability, Tropp/Lieb, Golden-Thompson, full Matrix Bernstein, or unconditional sample-covariance concentration. The CFC-free diff --git a/docs/RandomMatrixAPI.md b/docs/RandomMatrixAPI.md index 456c01c..b2c4a38 100644 --- a/docs/RandomMatrixAPI.md +++ b/docs/RandomMatrixAPI.md @@ -289,6 +289,11 @@ The two-sided/operator-norm exact-row integration is exposed as `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives`, with centered-square-chain variant `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppPrimitives`. +The reader-facing example route also exposes +`SampleCovarianceTailUsage.sampleCovariance_exactRow_centeredSquare_quadraticForm_tail_usage` +and +`SampleCovarianceTailUsage.sampleCovariance_exactRow_centeredSquare_operatorNorm_tail_usage` +as thin demonstrations of the corresponding core assumption bundles. These wrappers do not prove Tropp/Lieb, Golden-Thompson, trace-exp integrability, variance-proxy control beyond existing named adapters, or unconditional sample-covariance concentration. @@ -340,6 +345,9 @@ and they are not tail wrappers by themselves. - Prefer named adapters over anonymous lambdas. - Prefer the sample-covariance `_of_troppPrimitive` / `_of_troppPrimitives` wrappers when pointwise Bernstein CFC is the only remaining explicit field. +- For exact-row centered-square routes, prefer the core `SampleCovarianceExactRowCenteredSquare*TroppAssumptions` + bundles and the corresponding `SampleCovarianceTailUsage` examples instead of + copying the full hypothesis list. - Keep positive-side and negative-side assumptions visibly distinct when the theorem still needs both sides. - Put domain vocabulary in examples as thin wrappers over the core RandomMatrix diff --git a/docs/Status.md b/docs/Status.md index 2cf9179..93288f4 100644 --- a/docs/Status.md +++ b/docs/Status.md @@ -93,6 +93,8 @@ Sample covariance wrappers: - `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives` - `SampleCovarianceTailUsage.SampleCovarianceTailAssumptions` - `SampleCovarianceTailUsage.SampleCovarianceOperatorNormTailAssumptions` +- `SampleCovarianceTailUsage.sampleCovariance_exactRow_centeredSquare_quadraticForm_tail_usage` +- `SampleCovarianceTailUsage.sampleCovariance_exactRow_centeredSquare_operatorNorm_tail_usage` Sample covariance negative-side provider-transfer adapters: @@ -264,7 +266,7 @@ Low-level prefix/state, reindex, negative-family, nullspace/decomposition, exact hypotheses. - `StatementRoutes` is an examples-only route index; it groups representative example-level statement families without adding core API. Lower-level bridge and frontier checks belong in source, tests, and judge files rather than separate reader-facing examples. - Positive-threshold operator-norm routes use `0 < t`; the zero-dimensional `t = 0` endpoint is not part of that route. -- Sample covariance wrappers remain conditional APIs, not unconditional concentration theorems. The positive-side quadratic-form route and the two-sided/operator-norm route now have exact-row variance-proxy wrappers, plus centered-square-chain variants that replace sample-specific sharp-chain premises by generic centered-square-chain premises. The named negative sample-covariance family has an exact-row variance-proxy provider. The preferred sample-covariance example route now uses Tropp-only wrappers that fill pointwise Bernstein CFC fields with `bernsteinMatrixExp_le_quadratic`; explicit-CFC wrappers remain compatibility surfaces. +- Sample covariance wrappers remain conditional APIs, not unconditional concentration theorems. The positive-side quadratic-form route and the two-sided/operator-norm route now have exact-row variance-proxy wrappers, plus centered-square-chain variants that replace sample-specific sharp-chain premises by generic centered-square-chain premises. The named negative sample-covariance family has an exact-row variance-proxy provider. The preferred sample-covariance example route now uses Tropp-only wrappers that fill pointwise Bernstein CFC fields with `bernsteinMatrixExp_le_quadratic`; it also includes exact-row centered-square bundle usage examples. Explicit-CFC wrappers remain compatibility surfaces. - Negative-side provider-transfer adapters only move explicit opposite-parameter assumptions onto the named negative sample-covariance family; they do not prove exponential integrability, trace-exponential integrability, or CFC. The diff --git a/docs/TODO.md b/docs/TODO.md index 6d2818b..c66e772 100644 --- a/docs/TODO.md +++ b/docs/TODO.md @@ -17,8 +17,8 @@ This is the active short list. Old completed task logs were collapsed into Matrix Bernstein proofs. - Prefer shared RandomMatrix APIs over unfolded formulas in examples, tests, judge files, and docs. -- Current RandomMatrix hardbone branch: assumption-bundle follow-up for - `RM-natural-state-centered-square-wrapper-assumption-bundling-contract`. +- Current RandomMatrix hardbone branch: example-usage follow-up for + `RM-SC-centered-square-bundle-example-usage-contract`. - The centered-square-chain wrapper variants are available for both the positive-side quadratic-form route and the two-sided/operator-norm route; natural assumption bundles now package those exact-row routes without diff --git a/docs/TestPlan.md b/docs/TestPlan.md index 9bf657a..b61273f 100644 --- a/docs/TestPlan.md +++ b/docs/TestPlan.md @@ -42,7 +42,7 @@ git diff --check `HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean`, `HighDimProbJudge/RandomMatrix/TraceExpUse.lean`. - RandomMatrix sample-covariance negative-side provider-transfer adapters and - CFC-free sample-covariance wrappers, including the positive-side exact-row variance-proxy quadratic-form wrapper, its centered-square-chain variant and assumption bundle, the two-sided/operator-norm exact-row wrappers, their centered-square assumption bundle, and the negative exact-row variance-proxy provider, are covered in + CFC-free sample-covariance wrappers, including the positive-side exact-row variance-proxy quadratic-form wrapper, its centered-square-chain variant and assumption bundle, the example usage route for that bundle, the two-sided/operator-norm exact-row wrappers, their centered-square assumption bundle and example usage route, and the negative exact-row variance-proxy provider, are covered in `HighDimProbTest/RandomMatrixConcentrationAPI.lean`, `HighDimProbTest/ExamplesAPI.lean`, and `HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean`.