From f900a0c440519eee31d52cdfb60087188d00adee Mon Sep 17 00:00:00 2001 From: HighDimProb Dev Date: Fri, 19 Jun 2026 07:00:43 +0000 Subject: [PATCH] Expose sample-covariance wrappers after CFC hardbone Add narrow sample-covariance entry points that fill the pointwise Bernstein CFC premise with the proved bernsteinMatrixExp_le_quadratic leaf while keeping Tropp/Lieb, integrability, and variance-proxy assumptions explicit. Migrate example bundles off public cfcPrimitive fields and extend API/judge/docs coverage for the preferred conditional surface. Constraint: RM-HB-sample-covariance-cfc-free-wrapper-contract only removes caller-supplied pointwise CFC obligations; it must not claim Tropp/Lieb, Golden-Thompson, trace-exp providers, full Matrix Bernstein, or unconditional sample-covariance concentration. Rejected: Proving new analytic Tropp/Lieb or integrability leaves | outside this wrapper-contract scope and unsupported by the current theorem surface. Confidence: high Scope-risk: moderate Directive: Preserve explicit-CFC compatibility wrappers and keep future docs honest about remaining analytic assumptions. Tested: lake env lean HighDimProb/RandomMatrix/ConcentrationStatements.lean; lake env lean HighDimProb/Examples/RandomMatrix/SampleCovarianceTailUsage.lean; lake env lean HighDimProb/Examples/RandomMatrix/BoundedRowSampleCovarianceOperatorNormUsage.lean; lake env lean HighDimProbTest/RandomMatrixConcentrationAPI.lean; lake env lean HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean; lake env lean HighDimProbTest/ExamplesAPI.lean; lake build HighDimProbJudge; lake build HighDimProb.Examples; lake test; lake build; python scripts/judge_policy_check.py; python .github/scripts/check_text_quality.py; git diff --check; independent code-reviewer APPROVE; architect CLEAR. Not-tested: GitHub PR checks not run locally. --- ...dRowSampleCovarianceOperatorNormUsage.lean | 3 +- .../SampleCovarianceTailUsage.lean | 32 +- .../RandomMatrix/ConcentrationStatements.lean | 390 ++++++++++++++++++ .../RandomMatrix/MatrixBernsteinUse.lean | 4 + HighDimProbTest/ExamplesAPI.lean | 2 + .../RandomMatrixConcentrationAPI.lean | 4 + docs/AssumptionVocabulary.md | 10 +- docs/JudgeSystem.md | 15 +- docs/RandomMatrixAPI.md | 18 + docs/Status.md | 10 +- docs/TODO.md | 9 +- docs/TestPlan.md | 6 +- docs/TheoremAtlas.md | 7 +- 13 files changed, 461 insertions(+), 49 deletions(-) diff --git a/HighDimProb/Examples/RandomMatrix/BoundedRowSampleCovarianceOperatorNormUsage.lean b/HighDimProb/Examples/RandomMatrix/BoundedRowSampleCovarianceOperatorNormUsage.lean index 33b874f..274239c 100644 --- a/HighDimProb/Examples/RandomMatrix/BoundedRowSampleCovarianceOperatorNormUsage.lean +++ b/HighDimProb/Examples/RandomMatrix/BoundedRowSampleCovarianceOperatorNormUsage.lean @@ -26,7 +26,8 @@ The assumptions are exactly the canonical sample-covariance operator-norm usage assumptions. They keep the positive bounded-row route visible through `SampleCovarianceTailAssumptions`, derive negative structural and square-integrability obligations via named adapters, and leave negative -exponential/trace integrability plus CFC/Tropp primitives explicit. +exponential/trace integrability plus Tropp primitives explicit; the Bernstein +CFC field is filled by the core wrapper. -/ theorem boundedRowSampleCovariance_operatorNorm_tail_usage {Omega : Type*} [MeasurableSpace Omega] {P : Measure Omega} diff --git a/HighDimProb/Examples/RandomMatrix/SampleCovarianceTailUsage.lean b/HighDimProb/Examples/RandomMatrix/SampleCovarianceTailUsage.lean index 0a1e00e..8a097a0 100644 --- a/HighDimProb/Examples/RandomMatrix/SampleCovarianceTailUsage.lean +++ b/HighDimProb/Examples/RandomMatrix/SampleCovarianceTailUsage.lean @@ -5,7 +5,7 @@ import HighDimProb.RandomMatrix.ConcentrationStatements This examples-only file shows the preferred public API for the conditional sample-covariance quadratic-form and operator-norm tail bounds. It keeps the -independence, integrability, Tropp, Bernstein CFC, and analytic primitive +independence, integrability, Tropp, and analytic primitive assumptions explicit, while the crude bounded-row variance-proxy norm bound is supplied by the core wrappers. Radius, theta, variance-proxy RHS, and tail RHS helpers come from the core concentration API. The RHS helper takes the actual @@ -23,7 +23,7 @@ noncomputable section The structural centered rank-one assumptions and the centered operator-norm bound are discharged by the core theorem from the row-level hypotheses. The crude variance-proxy norm bound is derived from the row squared-norm bound; -the analytic Matrix Bernstein primitives remain explicit. -/ +the remaining Tropp/Lieb Matrix Bernstein primitive remains explicit. -/ structure SampleCovarianceTailAssumptions {Omega : Type*} [MeasurableSpace Omega] {P : Measure Omega} [IsProbabilityMeasure P] {m n : Nat} @@ -61,13 +61,6 @@ structure SampleCovarianceTailAssumptions {Omega : Type*} (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) R))) radiusPositive : 0 < R deviationPositive : 0 < t - cfcPrimitive : - forall k : Fin m, forall omega, - bernsteinMatrixExp_le_quadratic_statement - ((centeredSampleCovarianceRowRankOneFamily (P := P) A) k omega) - (sampleCovarianceTailTheta (m := m) R t - (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) R)) - (sampleCovarianceCenteredRankOneRadius R) troppPrimitive : troppMasterTraceMGFFiniteFamily_statement (P := P) @@ -86,7 +79,7 @@ structure SampleCovarianceTailAssumptions {Omega : Type*} /-- Preferred example-level sample-covariance quadratic-form tail wrapper. This is only a readability layer over -`sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound`; +`sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound_of_troppPrimitive`; all analytic assumptions remain visible in `SampleCovarianceTailAssumptions`. -/ theorem sampleCovariance_quadraticForm_tail_usage @@ -101,12 +94,12 @@ theorem sampleCovariance_quadraticForm_tail_usage (m := m) (n := n + 1) R t (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) R) := by exact - sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound + sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound_of_troppPrimitive (P := P) A R t h.sampleCountPositive h.randomMatrix h.coordinateMemLpTwo h.rowSqNormBound h.independentRows h.squareIntegrable h.expIntegrable h.traceExpIntegrable h.radiusPositive h.deviationPositive - h.cfcPrimitive h.troppPrimitive + h.troppPrimitive /-- Assumptions needed by the public conditional sample-covariance operator-norm tail wrapper. @@ -116,7 +109,7 @@ The positive-sign sample-covariance assumptions reuse integrability, independence, square-integrability, and pointwise operator-norm bounds are supplied by named row/negation adapters from the row `MemLp 2`, positive square-integrability, and row squared-norm assumptions. Negative -matrix-exponential integrability, trace-integrability, CFC, and Tropp +matrix-exponential integrability, trace-integrability, and Tropp primitives remain explicit. -/ structure SampleCovarianceOperatorNormTailAssumptions {Omega : Type*} [MeasurableSpace Omega] {P : Measure Omega} [IsProbabilityMeasure P] @@ -143,13 +136,6 @@ structure SampleCovarianceOperatorNormTailAssumptions {Omega : Type*} (sampleCovarianceTailTheta (m := m) Rneg t (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) Rneg))) negativeRadiusPositive : 0 < Rneg - cfcPrimitiveNeg : - forall k : Fin m, forall omega, - bernsteinMatrixExp_le_quadratic_statement - ((centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A) k omega) - (sampleCovarianceTailTheta (m := m) Rneg t - (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) Rneg)) - (sampleCovarianceCenteredRankOneRadius Rneg) troppPrimitiveNeg : troppMasterTraceMGFFiniteFamily_statement (P := P) @@ -168,7 +154,7 @@ structure SampleCovarianceOperatorNormTailAssumptions {Omega : Type*} /-- Preferred example-level sample-covariance operator-norm tail wrapper. This is only a readability layer over -`sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters`; +`sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives`; all analytic assumptions that are not discharged by named row/negation adapters remain visible in `SampleCovarianceOperatorNormTailAssumptions`. -/ theorem sampleCovariance_operatorNorm_tail_usage @@ -187,7 +173,7 @@ theorem sampleCovariance_operatorNorm_tail_usage (m := m) (n := n + 1) Rneg t (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) Rneg) := by exact - sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters + sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives (P := P) A R Rneg t h.positiveSide.sampleCountPositive h.positiveSide.randomMatrix @@ -200,12 +186,10 @@ theorem sampleCovariance_operatorNorm_tail_usage h.positiveSide.traceExpIntegrable h.positiveSide.radiusPositive h.positiveSide.deviationPositive - h.positiveSide.cfcPrimitive h.positiveSide.troppPrimitive h.expIntegrableNeg h.traceExpIntegrableNeg h.negativeRadiusPositive - h.cfcPrimitiveNeg h.troppPrimitiveNeg end diff --git a/HighDimProb/RandomMatrix/ConcentrationStatements.lean b/HighDimProb/RandomMatrix/ConcentrationStatements.lean index e2cb413..2f879eb 100644 --- a/HighDimProb/RandomMatrix/ConcentrationStatements.lean +++ b/HighDimProb/RandomMatrix/ConcentrationStatements.lean @@ -2596,6 +2596,80 @@ theorem sampleCovariance_quadraticForm_tail_optimized_under_explicit_variance_pr field_simp [ne_of_gt hmReal] exact le_trans (measure_mono hSubset) hMBNamed +/-- Sample-covariance quadratic-form upper-tail wrapper under explicit variance +proxy and the proved Bernstein CFC hardbone leaf. + +This is the CFC-free variant of +`sampleCovariance_quadraticForm_tail_optimized_under_explicit_variance_proxy`: +the caller still supplies the finite-family Tropp/Lieb trace-MGF primitive and +analytic integrability assumptions, but not a pointwise Bernstein CFC field. -/ +theorem sampleCovariance_quadraticForm_tail_optimized_under_explicit_variance_proxy_of_troppPrimitive + {Omega : Type*} [MeasurableSpace Omega] {P : Measure Omega} + [IsProbabilityMeasure P] {m n : Nat} + (A : RandomMatrix Omega m (n + 1)) + (R t sigmaSq : Real) + (hm : 0 < m) + (hMeas : IsRandomMatrix P A) + (hLp : + forall k : Fin m, forall j : Fin (n + 1), + MemLpRealRandomVariable P (matrixEntry A k j) 2) + (hSq : + forall k : Fin m, forall omega, + vectorSqNorm (rowVector A k omega) <= R) + (hIndep : + IndependentRandomMatrices P + (centeredSampleCovarianceRowRankOneFamily (P := P) A)) + (hIntSq : + forall k : Fin m, + IntegrableRandomMatrix P + (randomMatrixSquare + ((centeredSampleCovarianceRowRankOneFamily (P := P) A) k))) + (hExpInt : + forall k : Fin m, + IntegrableRandomMatrix P + (matrixExpScaledFamily + (centeredSampleCovarianceRowRankOneFamily (P := P) A) + (sampleCovarianceTailTheta (m := m) R t sigmaSq) + k)) + (hTraceInt : + IntegrableRealRandomVariable P + (traceExpIntegrand + (centeredSampleCovarianceRowRankOneSum (P := P) A) + (sampleCovarianceTailTheta (m := m) R t sigmaSq))) + (hSigma : 0 < sigmaSq) + (hR : 0 <= R) + (ht : 0 < t) + (hNorm : + MatrixVarianceProxyNormBound P + (centeredSampleCovarianceRowRankOneFamily (P := P) A) sigmaSq) + (hTropp : + troppMasterTraceMGFFiniteFamily_statement + (P := P) + (centeredSampleCovarianceRowRankOneFamily (P := P) A) + (bernsteinSecondMomentComparisonFamily P + (centeredSampleCovarianceRowRankOneFamily (P := P) A) + (sampleCovarianceTailTheta (m := m) R t sigmaSq) + (sampleCovarianceCenteredRankOneRadius R)) + (matrixVarianceProxy P + (centeredSampleCovarianceRowRankOneFamily (P := P) A)) + (sampleCovarianceTailTheta (m := m) R t sigmaSq) + (sampleCovarianceCenteredRankOneRadius R)) : + P (quadraticFormUpperTailEvent + (centeredRandomMatrix P (sampleCovariance A)) t) <= + sampleCovarianceQuadraticFormTailRHS + (m := m) (n := n + 1) R t sigmaSq := by + exact + sampleCovariance_quadraticForm_tail_optimized_under_explicit_variance_proxy + (P := P) (A := A) (R := R) (t := t) (sigmaSq := sigmaSq) + hm hMeas hLp hSq hIndep hIntSq hExpInt hTraceInt hSigma hR ht + hNorm + (fun k omega => + bernsteinMatrixExp_le_quadratic + ((centeredSampleCovarianceRowRankOneFamily (P := P) A) k omega) + (sampleCovarianceTailTheta (m := m) R t sigmaSq) + (sampleCovarianceCenteredRankOneRadius R)) + hTropp + /-- Sample-covariance quadratic-form upper-tail wrapper using the crude bounded-row variance-proxy norm bound. @@ -2682,6 +2756,81 @@ theorem sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound hm hMeas hLp hSq hIndep hIntSq hExpInt hTraceInt hSigma hR.le ht hNorm hCFC hTropp +/-- Preferred sample-covariance quadratic-form wrapper after the Bernstein CFC +hardbone leaf. + +This is the CFC-free bounded-row entry point: the caller still supplies the +finite-family Tropp/Lieb trace-MGF primitive and analytic integrability +assumptions, but no longer supplies a pointwise Bernstein CFC field. The +pointwise CFC inequality is filled by `bernsteinMatrixExp_le_quadratic`. -/ +theorem sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound_of_troppPrimitive + {Omega : Type*} [MeasurableSpace Omega] {P : Measure Omega} + [IsProbabilityMeasure P] {m n : Nat} + (A : RandomMatrix Omega m (n + 1)) + (R t : Real) + (hm : 0 < m) + (hMeas : IsRandomMatrix P A) + (hLp : + forall k : Fin m, forall j : Fin (n + 1), + MemLpRealRandomVariable P (matrixEntry A k j) 2) + (hSq : + forall k : Fin m, forall omega, + vectorSqNorm (rowVector A k omega) <= R) + (hIndep : + IndependentRandomMatrices P + (centeredSampleCovarianceRowRankOneFamily (P := P) A)) + (hIntSq : + forall k : Fin m, + IntegrableRandomMatrix P + (randomMatrixSquare + ((centeredSampleCovarianceRowRankOneFamily (P := P) A) k))) + (hExpInt : + forall k : Fin m, + IntegrableRandomMatrix P + (matrixExpScaledFamily + (centeredSampleCovarianceRowRankOneFamily (P := P) A) + (sampleCovarianceTailTheta (m := m) R t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) R)) + k)) + (hTraceInt : + IntegrableRealRandomVariable P + (traceExpIntegrand + (centeredSampleCovarianceRowRankOneSum (P := P) A) + (sampleCovarianceTailTheta (m := m) R t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) R)))) + (hR : 0 < R) + (ht : 0 < t) + (hTropp : + troppMasterTraceMGFFiniteFamily_statement + (P := P) + (centeredSampleCovarianceRowRankOneFamily (P := P) A) + (bernsteinSecondMomentComparisonFamily P + (centeredSampleCovarianceRowRankOneFamily (P := P) A) + (sampleCovarianceTailTheta (m := m) R t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) R)) + (sampleCovarianceCenteredRankOneRadius R)) + (matrixVarianceProxy P + (centeredSampleCovarianceRowRankOneFamily (P := P) A)) + (sampleCovarianceTailTheta (m := m) R t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) R)) + (sampleCovarianceCenteredRankOneRadius R)) : + P (quadraticFormUpperTailEvent + (centeredRandomMatrix P (sampleCovariance A)) t) <= + sampleCovarianceQuadraticFormTailRHS + (m := m) (n := n + 1) R t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) R) := by + exact + sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound + (P := P) A R t + hm hMeas hLp hSq hIndep hIntSq hExpInt hTraceInt hR ht + (fun k omega => + bernsteinMatrixExp_le_quadratic + ((centeredSampleCovarianceRowRankOneFamily (P := P) A) k omega) + (sampleCovarianceTailTheta (m := m) R t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) R)) + (sampleCovarianceCenteredRankOneRadius R)) + hTropp + /-- Sample-covariance self-adjoint operator-norm tail wrapper under explicit variance-proxy and Matrix Bernstein primitive assumptions. @@ -3623,6 +3772,128 @@ theorem sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos hTropp hCenteredNeg hIndepSANeg hIntXNeg hIntSqNeg hExpIntNeg hTraceIntNeg hBoundNeg hRNeg hCFCNeg hTroppNeg +/-- Bounded-row sample-covariance operator-norm wrapper using negative-family +adapters and the proved Bernstein CFC hardbone leaf. + +This is the CFC-free variant of +`sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_adapters`: +it still leaves negative square/exponential/trace integrability and both +sign-specific finite-family Tropp/Lieb primitives explicit. -/ +theorem sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_adapters_of_troppPrimitives + {Omega : Type*} [MeasurableSpace Omega] {P : Measure Omega} + [IsProbabilityMeasure P] {m n : Nat} + (A : RandomMatrix Omega m n) + (R Rneg t : Real) + (hm : 0 < m) + (hMeas : IsRandomMatrix P A) + (hLp : + forall k : Fin m, forall j : Fin n, + MemLpRealRandomVariable P (matrixEntry A k j) 2) + (hSq : + forall k : Fin m, forall omega, + vectorSqNorm (rowVector A k omega) <= R) + (hSqNeg : + forall k : Fin m, forall omega, + vectorSqNorm (rowVector A k omega) <= Rneg) + (hIndep : + IndependentRandomMatrices P + (centeredSampleCovarianceRowRankOneFamily (P := P) A)) + (hIntSq : + forall k : Fin m, + IntegrableRandomMatrix P + (randomMatrixSquare + ((centeredSampleCovarianceRowRankOneFamily (P := P) A) k))) + (hExpInt : + forall k : Fin m, + IntegrableRandomMatrix P + (matrixExpScaledFamily + (centeredSampleCovarianceRowRankOneFamily (P := P) A) + (sampleCovarianceTailTheta (m := m) R t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) R)) + k)) + (hTraceInt : + IntegrableRealRandomVariable P + (traceExpIntegrand + (centeredSampleCovarianceRowRankOneSum (P := P) A) + (sampleCovarianceTailTheta (m := m) R t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) R)))) + (hR : 0 < R) + (ht : 0 < t) + (hTropp : + troppMasterTraceMGFFiniteFamily_statement + (P := P) + (centeredSampleCovarianceRowRankOneFamily (P := P) A) + (bernsteinSecondMomentComparisonFamily P + (centeredSampleCovarianceRowRankOneFamily (P := P) A) + (sampleCovarianceTailTheta (m := m) R t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) R)) + (sampleCovarianceCenteredRankOneRadius R)) + (matrixVarianceProxy P + (centeredSampleCovarianceRowRankOneFamily (P := P) A)) + (sampleCovarianceTailTheta (m := m) R t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) R)) + (sampleCovarianceCenteredRankOneRadius R)) + (hIntSqNeg : + forall k : Fin m, + IntegrableRandomMatrix P + (randomMatrixSquare + ((centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A) k))) + (hExpIntNeg : + forall k : Fin m, + IntegrableRandomMatrix P + (matrixExpScaledFamily + (centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A) + (sampleCovarianceTailTheta (m := m) Rneg t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) Rneg)) + k)) + (hTraceIntNeg : + IntegrableRealRandomVariable P + (traceExpIntegrand + (centeredSampleCovarianceRowRankOneSumNeg (P := P) A) + (sampleCovarianceTailTheta (m := m) Rneg t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) Rneg)))) + (hRNeg : 0 < Rneg) + (hTroppNeg : + troppMasterTraceMGFFiniteFamily_statement + (P := P) + (centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A) + (bernsteinSecondMomentComparisonFamily P + (centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A) + (sampleCovarianceTailTheta (m := m) Rneg t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) Rneg)) + (sampleCovarianceCenteredRankOneRadius Rneg)) + (matrixVarianceProxy P + (centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A)) + (sampleCovarianceTailTheta (m := m) Rneg t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) Rneg)) + (sampleCovarianceCenteredRankOneRadius Rneg)) : + P (SelfAdjointOperatorNormTailEvent + (centeredRandomMatrix P (sampleCovariance A)) t) <= + sampleCovarianceQuadraticFormTailRHS + (m := m) (n := n) R t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) R) + + sampleCovarianceQuadraticFormTailRHS + (m := m) (n := n) Rneg t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) Rneg) := by + exact + sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_adapters + (P := P) (A := A) (R := R) (Rneg := Rneg) (t := t) + hm hMeas hLp hSq hSqNeg hIndep hIntSq hExpInt hTraceInt hR ht + (fun k omega => + bernsteinMatrixExp_le_quadratic + ((centeredSampleCovarianceRowRankOneFamily (P := P) A) k omega) + (sampleCovarianceTailTheta (m := m) R t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) R)) + (sampleCovarianceCenteredRankOneRadius R)) + hTropp hIntSqNeg hExpIntNeg hTraceIntNeg hRNeg + (fun k omega => + bernsteinMatrixExp_le_quadratic + ((centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A) k omega) + (sampleCovarianceTailTheta (m := m) Rneg t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) Rneg)) + (sampleCovarianceCenteredRankOneRadius Rneg)) + hTroppNeg + /-- Bounded-row sample-covariance operator-norm wrapper with negative-family adapters and the square-integrability transfer `(-X)^2 = X^2`. @@ -3753,6 +4024,125 @@ theorem sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos hCFC hTropp hIntSqNeg hExpIntNeg hTraceIntNeg hRNeg hCFCNeg hTroppNeg +/-- +Preferred bounded-row sample-covariance operator-norm wrapper after the +Bernstein CFC hardbone leaf. + +This is the CFC-free version of +`sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters`. +It still keeps the sign-specific finite-family Tropp/Lieb primitives and +integrability assumptions explicit, but fills both pointwise Bernstein CFC +premises with the proved theorem `bernsteinMatrixExp_le_quadratic`. -/ +theorem sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives + {Omega : Type*} [MeasurableSpace Omega] {P : Measure Omega} + [IsProbabilityMeasure P] {m n : Nat} + (A : RandomMatrix Omega m n) + (R Rneg t : Real) + (hm : 0 < m) + (hMeas : IsRandomMatrix P A) + (hLp : + forall k : Fin m, forall j : Fin n, + MemLpRealRandomVariable P (matrixEntry A k j) 2) + (hSq : + forall k : Fin m, forall omega, + vectorSqNorm (rowVector A k omega) <= R) + (hSqNeg : + forall k : Fin m, forall omega, + vectorSqNorm (rowVector A k omega) <= Rneg) + (hIndep : + IndependentRandomMatrices P + (centeredSampleCovarianceRowRankOneFamily (P := P) A)) + (hIntSq : + forall k : Fin m, + IntegrableRandomMatrix P + (randomMatrixSquare + ((centeredSampleCovarianceRowRankOneFamily (P := P) A) k))) + (hExpInt : + forall k : Fin m, + IntegrableRandomMatrix P + (matrixExpScaledFamily + (centeredSampleCovarianceRowRankOneFamily (P := P) A) + (sampleCovarianceTailTheta (m := m) R t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) R)) + k)) + (hTraceInt : + IntegrableRealRandomVariable P + (traceExpIntegrand + (centeredSampleCovarianceRowRankOneSum (P := P) A) + (sampleCovarianceTailTheta (m := m) R t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) R)))) + (hR : 0 < R) + (ht : 0 < t) + (hTropp : + troppMasterTraceMGFFiniteFamily_statement + (P := P) + (centeredSampleCovarianceRowRankOneFamily (P := P) A) + (bernsteinSecondMomentComparisonFamily P + (centeredSampleCovarianceRowRankOneFamily (P := P) A) + (sampleCovarianceTailTheta (m := m) R t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) R)) + (sampleCovarianceCenteredRankOneRadius R)) + (matrixVarianceProxy P + (centeredSampleCovarianceRowRankOneFamily (P := P) A)) + (sampleCovarianceTailTheta (m := m) R t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) R)) + (sampleCovarianceCenteredRankOneRadius R)) + (hExpIntNeg : + forall k : Fin m, + IntegrableRandomMatrix P + (matrixExpScaledFamily + (centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A) + (sampleCovarianceTailTheta (m := m) Rneg t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) Rneg)) + k)) + (hTraceIntNeg : + IntegrableRealRandomVariable P + (traceExpIntegrand + (centeredSampleCovarianceRowRankOneSumNeg (P := P) A) + (sampleCovarianceTailTheta (m := m) Rneg t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) Rneg)))) + (hRNeg : 0 < Rneg) + (hTroppNeg : + troppMasterTraceMGFFiniteFamily_statement + (P := P) + (centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A) + (bernsteinSecondMomentComparisonFamily P + (centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A) + (sampleCovarianceTailTheta (m := m) Rneg t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) Rneg)) + (sampleCovarianceCenteredRankOneRadius Rneg)) + (matrixVarianceProxy P + (centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A)) + (sampleCovarianceTailTheta (m := m) Rneg t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) Rneg)) + (sampleCovarianceCenteredRankOneRadius Rneg)) : + P (SelfAdjointOperatorNormTailEvent + (centeredRandomMatrix P (sampleCovariance A)) t) <= + sampleCovarianceQuadraticFormTailRHS + (m := m) (n := n) R t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) R) + + sampleCovarianceQuadraticFormTailRHS + (m := m) (n := n) Rneg t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) Rneg) := by + exact + sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters + (P := P) (A := A) (R := R) (Rneg := Rneg) (t := t) + hm hMeas hLp hSq hSqNeg hIndep hIntSq hExpInt hTraceInt hR ht + (fun k omega => + bernsteinMatrixExp_le_quadratic + ((centeredSampleCovarianceRowRankOneFamily (P := P) A) k omega) + (sampleCovarianceTailTheta (m := m) R t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) R)) + (sampleCovarianceCenteredRankOneRadius R)) + hTropp hExpIntNeg hTraceIntNeg hRNeg + (fun k omega => + bernsteinMatrixExp_le_quadratic + ((centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A) k omega) + (sampleCovarianceTailTheta (m := m) Rneg t + (sampleCovarianceCenteredRankOneVarianceProxyBound (m := m) Rneg)) + (sampleCovarianceCenteredRankOneRadius Rneg)) + hTroppNeg + abbrev matrixBernsteinTraceMGFToLaplaceContract_statement {Omega : Type*} [MeasurableSpace Omega] {I : Type*} [Fintype I] {n : Nat} (P : Measure Omega) (A : I -> RandomMatrix Omega n n) (theta t R : Real) : Prop := diff --git a/HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean b/HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean index aa7c638..bb33201 100644 --- a/HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean +++ b/HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean @@ -41,14 +41,18 @@ open HighDimProb #check HighDimProb.sampleCovarianceTailThetaOfRows #check HighDimProb.sampleCovarianceQuadraticFormTailRHS #check HighDimProb.sampleCovariance_quadraticForm_tail_optimized_under_explicit_variance_proxy +#check HighDimProb.sampleCovariance_quadraticForm_tail_optimized_under_explicit_variance_proxy_of_troppPrimitive #check HighDimProb.sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound +#check HighDimProb.sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound_of_troppPrimitive #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 #check HighDimProb.sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_explicit_variance_proxy #check HighDimProb.sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound #check HighDimProb.sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_adapters +#check HighDimProb.sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_adapters_of_troppPrimitives #check HighDimProb.sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters +#check HighDimProb.sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives #check HighDimProb.negRandomMatrixFamily #check HighDimProb.matrixExpScaledFamily_negRandomMatrixFamily #check HighDimProb.integrableRandomMatrix_matrixExpScaledFamily_negRandomMatrixFamily diff --git a/HighDimProbTest/ExamplesAPI.lean b/HighDimProbTest/ExamplesAPI.lean index d1ed91f..4dc8981 100644 --- a/HighDimProbTest/ExamplesAPI.lean +++ b/HighDimProbTest/ExamplesAPI.lean @@ -54,10 +54,12 @@ variable (kernelHExplicitPSD : IsPSDMatrix kernelA) #check sampleCovarianceQuadraticFormTailRHS #check SampleCovarianceTailAssumptions #check sampleCovariance_quadraticForm_tail_usage +#check sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound_of_troppPrimitive #check centeredSampleCovarianceRowRankOneFamilyNeg #check centeredSampleCovarianceRowRankOneSumNeg #check SampleCovarianceOperatorNormTailAssumptions #check sampleCovariance_operatorNorm_tail_usage +#check sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives #check AttentionFeatureGramTailAssumptions #check attentionFeatureGram_quadraticForm_tail_usage #check attentionFeatureGram_operatorNorm_tail_usage diff --git a/HighDimProbTest/RandomMatrixConcentrationAPI.lean b/HighDimProbTest/RandomMatrixConcentrationAPI.lean index ac895b5..c23fb69 100644 --- a/HighDimProbTest/RandomMatrixConcentrationAPI.lean +++ b/HighDimProbTest/RandomMatrixConcentrationAPI.lean @@ -155,13 +155,17 @@ variable (R theta sigma2 c c1 c2 t bound K : Real) #check sampleCovarianceTailThetaOfRows #check sampleCovarianceQuadraticFormTailRHS #check sampleCovariance_quadraticForm_tail_optimized_under_explicit_variance_proxy +#check sampleCovariance_quadraticForm_tail_optimized_under_explicit_variance_proxy_of_troppPrimitive #check sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound +#check sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound_of_troppPrimitive #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 #check sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound #check sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_adapters +#check sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_adapters_of_troppPrimitives #check sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters +#check sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives #check centeredSampleCovarianceRowRankOneFamilyNeg #check centeredSampleCovarianceRowRankOneSumNeg #check isRandomMatrix_negRandomMatrixFamily diff --git a/docs/AssumptionVocabulary.md b/docs/AssumptionVocabulary.md index 214d566..410ff67 100644 --- a/docs/AssumptionVocabulary.md +++ b/docs/AssumptionVocabulary.md @@ -80,10 +80,10 @@ remain in the object modules such as `Basic`, `Expectation`, `SelfAdjoint`, and dimension/rank targets; the Bernstein CFC primitive is now proved as `bernsteinMatrixExp_le_quadratic`. The generic optimized Matrix Bernstein surface now has Tropp-only - positive/negative bundles that no longer expose pointwise CFC fields. The - next RandomMatrix hardbone branch is - `RM-HB-sample-covariance-cfc-free-wrapper-contract`; natural-state assumption - bundling and negative trace-MGF provider-wrapper cleanup remain future side - leaves. + positive/negative bundles, and the sample-covariance route has CFC-free + Tropp-only wrappers, so preferred call sites no longer expose pointwise CFC + fields. The next RandomMatrix hardbone branch is + `RM-HB12-select-next-hardbone-proof-leaf`; natural-state assumption bundling + and negative trace-MGF provider-wrapper cleanup remain future side leaves. - Scalar concentration can continue toward moment/MGF links without depending on the matrix assumption layer. diff --git a/docs/JudgeSystem.md b/docs/JudgeSystem.md index b626f27..2851c9b 100644 --- a/docs/JudgeSystem.md +++ b/docs/JudgeSystem.md @@ -332,12 +332,11 @@ python scripts/judge_policy_check.py self-adjoint/centered-self-adjoint structure, independence, and pointwise operator-norm bounds. - The same judge file checks the sample-covariance negative row-rank-one - adapters and - `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_adapters`, - the square-negation adapter declarations, - `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters`, - and the opposite-parameter sample-covariance exp/trace/CFC - provider-transfer adapters. + 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. - The checks are import-boundary/API checks only; they do not prove - exponential/trace integrability, Tropp/Lieb, Bernstein CFC, Golden-Thompson, - full Matrix Bernstein, or unconditional sample-covariance concentration. + exponential/trace integrability, Tropp/Lieb, Golden-Thompson, full Matrix + Bernstein, or unconditional sample-covariance concentration. The CFC-free + wrappers only reuse the proved `bernsteinMatrixExp_le_quadratic` leaf. diff --git a/docs/RandomMatrixAPI.md b/docs/RandomMatrixAPI.md index f917e57..f0bcfd9 100644 --- a/docs/RandomMatrixAPI.md +++ b/docs/RandomMatrixAPI.md @@ -191,6 +191,8 @@ import HighDimProb.Examples.RandomMatrix.HardboneStatementAtlasUsage ## Sample Covariance Surface +Explicit-CFC compatibility wrappers: + - `sampleCovariance_quadraticForm_tail_optimized_under_explicit_variance_proxy` - `sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound` - `sampleCovariance_selfAdjointOperatorNormTailEvent_subset_centeredRowRankOneSum` @@ -200,6 +202,20 @@ import HighDimProb.Examples.RandomMatrix.HardboneStatementAtlasUsage - `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_square_adapters` +Preferred CFC-free wrappers after the Bernstein CFC hardbone leaf: + +- `sampleCovariance_quadraticForm_tail_optimized_under_explicit_variance_proxy_of_troppPrimitive` +- `sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound_of_troppPrimitive` +- `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_adapters_of_troppPrimitives` +- `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives` + +These wrappers still require Tropp/Lieb trace-MGF primitives and analytic +integrability assumptions. They only remove the user-supplied pointwise +Bernstein CFC fields by applying `bernsteinMatrixExp_le_quadratic`; they do not +prove Tropp/Lieb, Golden-Thompson, trace-exp integrability, variance-proxy +control beyond existing named adapters, or unconditional sample-covariance +concentration. + ### Sample covariance negative-side provider adapters - `centeredSampleCovarianceRowRankOneFamilyNeg_expIntegrable_of_expIntegrable_neg_theta` @@ -222,6 +238,8 @@ and they are not tail wrappers by themselves. - Name matrix families before using them in public wrappers. - 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. - 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 3c6a26c..ab5c807 100644 --- a/docs/Status.md +++ b/docs/Status.md @@ -59,10 +59,15 @@ TraceExp / Tropp bookkeeping helpers: Sample covariance wrappers: +- `sampleCovariance_quadraticForm_tail_optimized_under_explicit_variance_proxy` +- `sampleCovariance_quadraticForm_tail_optimized_under_explicit_variance_proxy_of_troppPrimitive` - `sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound` +- `sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound_of_troppPrimitive` - `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` - `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters` +- `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives` - `SampleCovarianceTailUsage.SampleCovarianceTailAssumptions` - `SampleCovarianceTailUsage.SampleCovarianceOperatorNormTailAssumptions` @@ -124,11 +129,12 @@ Example modules: hypotheses. - The conditional-state bundle is example-local, and the reindexed example is transport-only. - 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. +- Sample covariance wrappers remain conditional APIs, not unconditional concentration theorems. 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. - 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. -- Next safe hardbone task: `RM-HB-sample-covariance-cfc-free-wrapper-contract`. +- Completed hardbone wrapper task: `RM-HB-sample-covariance-cfc-free-wrapper-contract`. +- Next safe hardbone task: `RM-HB12-select-next-hardbone-proof-leaf`. ## Verification diff --git a/docs/TODO.md b/docs/TODO.md index 851cce1..7f04f70 100644 --- a/docs/TODO.md +++ b/docs/TODO.md @@ -5,14 +5,15 @@ This is the active short list. Old completed task logs were collapsed into ## Active RandomMatrix Work -- Audit remaining explicit CFC fields in the sample-covariance route. Reuse - `bernsteinMatrixExp_le_quadratic` and the new Tropp-only Matrix Bernstein - bundles before adding any new fields. +- Select the next smallest theorem-backed hardbone proof leaf with a read-only + Mathlib/API audit before editing Lean. - 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. -- Next RandomMatrix hardbone task: +- Completed RandomMatrix hardbone wrapper task: `RM-HB-sample-covariance-cfc-free-wrapper-contract`. +- Next RandomMatrix hardbone task: + `RM-HB12-select-next-hardbone-proof-leaf`. ## Active Documentation Work diff --git a/docs/TestPlan.md b/docs/TestPlan.md index 9105339..9d51701 100644 --- a/docs/TestPlan.md +++ b/docs/TestPlan.md @@ -38,8 +38,10 @@ git diff --check `HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean`, `HighDimProbJudge/RandomMatrix/TraceExpUse.lean`, and the `HardboneStatementAtlasUsage` example. -- RandomMatrix sample-covariance negative-side provider-transfer adapters are - covered in `HighDimProbTest/RandomMatrixConcentrationAPI.lean` and +- RandomMatrix sample-covariance negative-side provider-transfer adapters and + CFC-free sample-covariance wrappers are covered in + `HighDimProbTest/RandomMatrixConcentrationAPI.lean`, + `HighDimProbTest/ExamplesAPI.lean`, and `HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean`. - RandomMatrix CFC-free Matrix Bernstein assumption bundles and preferred `*_of_troppAssumptions` wrappers are covered in diff --git a/docs/TheoremAtlas.md b/docs/TheoremAtlas.md index 1648ef1..5f1dc87 100644 --- a/docs/TheoremAtlas.md +++ b/docs/TheoremAtlas.md @@ -46,15 +46,16 @@ that CFC proof while keeping Tropp/Lieb and integrability assumptions explicit. The preferred optimized Matrix Bernstein wrappers use `MatrixBernsteinPositiveSideTroppAssumptions` and `MatrixBernsteinNegativeSideTroppAssumptions` to avoid exposing pointwise CFC -fields in generic call sites. +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. ## Not Yet Proved - Full Tropp/Lieb machinery. - Golden-Thompson route. - Full unconditional Matrix Bernstein theorem. -- Tropp-only sample-covariance wrappers without explicit sample-covariance CFC - fields. - 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,