From d1669909ce1507d50a88f672e651e71cfe2e9843 Mon Sep 17 00:00:00 2001 From: HighDimProb Dev Date: Sat, 20 Jun 2026 06:16:38 +0000 Subject: [PATCH] Package exact-row centered-square assumptions Expose semantic bundles for the exact-row centered-square sample-covariance routes so downstream callers can reuse the PR #22 wrappers without repeating the full proof-facing hypothesis list. The wrappers only destruct bundles and preserve every analytic and Tropp/centered-square premise explicitly.\n\nConstraint: stacked on PR #22 because the centered-square wrapper primitives are not merged to main yet.\nRejected: changing existing primitive wrapper signatures | would disrupt the current PR #22 API and compatibility checks.\nConfidence: high\nScope-risk: narrow\nDirective: Do not treat these bundles as proving the centered-square chain, Tropp/Lieb, trace-MGF, Matrix Bernstein, or unconditional concentration.\nTested: lake build HighDimProb.RandomMatrix.ConcentrationStatements; lake env lean HighDimProbTest/RandomMatrixConcentrationAPI.lean; lake env lean HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean; python .github/scripts/check_text_quality.py; python scripts/judge_policy_check.py; git diff --check; lake build HighDimProbJudge; lake test; lake build\nNot-tested: GitHub CI on the stacked branch has not run yet. --- .../RandomMatrix/ConcentrationStatements.lean | 192 ++++++++++++++++++ .../RandomMatrix/MatrixBernsteinUse.lean | 4 + .../RandomMatrixConcentrationAPI.lean | 4 + docs/JudgeSystem.md | 2 +- docs/RandomMatrixAPI.md | 6 +- docs/Status.md | 4 + docs/TODO.md | 11 +- docs/TestPlan.md | 2 +- docs/TheoremAtlas.md | 2 +- 9 files changed, 218 insertions(+), 9 deletions(-) diff --git a/HighDimProb/RandomMatrix/ConcentrationStatements.lean b/HighDimProb/RandomMatrix/ConcentrationStatements.lean index a54401c..8d6bfa3 100644 --- a/HighDimProb/RandomMatrix/ConcentrationStatements.lean +++ b/HighDimProb/RandomMatrix/ConcentrationStatements.lean @@ -2721,6 +2721,131 @@ theorem sampleCovariance_quadraticForm_tail_optimized_under_explicit_variance_pr (sampleCovarianceCenteredRankOneRadius R)) hTropp + +/-- Positive-side assumption bundle for the exact-row centered-square-chain +sample-covariance route. + +This packages the hypotheses consumed by +`sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppPrimitive`. +It is only a semantic bundle: the generic centered-square variance-proxy chain, +Tropp/Lieb trace-MGF primitive, independence, integrability, and radius +conditions remain explicit fields. -/ +structure SampleCovarianceExactRowCenteredSquareTroppAssumptions {Omega : Type*} + [MeasurableSpace Omega] {P : Measure Omega} [IsProbabilityMeasure P] + {m n : Nat} + (A : RandomMatrix Omega m n) (R t : Real) (Rvar : Fin m -> Real) : Prop where + nonemptyRows : 0 < m + measurable : IsRandomMatrix P A + rowMemLp : + forall k : Fin m, forall j : Fin n, + MemLpRealRandomVariable P (matrixEntry A k j) 2 + rowSqNormBound : + forall k : Fin m, forall omega, + vectorSqNorm (rowVector A k omega) <= R + rowSqNormVarianceBound : + forall k : Fin m, forall omega, + vectorSqNorm (rowVector A k omega) <= Rvar k + independentRows : + IndependentRandomMatrices P + (centeredSampleCovarianceRowRankOneFamily (P := P) A) + expIntegrable : + forall k : Fin m, + IntegrableRandomMatrix P + (matrixExpScaledFamily + (centeredSampleCovarianceRowRankOneFamily (P := P) A) + (sampleCovarianceTailTheta (m := m) R t + (rowSqNormVarianceProxyNormRHS Rvar)) + k) + traceExpIntegrable : + IntegrableRealRandomVariable P + (traceExpIntegrand + (centeredSampleCovarianceRowRankOneSum (P := P) A) + (sampleCovarianceTailTheta (m := m) R t + (rowSqNormVarianceProxyNormRHS Rvar))) + variancePositive : 0 < rowSqNormVarianceProxyNormRHS Rvar + radiusNonneg : 0 <= R + varianceRadiiNonneg : forall i : Fin m, 0 <= Rvar i + deviationPositive : 0 < t + centeredSquareChain : + @varianceProxyNormBound_of_centeredSquareChain_statement + Omega _ P _ (Fin m) _ n + (rankOneRandomMatrixFamily (rowVector A)) + (fun i => matrixSecondMoment P (rankOneRandomMatrix (rowVector A i))) + (rowSqNormVarianceProxyNormRHS Rvar) + troppPrimitive : + troppMasterTraceMGFFiniteFamily_statement + (P := P) + (centeredSampleCovarianceRowRankOneFamily (P := P) A) + (bernsteinSecondMomentComparisonFamily P + (centeredSampleCovarianceRowRankOneFamily (P := P) A) + (sampleCovarianceTailTheta (m := m) R t + (rowSqNormVarianceProxyNormRHS Rvar)) + (sampleCovarianceCenteredRankOneRadius R)) + (matrixVarianceProxy P + (centeredSampleCovarianceRowRankOneFamily (P := P) A)) + (sampleCovarianceTailTheta (m := m) R t + (rowSqNormVarianceProxyNormRHS Rvar)) + (sampleCovarianceCenteredRankOneRadius R) + +/-- Two-sided/operator-norm assumption bundle for the exact-row +centered-square-chain sample-covariance route. + +The positive-side fields are reused through +`SampleCovarianceExactRowCenteredSquareTroppAssumptions`. Negative-side fields +remain explicit because they use the negative centered row-rank-one family and a +separate variance-radius family. -/ +structure SampleCovarianceExactRowCenteredSquareTwoSidedTroppAssumptions + {Omega : Type*} [MeasurableSpace Omega] {P : Measure Omega} + [IsProbabilityMeasure P] {m n : Nat} + (A : RandomMatrix Omega m n) (R Rneg t : Real) + (Rvar RvarNeg : Fin m -> Real) : Prop where + positive : + SampleCovarianceExactRowCenteredSquareTroppAssumptions + (P := P) A R t Rvar + negRowSqNormBound : + forall k : Fin m, forall omega, + vectorSqNorm (rowVector A k omega) <= Rneg + negRowSqNormVarianceBound : + forall k : Fin m, forall omega, + vectorSqNorm (rowVector A k omega) <= RvarNeg k + negExpIntegrable : + forall k : Fin m, + IntegrableRandomMatrix P + (matrixExpScaledFamily + (centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A) + (sampleCovarianceTailTheta (m := m) Rneg t + (rowSqNormVarianceProxyNormRHS RvarNeg)) + k) + negTraceExpIntegrable : + IntegrableRealRandomVariable P + (traceExpIntegrand + (centeredSampleCovarianceRowRankOneSumNeg (P := P) A) + (sampleCovarianceTailTheta (m := m) Rneg t + (rowSqNormVarianceProxyNormRHS RvarNeg))) + negVariancePositive : 0 < rowSqNormVarianceProxyNormRHS RvarNeg + negRadiusNonneg : 0 <= Rneg + negVarianceRadiiNonneg : forall i : Fin m, 0 <= RvarNeg i + negCenteredSquareChain : + @varianceProxyNormBound_of_centeredSquareChain_statement + Omega _ P _ (Fin m) _ n + (rankOneRandomMatrixFamily (rowVector A)) + (fun i => matrixSecondMoment P (rankOneRandomMatrix (rowVector A i))) + (rowSqNormVarianceProxyNormRHS RvarNeg) + negTroppPrimitive : + troppMasterTraceMGFFiniteFamily_statement + (P := P) + (centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A) + (bernsteinSecondMomentComparisonFamily P + (centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A) + (sampleCovarianceTailTheta (m := m) Rneg t + (rowSqNormVarianceProxyNormRHS RvarNeg)) + (sampleCovarianceCenteredRankOneRadius Rneg)) + (matrixVarianceProxy P + (centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A)) + (sampleCovarianceTailTheta (m := m) Rneg t + (rowSqNormVarianceProxyNormRHS RvarNeg)) + (sampleCovarianceCenteredRankOneRadius Rneg) + /-- Sample-covariance quadratic-form upper-tail wrapper using the exact-row bounded-row variance-proxy consumer. @@ -2917,6 +3042,36 @@ theorem sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound (P := P) (A := A) (R := R) (t := t) (Rvar := Rvar) hm hMeas hLp hSq hSqVar hIndep hExpInt hTraceInt hSigma hR hRvar ht hSharp hTropp + +/-- Sample-covariance quadratic-form upper-tail wrapper consuming the bundled +exact-row centered-square-chain Tropp assumptions. + +This is a thin natural-state wrapper over +`sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppPrimitive`. +It packages existing premises only and proves no new Tropp/Lieb, trace-MGF, +variance-proxy, or concentration theorem. -/ +theorem sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppAssumptions + {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_troppPrimitive + (P := P) (A := A) (R := R) (t := t) (Rvar := Rvar) + h.nonemptyRows h.measurable h.rowMemLp h.rowSqNormBound + h.rowSqNormVarianceBound h.independentRows h.expIntegrable + h.traceExpIntegrable h.variancePositive h.radiusNonneg + h.varianceRadiiNonneg h.deviationPositive h.centeredSquareChain + h.troppPrimitive + /-- Sample-covariance quadratic-form upper-tail wrapper using the crude bounded-row variance-proxy norm bound. @@ -4040,6 +4195,43 @@ theorem sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos hSigma hR hRvar ht hSharp hTropp hExpIntNeg hTraceIntNeg hSigmaNeg hRNeg hRvarNeg hSharpNeg hTroppNeg + +/-- Arbitrary-column sample-covariance operator-norm wrapper consuming the +bundled exact-row centered-square-chain Tropp assumptions. + +This is a thin natural-state wrapper over the corresponding `..._of_troppPrimitives` +route. It keeps the positive and negative centered-square chains and Tropp +primitives explicit inside the bundle. -/ +theorem sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppAssumptions + {Omega : Type*} [MeasurableSpace Omega] {P : Measure Omega} + [IsProbabilityMeasure P] {m n : Nat} + (A : RandomMatrix Omega m n) + (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) R t (rowSqNormVarianceProxyNormRHS Rvar) + + sampleCovarianceQuadraticFormTailRHS + (m := m) (n := n) Rneg t + (rowSqNormVarianceProxyNormRHS RvarNeg) := by + exact + sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppPrimitives + (P := P) (A := A) (R := R) (Rneg := Rneg) (t := t) + (Rvar := Rvar) (RvarNeg := RvarNeg) + h.positive.nonemptyRows h.positive.measurable h.positive.rowMemLp + h.positive.rowSqNormBound h.negRowSqNormBound + h.positive.rowSqNormVarianceBound h.negRowSqNormVarianceBound + h.positive.independentRows h.positive.expIntegrable + h.positive.traceExpIntegrable h.positive.variancePositive + h.positive.radiusNonneg h.positive.varianceRadiiNonneg + h.positive.deviationPositive h.positive.centeredSquareChain + h.positive.troppPrimitive h.negExpIntegrable h.negTraceExpIntegrable + h.negVariancePositive h.negRadiusNonneg h.negVarianceRadiiNonneg + h.negCenteredSquareChain h.negTroppPrimitive + /-- Arbitrary-column sample-covariance self-adjoint operator-norm tail wrapper using crude bounded-row variance-proxy norm bounds. diff --git a/HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean b/HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean index 539a20b..7f0e04f 100644 --- a/HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean +++ b/HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean @@ -46,6 +46,8 @@ open HighDimProb #check HighDimProb.sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound_of_troppPrimitive #check HighDimProb.sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_troppPrimitive #check HighDimProb.sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppPrimitive +#check HighDimProb.SampleCovarianceExactRowCenteredSquareTroppAssumptions +#check HighDimProb.sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppAssumptions #check HighDimProb.sampleCovariance_selfAdjointOperatorNormTailEvent_subset_centeredRowRankOneSum #check HighDimProb.sampleCovariance_selfAdjointOperatorNorm_tail_optimized_under_explicit_variance_proxy #check HighDimProb.sampleCovariance_selfAdjointOperatorNorm_tail_optimized_nonempty_under_explicit_variance_proxy @@ -57,6 +59,8 @@ open HighDimProb #check HighDimProb.sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives #check HighDimProb.sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives #check HighDimProb.sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppPrimitives +#check HighDimProb.SampleCovarianceExactRowCenteredSquareTwoSidedTroppAssumptions +#check HighDimProb.sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppAssumptions #check HighDimProb.negRandomMatrixFamily #check HighDimProb.matrixExpScaledFamily_negRandomMatrixFamily #check HighDimProb.integrableRandomMatrix_matrixExpScaledFamily_negRandomMatrixFamily diff --git a/HighDimProbTest/RandomMatrixConcentrationAPI.lean b/HighDimProbTest/RandomMatrixConcentrationAPI.lean index 3674221..f38cd3e 100644 --- a/HighDimProbTest/RandomMatrixConcentrationAPI.lean +++ b/HighDimProbTest/RandomMatrixConcentrationAPI.lean @@ -160,6 +160,8 @@ variable (R theta sigma2 c c1 c2 t bound K : Real) #check sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound_of_troppPrimitive #check sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_troppPrimitive #check sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppPrimitive +#check SampleCovarianceExactRowCenteredSquareTroppAssumptions +#check sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppAssumptions #check sampleCovariance_selfAdjointOperatorNorm_tail_optimized_under_explicit_variance_proxy #check sampleCovariance_selfAdjointOperatorNorm_tail_optimized_nonempty_under_explicit_variance_proxy #check sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_explicit_variance_proxy @@ -170,6 +172,8 @@ variable (R theta sigma2 c c1 c2 t bound K : Real) #check sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives #check sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives #check sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppPrimitives +#check SampleCovarianceExactRowCenteredSquareTwoSidedTroppAssumptions +#check sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppAssumptions #check centeredSampleCovarianceRowRankOneFamilyNeg #check centeredSampleCovarianceRowRankOneSumNeg #check isRandomMatrix_negRandomMatrixFamily diff --git a/docs/JudgeSystem.md b/docs/JudgeSystem.md index 6b75668..b1e57f4 100644 --- a/docs/JudgeSystem.md +++ b/docs/JudgeSystem.md @@ -73,7 +73,7 @@ theorems or typed statements without relying on local test internals. Laplace/Chernoff/operator-norm Laplace statement APIs. - `HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean`: proof-ready matrix Bernstein statement surface, `matrixBernsteinLaplacePrerequisitesStatement`, - `matrixBernsteinTraceMGF_statement`, sample-covariance exact-row and centered-square-chain wrapper visibility, + `matrixBernsteinTraceMGF_statement`, sample-covariance exact-row centered-square-chain wrapper and assumption-bundle visibility, negative exact-row variance-proxy provider visibility, and their main structural/analytic dependencies. diff --git a/docs/RandomMatrixAPI.md b/docs/RandomMatrixAPI.md index 7ebfbdc..456c01c 100644 --- a/docs/RandomMatrixAPI.md +++ b/docs/RandomMatrixAPI.md @@ -115,7 +115,11 @@ Variance-proxy / centered-square chain: - `sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two` - `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two_of_centeredSquareChain` - `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppPrimitive` +- `SampleCovarianceExactRowCenteredSquareTroppAssumptions` +- `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppAssumptions` - `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppPrimitives` +- `SampleCovarianceExactRowCenteredSquareTwoSidedTroppAssumptions` +- `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppAssumptions` - `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two` - `varianceProxyNormBound_of_centeredSquareChain_statement` - `varianceProxyNormBound_of_centeredSquareChain_expansion` @@ -167,7 +171,7 @@ Hardbone status table: | 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` | 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 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`, `matrixSquare_centeredRandomMatrix_expectation_expansion_statement`, `centeredRankOneSquare_le_rankOneSecondMoment_statement` | centered-square expectation expansion 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`, `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`, `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppPrimitive`, `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppPrimitives`, `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two`, `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives`, `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 proof remains external; wrappers still require Tropp/Lieb and analytic integrability premises | +| Variance proxy / centered square | `varianceProxyNormBound_of_centeredSquareChain_statement`, `matrixSquare_centeredRandomMatrix_expectation_expansion_statement`, `centeredRankOneSquare_le_rankOneSecondMoment_statement` | centered-square expectation expansion 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`, `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`, `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppPrimitive`, `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppPrimitives`, `SampleCovarianceExactRowCenteredSquareTroppAssumptions`, `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppAssumptions`, `SampleCovarianceExactRowCenteredSquareTwoSidedTroppAssumptions`, `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppAssumptions`, `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two`, `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives`, `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 proof remains external; wrappers and bundles still require Tropp/Lieb and analytic integrability premises | | 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 | diff --git a/docs/Status.md b/docs/Status.md index c9a4c1c..2cf9179 100644 --- a/docs/Status.md +++ b/docs/Status.md @@ -84,6 +84,8 @@ Sample covariance wrappers: - `sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound` - `sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound_of_troppPrimitive` - `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_troppPrimitive` +- `SampleCovarianceExactRowCenteredSquareTroppAssumptions` +- `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppAssumptions` - `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound` - `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_adapters` - `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_adapters_of_troppPrimitives` @@ -99,6 +101,8 @@ Sample covariance negative-side provider-transfer adapters: - `centeredSampleCovarianceRowRankOneFamilyNeg_cfcPrimitive_of_cfcPrimitive_neg_theta` - `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two` - `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives` +- `SampleCovarianceExactRowCenteredSquareTwoSidedTroppAssumptions` +- `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppAssumptions` Hardbone proved leaves, deterministic bridges, statement targets, and thin consumers: diff --git a/docs/TODO.md b/docs/TODO.md index 96ba05e..6d2818b 100644 --- a/docs/TODO.md +++ b/docs/TODO.md @@ -17,12 +17,13 @@ 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 closeout: finish PR/check review for - `RM-VP-centered-square-chain-wrapper-integration-contract`. +- Current RandomMatrix hardbone branch: assumption-bundle follow-up for + `RM-natural-state-centered-square-wrapper-assumption-bundling-contract`. - The centered-square-chain wrapper variants are available for both the - positive-side quadratic-form route and the two-sided/operator-norm route. - Keep follow-up tasks from claiming new Tropp/Lieb, trace-MGF, or full Matrix - Bernstein proofs. + positive-side quadratic-form route and the two-sided/operator-norm route; + natural assumption bundles now package those exact-row routes without + discharging the centered-square chain, Tropp/Lieb, trace-MGF, or full Matrix + Bernstein blockers. ## Active Documentation Work diff --git a/docs/TestPlan.md b/docs/TestPlan.md index 0b08583..9bf657a 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, the two-sided/operator-norm exact-row wrappers, 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 two-sided/operator-norm exact-row wrappers, their centered-square assumption bundle, and the negative exact-row variance-proxy provider, are covered in `HighDimProbTest/RandomMatrixConcentrationAPI.lean`, `HighDimProbTest/ExamplesAPI.lean`, and `HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean`. diff --git a/docs/TheoremAtlas.md b/docs/TheoremAtlas.md index 9db21e7..5a39140 100644 --- a/docs/TheoremAtlas.md +++ b/docs/TheoremAtlas.md @@ -78,7 +78,7 @@ supplies it from coordinate `MemLp 4` assumptions via Mathlib Holder product APIs. The bounded-row provider `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_sqNorm_bound_memLp_two` supplies it from coordinate `MemLp 2` plus pointwise `vectorSqNorm <= R`. -Centered rank-one square-integrability providers are proved for coordinate `MemLp 4` and bounded-row `MemLp 2` routes. The row-specific exact-row consumer `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two` now supplies a `rowSqNormVarianceProxyNormRHS R` variance-proxy bound from coordinate `MemLp 2`, pointwise `vectorSqNorm <= R_i`, nonnegative radii, and the explicit hardbone sharp-chain premise. The concrete row-moment bridge `sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two` turns the generic centered-square variance-proxy chain into the exact-row sample-specific sharp-chain statement, and `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two_of_centeredSquareChain` exposes the matching consumer. The generic centered-square chain remains explicit. The negative-side provider `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two` transfers that row-specific bound through `matrixVarianceProxy_negRandomMatrixFamily`. Positive-side quadratic-form tail-wrapper integration is available through `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_troppPrimitive`, with centered-square-chain variant `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppPrimitive`. The CFC-free two-sided/operator-norm integration is available through `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`. +Centered rank-one square-integrability providers are proved for coordinate `MemLp 4` and bounded-row `MemLp 2` routes. The row-specific exact-row consumer `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two` now supplies a `rowSqNormVarianceProxyNormRHS R` variance-proxy bound from coordinate `MemLp 2`, pointwise `vectorSqNorm <= R_i`, nonnegative radii, and the explicit hardbone sharp-chain premise. The concrete row-moment bridge `sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two` turns the generic centered-square variance-proxy chain into the exact-row sample-specific sharp-chain statement, and `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two_of_centeredSquareChain` exposes the matching consumer. The generic centered-square chain remains explicit. The negative-side provider `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two` transfers that row-specific bound through `matrixVarianceProxy_negRandomMatrixFamily`. Positive-side quadratic-form tail-wrapper integration is available through `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_troppPrimitive`, with centered-square-chain variant `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppPrimitive` and bundled route `SampleCovarianceExactRowCenteredSquareTroppAssumptions` / `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppAssumptions`. The CFC-free two-sided/operator-norm integration is available through `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` and bundled route `SampleCovarianceExactRowCenteredSquareTwoSidedTroppAssumptions` / `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppAssumptions`. The rank/support trace-bound bridge is proved by `traceMatrixExp_le_trace_support_exp_lambdaMax_of_supportDomination`, with rank/support consumers for the hardbone targets. Deterministic trace/rank