From 8839ff3ed852565a32bafbabe127f76e6eac6c51 Mon Sep 17 00:00:00 2001 From: HighDimProb Dev Date: Sat, 20 Jun 2026 05:30:35 +0000 Subject: [PATCH 1/2] Bridge exact-row variance proxies to centered-square chains Add a narrow hardbone bridge that lets exact-row sample-covariance variance-proxy consumers depend on the generic centered-square chain while preserving explicit Tropp/Lieb and Matrix Bernstein boundaries. Constraint: Keep theorem boundaries honest; generic centered-square chain and Tropp/Lieb primitives remain explicit. Rejected: Proving a full hardbone sharp-chain or Matrix Bernstein theorem | would broaden the verified contract beyond available leaves. Confidence: high Scope-risk: moderate Directive: Do not treat these wrappers as unconditional concentration theorems; downstream wrappers must keep missing analytic primitives explicit. Tested: lake env lean HighDimProb/RandomMatrix/HardboneStatements.lean; lake build HighDimProb.RandomMatrix.HardboneStatements; API/judge focused checks; python .github/scripts/check_text_quality.py; python scripts/judge_policy_check.py; git diff --check; lake build HighDimProbJudge; lake test; lake build Not-tested: GitHub Actions after PR creation --- .../RandomMatrix/ConcentrationStatements.lean | 268 ++++++++++++++++++ .../RandomMatrix/HardboneStatements.lean | 93 ++++++ .../RandomMatrix/MatrixBernsteinUse.lean | 2 + .../RandomMatrix/TraceExpUse.lean | 2 + .../RandomMatrix/VarianceProxyUse.lean | 2 + .../RandomMatrixConcentrationAPI.lean | 2 + .../RandomMatrixHardboneStatementsAPI.lean | 2 + docs/JudgeSystem.md | 9 +- docs/LeafPlan.md | 28 +- docs/RandomMatrixAPI.md | 20 +- docs/Status.md | 43 ++- docs/TODO.md | 10 +- docs/TestPlan.md | 8 +- docs/TheoremAtlas.md | 4 +- 14 files changed, 465 insertions(+), 28 deletions(-) diff --git a/HighDimProb/RandomMatrix/ConcentrationStatements.lean b/HighDimProb/RandomMatrix/ConcentrationStatements.lean index 43bbbdb..4e019fb 100644 --- a/HighDimProb/RandomMatrix/ConcentrationStatements.lean +++ b/HighDimProb/RandomMatrix/ConcentrationStatements.lean @@ -2388,6 +2388,57 @@ theorem MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamily_of centeredRankOneVarianceProxyNormRHS, pointwiseOperatorNormVarianceProxyNormRHS] using hGeneric +/-- Negative sample-covariance row-rank-one variance-proxy norm bound from +row-specific squared-norm bounds. + +This is the negative-side exact-row provider for sample-covariance routes. It +does not prove a new sharp-variance chain: it reuses the positive exact-row +hardbone consumer and the algebraic fact that pointwise negation preserves the +matrix variance proxy. -/ +theorem MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two + {Omega : Type*} [MeasurableSpace Omega] {P : Measure Omega} + [IsProbabilityMeasure P] {m n : Nat} + (A : RandomMatrix Omega m n) + (R : Fin m -> Real) + (hChain : + sampleCovarianceVarianceProxy_sharp_statement (P := P) (X := rowVector A) + (fun i => matrixSecondMoment P (rankOneRandomMatrix (rowVector A i))) + (rowSqNormVarianceProxyNormRHS R)) + (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 k) + (hR : forall k : Fin m, 0 <= R k) : + MatrixVarianceProxyNormBound P + (centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A) + (rowSqNormVarianceProxyNormRHS R) := by + have hRowsLp : + forall k : Fin m, forall j : Fin n, + MemLpRealRandomVariable P (coord (rowVector A k) j) 2 := by + intro k j + change MemLpRealRandomVariable P (matrixEntry A k j) 2 + exact hLp k j + have hPos : + MatrixVarianceProxyNormBound P + (centeredSampleCovarianceRowRankOneFamily (P := P) A) + (rowSqNormVarianceProxyNormRHS R) := by + change MatrixVarianceProxyNormBound P + (centeredRankOneRandomMatrixFamily P (rowVector A)) + (rowSqNormVarianceProxyNormRHS R) + exact + sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two + (P := P) (X := rowVector A) (R := R) + hChain hRowsLp hSq hR + change + matrixVarianceProxyNorm P + (negRandomMatrixFamily + (centeredSampleCovarianceRowRankOneFamily (P := P) A)) <= + rowSqNormVarianceProxyNormRHS R + rw [matrixVarianceProxyNorm, matrixVarianceProxy_negRandomMatrixFamily] + simpa [MatrixVarianceProxyNormBound, matrixVarianceProxyNorm] using hPos + /-- Sample covariance quadratic-form upper-tail wrapper under explicit Matrix Bernstein primitive assumptions. @@ -3526,6 +3577,223 @@ theorem sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos hExpIntNeg hTraceIntNeg hBoundNeg hSigmaNeg hRNeg hNormNeg hCFCNeg hTroppNeg +/-- Sample-covariance self-adjoint operator-norm tail wrapper using exact-row +variance proxies on both signs. + +This is a CFC-free exact-row integration wrapper. It uses uniform row +squared-norm radii `R` and `Rneg` for the Bernstein radii, and row-specific +radius families `Rvar` and `RvarNeg` for the positive and negative variance +proxy RHS values. The two hardbone sharp-variance chain premises, +sign-specific exp/trace integrability, independence, and finite-family +Tropp/Lieb primitives remain explicit. -/ +theorem sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_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) + (Rvar RvarNeg : Fin m -> 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) + (hSqVar : + forall k : Fin m, forall omega, + vectorSqNorm (rowVector A k omega) <= Rvar k) + (hSqVarNeg : + forall k : Fin m, forall omega, + vectorSqNorm (rowVector A k omega) <= RvarNeg k) + (hIndep : + IndependentRandomMatrices P + (centeredSampleCovarianceRowRankOneFamily (P := P) A)) + (hExpInt : + forall k : Fin m, + IntegrableRandomMatrix P + (matrixExpScaledFamily + (centeredSampleCovarianceRowRankOneFamily (P := P) A) + (sampleCovarianceTailTheta (m := m) R t + (rowSqNormVarianceProxyNormRHS Rvar)) + k)) + (hTraceInt : + IntegrableRealRandomVariable P + (traceExpIntegrand + (centeredSampleCovarianceRowRankOneSum (P := P) A) + (sampleCovarianceTailTheta (m := m) R t + (rowSqNormVarianceProxyNormRHS Rvar)))) + (hSigma : 0 < rowSqNormVarianceProxyNormRHS Rvar) + (hR : 0 <= R) + (hRvar : forall i : Fin m, 0 <= Rvar i) + (ht : 0 < t) + (hChain : + sampleCovarianceVarianceProxy_sharp_statement (P := P) (X := rowVector A) + (fun i => matrixSecondMoment P (rankOneRandomMatrix (rowVector A i))) + (rowSqNormVarianceProxyNormRHS Rvar)) + (hTropp : + 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)) + (hExpIntNeg : + forall k : Fin m, + IntegrableRandomMatrix P + (matrixExpScaledFamily + (centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A) + (sampleCovarianceTailTheta (m := m) Rneg t + (rowSqNormVarianceProxyNormRHS RvarNeg)) + k)) + (hTraceIntNeg : + IntegrableRealRandomVariable P + (traceExpIntegrand + (centeredSampleCovarianceRowRankOneSumNeg (P := P) A) + (sampleCovarianceTailTheta (m := m) Rneg t + (rowSqNormVarianceProxyNormRHS RvarNeg)))) + (hSigmaNeg : 0 < rowSqNormVarianceProxyNormRHS RvarNeg) + (hRNeg : 0 <= Rneg) + (hRvarNeg : forall i : Fin m, 0 <= RvarNeg i) + (hChainNeg : + sampleCovarianceVarianceProxy_sharp_statement (P := P) (X := rowVector A) + (fun i => matrixSecondMoment P (rankOneRandomMatrix (rowVector A i))) + (rowSqNormVarianceProxyNormRHS RvarNeg)) + (hTroppNeg : + 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)) : + 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 + have hRowsRandom : + forall k : Fin m, IsRandomVector P (rowVector A k) := by + intro k + exact isRandomVector_rowVector hMeas k + have hRowsLp : + forall k : Fin m, forall j : Fin n, + MemLpRealRandomVariable P (coord (rowVector A k) j) 2 := by + intro k j + change MemLpRealRandomVariable P (matrixEntry A k j) 2 + exact hLp k j + have hCentered : + CenteredSelfAdjointRandomMatrixFamily P + (centeredSampleCovarianceRowRankOneFamily (P := P) A) := by + simpa [centeredSampleCovarianceRowRankOneFamily] using + centeredRankOneRandomMatrix_centeredSelfAdjoint_of_memLp_two + (P := P) (X := rowVector A) hRowsRandom hRowsLp + have hIndepSA : + IndependentSelfAdjointRandomMatrices P + (centeredSampleCovarianceRowRankOneFamily (P := P) A) := + ⟨hCentered.1, hIndep⟩ + have hCenteredNeg : + CenteredSelfAdjointRandomMatrixFamily P + (centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A) := by + simpa [centeredSampleCovarianceRowRankOneFamilyNeg] using + centeredSelfAdjointRandomMatrixFamily_negRandomMatrixFamily + (P := P) (A := centeredSampleCovarianceRowRankOneFamily (P := P) A) + hCentered + have hIndepSANeg : + IndependentSelfAdjointRandomMatrices P + (centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A) := by + simpa [centeredSampleCovarianceRowRankOneFamilyNeg] using + independentSelfAdjointRandomMatrices_negRandomMatrixFamily + (P := P) (A := centeredSampleCovarianceRowRankOneFamily (P := P) A) + hIndepSA + have hIntXNeg : + forall k : Fin m, + IntegrableRandomMatrix P + ((centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A) k) := + centeredSampleCovarianceRowRankOneFamilyNeg_integrable_of_memLp_two + (P := P) (A := A) hLp + have hIntSq : + forall k : Fin m, + IntegrableRandomMatrix P + (randomMatrixSquare + ((centeredSampleCovarianceRowRankOneFamily (P := P) A) k)) := by + intro k + change IntegrableRandomMatrix P + (randomMatrixSquare ((centeredRankOneRandomMatrixFamily P (rowVector A)) k)) + exact + integrableRandomMatrix_randomMatrixSquare_centeredRankOneRandomMatrixFamily_of_sqNorm_bound_memLp_two + (P := P) (X := rowVector A) (R := R) hRowsLp hSq k + have hIntSqNeg : + forall k : Fin m, + IntegrableRandomMatrix P + (randomMatrixSquare + ((centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A) k)) := + centeredSampleCovarianceRowRankOneFamilyNeg_squareIntegrable_of_squareIntegrable + (P := P) (A := A) hIntSq + have hBoundNeg : + PointwiseOperatorNormBound + (centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A) + (sampleCovarianceCenteredRankOneRadius Rneg) := + PointwiseOperatorNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_rowSqNorm_bound + (P := P) A hMeas hLp hSqNeg hRNeg + have hNorm : + MatrixVarianceProxyNormBound P + (centeredSampleCovarianceRowRankOneFamily (P := P) A) + (rowSqNormVarianceProxyNormRHS Rvar) := by + change MatrixVarianceProxyNormBound P + (centeredRankOneRandomMatrixFamily P (rowVector A)) + (rowSqNormVarianceProxyNormRHS Rvar) + exact + sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two + (P := P) (X := rowVector A) (R := Rvar) + hChain hRowsLp hSqVar hRvar + have hNormNeg : + MatrixVarianceProxyNormBound P + (centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A) + (rowSqNormVarianceProxyNormRHS RvarNeg) := + MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two + (P := P) A RvarNeg hChainNeg hLp hSqVarNeg hRvarNeg + exact + sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_explicit_variance_proxy + (P := P) (A := A) (R := R) (Rneg := Rneg) (t := t) + (sigmaSq := rowSqNormVarianceProxyNormRHS Rvar) + (sigmaSqNeg := rowSqNormVarianceProxyNormRHS RvarNeg) + 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 + (rowSqNormVarianceProxyNormRHS Rvar)) + (sampleCovarianceCenteredRankOneRadius R)) + hTropp hCenteredNeg hIndepSANeg hIntXNeg hIntSqNeg hExpIntNeg + hTraceIntNeg hBoundNeg hSigmaNeg hRNeg hNormNeg + (fun k omega => + bernsteinMatrixExp_le_quadratic + ((centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A) k omega) + (sampleCovarianceTailTheta (m := m) Rneg t + (rowSqNormVarianceProxyNormRHS RvarNeg)) + (sampleCovarianceCenteredRankOneRadius Rneg)) + hTroppNeg + /-- Arbitrary-column sample-covariance self-adjoint operator-norm tail wrapper using crude bounded-row variance-proxy norm bounds. diff --git a/HighDimProb/RandomMatrix/HardboneStatements.lean b/HighDimProb/RandomMatrix/HardboneStatements.lean index 07bd4a2..358b640 100644 --- a/HighDimProb/RandomMatrix/HardboneStatements.lean +++ b/HighDimProb/RandomMatrix/HardboneStatements.lean @@ -616,6 +616,7 @@ theorem sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_sqNorm_bound_memLp_two (P := P) (X := X i) (R := R i) (hLp i) (hSq i)) hSq hR) + /-- Generic provider-chain target from centered-square comparisons to a variance-proxy norm bound. @@ -686,6 +687,98 @@ theorem varianceProxyNormBound_of_centeredSquareChain_expansion hChain (fun i => matrixSquare_centeredRandomMatrix_expectation_expansion (P := P) (A i)) hLE hNorm +/-- Exact-row sample-covariance sharp-chain statement provider from the generic +centered-square variance-proxy chain. + +This bridges the generic `varianceProxyNormBound_of_centeredSquareChain_statement` +for the rank-one row family to the sample-covariance-specific +`sampleCovarianceVarianceProxy_sharp_statement`. The concrete row assumptions +only discharge the integrability premises needed by the centered rank-one +second-moment comparison. The generic centered-square chain remains explicit; +this theorem does not prove Matrix Bernstein, Tropp/Lieb, trace-MGF iteration, +or an unconditional sample-covariance tail bound. -/ +theorem sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two + {Omega : Type*} [mOmega : MeasurableSpace Omega] + {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] + {m n : Nat} + (X : Fin m -> RandomVector Omega n) + (R : Fin m -> Real) + (hChain : @varianceProxyNormBound_of_centeredSquareChain_statement + Omega mOmega P _ (Fin m) _ n (rankOneRandomMatrixFamily X) + (fun i => matrixSecondMoment P (rankOneRandomMatrix (X i))) + (rowSqNormVarianceProxyNormRHS R)) + (hMeas : forall i, IsRandomVector P (X i)) + (hLp : forall i, forall j : Fin n, + MemLpRealRandomVariable P (coord (X i) j) 2) + (hSq : forall i omega, vectorSqNorm (X i omega) <= R i) : + @sampleCovarianceVarianceProxy_sharp_statement + Omega mOmega P _ m n X + (fun i => matrixSecondMoment P (rankOneRandomMatrix (X i))) + (rowSqNormVarianceProxyNormRHS R) := by + intro hCentered hSecond hNorm + have hResult : MatrixVarianceProxyNormBound P + (centeredRandomMatrixFamily P (rankOneRandomMatrixFamily X)) + (rowSqNormVarianceProxyNormRHS R) := by + apply hChain + · intro i + exact matrixSquare_centeredRandomMatrix_expectation_expansion + (P := P) ((rankOneRandomMatrixFamily X) i) + · intro i + have hRankSq : IntegrableRandomMatrix P + (randomMatrixSquare (rankOneRandomMatrix (X i))) := + integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_sqNorm_bound_memLp_two + (P := P) (X := X i) (R := R i) (hLp i) (hSq i) + have hRankInt : IntegrableRandomMatrix P (rankOneRandomMatrix (X i)) := + integrableRandomMatrix_rankOneRandomMatrix_of_memLp_two + (P := P) (X := X i) (hLp i) + have hCenteredSq : IntegrableRandomMatrix P + (randomMatrixSquare (centeredRankOneRandomMatrix P (X i))) := by + simpa [centeredRankOneRandomMatrix] using + integrableRandomMatrix_randomMatrixSquare_centeredRandomMatrix + (P := P) (A := rankOneRandomMatrix (X i)) hRankInt hRankSq + have hCenteredLE : MatrixLE + (matrixSecondMoment P (centeredRankOneRandomMatrix P (X i))) + (matrixSecondMoment P (rankOneRandomMatrix (X i))) := + hCentered i (hMeas i) (hLp i) hCenteredSq hRankSq + have hLE : MatrixLE + (matrixSecondMoment P (centeredRankOneRandomMatrix P (X i))) + (matrixSecondMoment P (rankOneRandomMatrix (X i))) := hCenteredLE + simpa [rankOneRandomMatrixFamily, centeredRankOneRandomMatrix] using + matrixLE_trans hLE (hSecond i) + · simpa [rankOneRandomMatrixFamily] using hNorm + simpa [centeredRankOneRandomMatrixFamily] using hResult + +/-- Exact-row sample-covariance variance-proxy consumer from the generic +centered-square chain. + +Compared with `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two`, +this theorem replaces the sample-specific sharp-chain premise by the generic +centered-square chain plus concrete row measurability, `MemLp 2`, and exact row +squared-norm witnesses. The row-specific deterministic norm control remains the +existing `rowSqNormVarianceProxyNormRHS R` route. -/ +theorem sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two_of_centeredSquareChain + {Omega : Type*} [mOmega : MeasurableSpace Omega] + {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] + {m n : Nat} + (X : Fin m -> RandomVector Omega n) + (R : Fin m -> Real) + (hChain : @varianceProxyNormBound_of_centeredSquareChain_statement + Omega mOmega P _ (Fin m) _ n (rankOneRandomMatrixFamily X) + (fun i => matrixSecondMoment P (rankOneRandomMatrix (X i))) + (rowSqNormVarianceProxyNormRHS R)) + (hMeas : forall i, IsRandomVector P (X i)) + (hLp : forall i, forall j : Fin n, + MemLpRealRandomVariable P (coord (X i) j) 2) + (hSq : forall i omega, vectorSqNorm (X i omega) <= R i) + (hR : forall i, 0 <= R i) : + MatrixVarianceProxyNormBound P + (centeredRankOneRandomMatrixFamily P X) + (rowSqNormVarianceProxyNormRHS R) := + sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two + (P := P) X R + (sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two + (P := P) X R hChain hMeas hLp hSq) + hLp hSq hR /-! ## Dimension, support, and effective-rank hardbone statement chain -/ /-- Rank-refined trace-exponential dimension-factor target with an explicit diff --git a/HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean b/HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean index 0586a92..bb923d6 100644 --- a/HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean +++ b/HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean @@ -54,6 +54,7 @@ open HighDimProb #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.sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives #check HighDimProb.negRandomMatrixFamily #check HighDimProb.matrixExpScaledFamily_negRandomMatrixFamily #check HighDimProb.integrableRandomMatrix_matrixExpScaledFamily_negRandomMatrixFamily @@ -84,6 +85,7 @@ open HighDimProb #check HighDimProb.centeredSampleCovarianceRowRankOneFamilyNeg_expIntegrable_of_expIntegrable_neg_theta #check HighDimProb.centeredSampleCovarianceRowRankOneSumNeg_traceExpIntegrable_of_traceExpIntegrable_neg_theta #check HighDimProb.centeredSampleCovarianceRowRankOneFamilyNeg_cfcPrimitive_of_cfcPrimitive_neg_theta +#check HighDimProb.MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two #check HighDimProb.matrixVarianceProxyNorm #check HighDimProb.PointwiseOperatorNormBound #check HighDimProb.IndependentSelfAdjointRandomMatrices diff --git a/HighDimProbJudge/RandomMatrix/TraceExpUse.lean b/HighDimProbJudge/RandomMatrix/TraceExpUse.lean index 40ca65f..ad5127a 100644 --- a/HighDimProbJudge/RandomMatrix/TraceExpUse.lean +++ b/HighDimProbJudge/RandomMatrix/TraceExpUse.lean @@ -124,6 +124,8 @@ open scoped MatrixOrder Matrix.Norms.Operator #check HighDimProb.sampleCovarianceVarianceProxy_sharp_statement #check HighDimProb.sampleCovarianceVarianceProxy_sharp_of_rankOneSecondMoment #check HighDimProb.sampleCovarianceVarianceProxy_sharp_of_exactRowSecondMoment +#check HighDimProb.sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two +#check HighDimProb.sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two_of_centeredSquareChain #check HighDimProb.varianceProxyNormBound_of_centeredSquareChain_statement #check HighDimProb.varianceProxyNormBound_of_centeredSquareChain #check HighDimProb.varianceProxyNormBound_of_centeredSquareChain_expansion diff --git a/HighDimProbJudge/RandomMatrix/VarianceProxyUse.lean b/HighDimProbJudge/RandomMatrix/VarianceProxyUse.lean index 8ebb9f4..fe83432 100644 --- a/HighDimProbJudge/RandomMatrix/VarianceProxyUse.lean +++ b/HighDimProbJudge/RandomMatrix/VarianceProxyUse.lean @@ -40,6 +40,8 @@ import HighDimProb.RandomMatrix #check HighDimProb.MatrixVarianceProxyNormBound_centeredRankOneRandomMatrixFamily_of_sqNorm_bound #check HighDimProb.MatrixVarianceProxyNormBound_centeredRankOneRandomMatrixFamily_of_sqNorm_bound_memLp_two #check HighDimProb.sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two +#check HighDimProb.sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two +#check HighDimProb.sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two_of_centeredSquareChain #check HighDimProb.matrixQuadraticForm_sum #check HighDimProb.matrixQuadraticForm_add #check HighDimProb.matrixQuadraticForm_smul diff --git a/HighDimProbTest/RandomMatrixConcentrationAPI.lean b/HighDimProbTest/RandomMatrixConcentrationAPI.lean index fe228a5..1d3f681 100644 --- a/HighDimProbTest/RandomMatrixConcentrationAPI.lean +++ b/HighDimProbTest/RandomMatrixConcentrationAPI.lean @@ -167,6 +167,7 @@ variable (R theta sigma2 c c1 c2 t bound K : Real) #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 sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives #check centeredSampleCovarianceRowRankOneFamilyNeg #check centeredSampleCovarianceRowRankOneSumNeg #check isRandomMatrix_negRandomMatrixFamily @@ -185,6 +186,7 @@ variable (R theta sigma2 c c1 c2 t bound K : Real) #check centeredSampleCovarianceRowRankOneFamilyNeg_expIntegrable_of_expIntegrable_neg_theta #check centeredSampleCovarianceRowRankOneSumNeg_traceExpIntegrable_of_traceExpIntegrable_neg_theta #check centeredSampleCovarianceRowRankOneFamilyNeg_cfcPrimitive_of_cfcPrimitive_neg_theta +#check MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two #check operatorNorm_eq_spectralRadius_of_selfAdjointStatement #check HighProbabilityBound #check highProbabilityBound diff --git a/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean b/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean index 0f000f6..f3cf618 100644 --- a/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean +++ b/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean @@ -51,6 +51,8 @@ variable (mHist : Fin m -> MeasurableSpace Omega) #check sampleCovarianceVarianceProxy_sharp_of_rankOneSecondMoment #check sampleCovarianceVarianceProxy_sharp_of_exactRowSecondMoment #check sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two +#check sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two +#check sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two_of_centeredSquareChain #check varianceProxyNormBound_of_centeredSquareChain_statement #check traceMatrixExp_le_rank_exp_lambdaMax_statement #check traceMatrixExp_le_supportDim_exp_lambdaMax_statement diff --git a/docs/JudgeSystem.md b/docs/JudgeSystem.md index f116c25..42628b7 100644 --- a/docs/JudgeSystem.md +++ b/docs/JudgeSystem.md @@ -52,9 +52,9 @@ theorems or typed statements without relying on local test internals. PSD and quadratic-form nonnegativity APIs. - `HighDimProbJudge/RandomMatrix/VarianceProxyUse.lean`: matrix square, second moment, variance proxy, semantic variance-proxy bounds, - variance-proxy norm, self-adjointness lemmas, matrix expectation PSD/order - and add/smul/zero/constant normalization lemmas, PSD typed targets, and - matrix Bernstein statement surface. + variance-proxy norm, self-adjointness lemmas, exact-row generic-centered-square + chain bridge visibility, matrix expectation PSD/order and add/smul/zero/constant + normalization lemmas, PSD typed targets, and matrix Bernstein statement surface. - `HighDimProbJudge/RandomMatrix/SpectralUse.lean`: lambda-max wrappers, ordered endpoint wrappers, quadratic-form bound predicates, monotonicity lemmas, two-sided tail events, and spectral tail event APIs. @@ -73,7 +73,8 @@ 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`, and its main structural/analytic + `matrixBernsteinTraceMGF_statement`, sample-covariance negative exact-row + variance-proxy provider visibility, and its main structural/analytic dependencies. ## How It Differs From Normal Tests diff --git a/docs/LeafPlan.md b/docs/LeafPlan.md index 473adfb..2ed577e 100644 --- a/docs/LeafPlan.md +++ b/docs/LeafPlan.md @@ -36,7 +36,7 @@ - Stage M-real-2: real-exponent `SubExponentialMoment` bridge - Stage SC-final-update: scalar closeout refreshed after both moment bridges - Current repository next task: - RM-VP-negative-exact-row-variance-proxy-provider-contract. Natural-state + RM-VP-centered-square-chain-wrapper-integration-contract. Natural-state assumption bundling, negative trace-MGF provider cleanup, Matrix Bernstein, Hanson-Wright, and WLLN/SLLN remain separate future directions. - OrliczToTail @@ -236,7 +236,31 @@ - Boundary preserved: this does not prove the hardbone sharp-chain provider, Tropp/Lieb, Golden-Thompson, Bernstein CFC, two-sided control, operator-norm control, or Matrix Bernstein. -- Next safe leaf: `RM-VP-negative-exact-row-variance-proxy-provider-contract`. +- Follow-up completed proof leaf: + `RM-VP-negative-exact-row-variance-proxy-provider-contract`, adding + `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two` + as the negative-side exact-row variance-proxy provider by transferring the + positive row-specific bound through `matrixVarianceProxy_negRandomMatrixFamily`. +- Boundary preserved: this does not prove two-sided/operator-norm wrapper + integration, concrete row-moment evaluation, Tropp/Lieb, Golden-Thompson, + Bernstein CFC, or Matrix Bernstein. +- Follow-up completed proof leaf: + `RM-VP-two-sided-operator-norm-exact-row-wrapper-integration-contract`, adding + `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives` as the CFC-free operator-norm wrapper over positive and negative + row-specific exact-row variance-proxy RHS values. +- Boundary preserved: this does not prove concrete row-moment evaluation, new + hardbone sharp-chain providers, Tropp/Lieb, Golden-Thompson, Bernstein CFC, + or Matrix Bernstein. +- Follow-up completed proof leaf: + `RM-VP-concrete-row-moment-evaluation-contract`, adding + `sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two` + and + `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two_of_centeredSquareChain` + as the exact-row bridge from the generic centered-square variance-proxy chain + to the sample-specific sharp-chain statement and consumer. +- Boundary preserved: this does not prove the generic centered-square chain, + Tropp/Lieb, Golden-Thompson, Bernstein CFC, or Matrix Bernstein. +- Next safe leaf: `RM-VP-centered-square-chain-wrapper-integration-contract`. ## Process diff --git a/docs/RandomMatrixAPI.md b/docs/RandomMatrixAPI.md index fac6b35..97446ea 100644 --- a/docs/RandomMatrixAPI.md +++ b/docs/RandomMatrixAPI.md @@ -112,6 +112,9 @@ Variance-proxy / centered-square chain: - `sampleCovarianceVarianceProxy_sharp_of_rankOneSecondMoment` - `sampleCovarianceVarianceProxy_sharp_of_exactRowSecondMoment` - `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` +- `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two` - `varianceProxyNormBound_of_centeredSquareChain_statement` - `varianceProxyNormBound_of_centeredSquareChain_expansion` @@ -162,7 +165,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`, `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` | hardbone sharp-variance-chain provider, concrete row-moment evaluation, negative-side exact-row provider, and two-sided/operator-norm exact-row wrapper integration | +| 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`, `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` | wrapper variants consuming the generic centered-square chain bridge; full hardbone chain proof remains external | | 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 | @@ -265,6 +268,7 @@ Preferred CFC-free wrappers after the Bernstein CFC hardbone leaf: - `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_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` +- `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives` These wrappers still require Tropp/Lieb trace-MGF primitives and analytic integrability assumptions. The CFC-free wrappers remove the user-supplied @@ -273,18 +277,20 @@ The exact-row quadratic-form wrapper additionally removes the direct `MatrixVarianceProxyNormBound` premise on the positive-side route by using the hardbone exact-row consumer; it keeps the hardbone sharp-variance chain explicit and separates the uniform Bernstein radius from the row-specific variance-proxy -radii. These wrappers do not -prove Tropp/Lieb, Golden-Thompson, trace-exp integrability, variance-proxy -control beyond existing named adapters, or unconditional sample-covariance -concentration. +radii. 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`. These wrappers 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` - `centeredSampleCovarianceRowRankOneSumNeg_traceExpIntegrable_of_traceExpIntegrable_neg_theta` - `centeredSampleCovarianceRowRankOneFamilyNeg_cfcPrimitive_of_cfcPrimitive_neg_theta` +- `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two` -These are sign-normalization adapters from explicit original-family +The exact-row variance-proxy provider transfers the positive row-specific bound +through `matrixVarianceProxy_negRandomMatrixFamily`; the other entries are sign-normalization adapters from explicit original-family opposite-parameter provider assumptions. They do not prove exponential integrability, trace-exponential integrability, or the Bernstein CFC primitive, and they are not tail wrappers by themselves. @@ -311,6 +317,8 @@ and they are not tail wrappers by themselves. - `MatrixVarianceProxyNormBound_centeredRankOneRandomMatrixFamily_of_sqNorm_bound` - `MatrixVarianceProxyNormBound_centeredRankOneRandomMatrixFamily_of_sqNorm_bound_memLp_two` - `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamily_of_rowSqNorm_bound` +- `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two` +- `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives` - `sampleCovarianceCenteredRankOneVarianceProxyBound` ## Example Style diff --git a/docs/Status.md b/docs/Status.md index 2176b69..bcadda6 100644 --- a/docs/Status.md +++ b/docs/Status.md @@ -97,6 +97,8 @@ Sample covariance negative-side provider-transfer adapters: - `centeredSampleCovarianceRowRankOneFamilyNeg_expIntegrable_of_expIntegrable_neg_theta` - `centeredSampleCovarianceRowRankOneSumNeg_traceExpIntegrable_of_traceExpIntegrable_neg_theta` - `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` Hardbone proved leaves, deterministic bridges, statement targets, and thin consumers: @@ -192,8 +194,18 @@ Low-level prefix/state, reindex, negative-family, nullspace/decomposition, exact The row-specific exact-row sample-covariance hardbone consumer `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two` now combines this bounded-row square-integrability route with exact-row - deterministic norm control to produce RHS `rowSqNormVarianceProxyNormRHS R`; it still keeps the - abstract sharp-variance chain explicit. These are square-integrability and + deterministic norm control to produce RHS `rowSqNormVarianceProxyNormRHS R`. + 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 corresponding exact-row consumer. The generic centered-square + chain remains explicit. The negative-side provider + `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two` + transfers that exact-row bound to the named negative sample-covariance family + by reusing `matrixVarianceProxy_negRandomMatrixFamily`. Both keep the abstract + sharp-variance chain explicit. These are square-integrability and hardbone-consumer providers only; they do not duplicate the crude variance-proxy norm theorem. The variance-proxy provider-chain consumer is @@ -248,10 +260,12 @@ 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 now has an exact-row variance-proxy wrapper, but two-sided and operator-norm exact-row wrappers still need a negative-side exact-row variance-proxy provider contract. 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, and 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. - 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. + prove exponential integrability, trace-exponential integrability, or CFC. The + exact-row variance-proxy provider only transfers an already explicit + sharp-chain bound through negation; it is not a tail wrapper. - Completed hardbone wrapper task: `RM-HB-sample-covariance-cfc-free-wrapper-contract`. - Completed hardbone proof leaf: `RM-HB12-matrix-exp-log-selfadjoint-normalization-leaf`. @@ -336,10 +350,25 @@ Low-level prefix/state, reindex, negative-family, nullspace/decomposition, exact `RM-VP-sample-covariance-tail-wrapper-with-exact-row-vp-contract`, adding `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_troppPrimitive` as a positive-side quadratic-form wrapper with row-specific exact-row variance-proxy RHS and explicit hardbone sharp-chain premise. +- Completed hardbone proof leaf: + `RM-VP-negative-exact-row-variance-proxy-provider-contract`, adding + `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two` + as the named negative-family exact-row variance-proxy provider under the + explicit hardbone sharp-chain, coordinate `MemLp 2`, pointwise row squared-norm, + and nonnegative row-radius assumptions. +- Completed hardbone proof leaf: + `RM-VP-two-sided-operator-norm-exact-row-wrapper-integration-contract`, adding + `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives` as the CFC-free operator-norm wrapper that consumes positive and + negative row-specific exact-row variance-proxy RHS values. +- Completed hardbone proof leaf: + `RM-VP-concrete-row-moment-evaluation-contract`, adding the exact-row + concrete row-moment bridge from the generic centered-square variance-proxy + chain to the sample-specific sharp-chain statement and consumer. - Next safe hardbone task: - `RM-VP-negative-exact-row-variance-proxy-provider-contract`, focused on the - negative-side exact-row variance-proxy route required before two-sided or - operator-norm sample-covariance wrappers can use the exact-row RHS. + `RM-VP-centered-square-chain-wrapper-integration-contract`, focused on adding + thin sample-covariance wrapper variants that consume the generic + centered-square chain bridge instead of the sample-specific sharp-chain + premise, without changing Tropp/Lieb or Matrix Bernstein boundaries. ## Verification diff --git a/docs/TODO.md b/docs/TODO.md index 4d18792..f96c2a9 100644 --- a/docs/TODO.md +++ b/docs/TODO.md @@ -18,10 +18,12 @@ This is the active short list. Old completed task logs were collapsed into - Prefer shared RandomMatrix APIs over unfolded formulas in examples, tests, judge files, and docs. - Next RandomMatrix hardbone task: - `RM-VP-negative-exact-row-variance-proxy-provider-contract`. -- That next task should audit the negative-side exact-row variance-proxy route - needed before two-sided quadratic-form or operator-norm sample-covariance - wrappers can use row-specific exact-row variance proxies. + `RM-VP-centered-square-chain-wrapper-integration-contract`. +- The concrete exact-row row-moment bridge is available. The next task should + add thin sample-covariance wrapper variants that consume the generic + centered-square variance-proxy chain bridge instead of the sample-specific + sharp-chain premise, without claiming new Tropp/Lieb or full Matrix Bernstein + proofs. ## Active Documentation Work diff --git a/docs/TestPlan.md b/docs/TestPlan.md index 34caba4..adf16ee 100644 --- a/docs/TestPlan.md +++ b/docs/TestPlan.md @@ -28,7 +28,7 @@ git diff --check - Scalar API tests: probability, tail, Lp/moment, Orlicz, subGaussian, subExponential, real-inequality helpers, and scalar concentration files under `HighDimProbTest`. - Random-family and process API checks: `HighDimProbTest/RandomFamilyAPI.lean` plus `BranchImports.lean` and `ExperimentalImports.lean`. - RandomMatrix API tests: variance proxy, spectral, trace-exp, hardbone - statement targets, thin consumers, rank/support trace bridge, excess-support trace bridge, centered-square expectation expansion, `MatrixExpSupportDomination`, `MatrixExpExcessSupportDomination`, trace-exp eigenvalue-sum bridge, effective-rank consumer, ambient trace certificate, ambient effective-rank wrapper, star-projection trace/rank/PSD certificate and rank consumer, Laplace, concentration, and example API + statement targets, thin consumers, rank/support trace bridge, excess-support trace bridge, centered-square expectation expansion, `MatrixExpSupportDomination`, `MatrixExpExcessSupportDomination`, trace-exp eigenvalue-sum bridge, effective-rank consumer, ambient trace certificate, ambient effective-rank wrapper, star-projection trace/rank/PSD certificate and rank consumer, negative exact-row variance-proxy provider, Laplace, concentration, and example API checks. - RandomMatrix bookkeeping checks: trace-exp endpoint wrappers and the natural-state TraceExp route are covered in @@ -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, are covered in + CFC-free sample-covariance wrappers, including the positive-side exact-row variance-proxy quadratic-form wrapper and the negative exact-row variance-proxy provider, are covered in `HighDimProbTest/RandomMatrixConcentrationAPI.lean`, `HighDimProbTest/ExamplesAPI.lean`, and `HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean`. @@ -55,7 +55,9 @@ git diff --check comparison, rank-one second-moment consumer, exact row second-moment hardbone consumer, deterministic variance-proxy norm subadditivity, exact rank-one second-moment norm providers, the rank-one square-integrability four-product, - `MemLp 4`, bounded-row, centered-family providers, and the row-specific exact-row sample-covariance hardbone consumer in + `MemLp 4`, bounded-row, centered-family providers, the row-specific exact-row + sample-covariance hardbone consumer, and the generic-centered-square-chain + exact-row bridge in `RandomMatrixVarianceProxyAPI`, `RandomMatrixHardboneStatementsAPI`, and the corresponding judge/example surfaces. diff --git a/docs/TheoremAtlas.md b/docs/TheoremAtlas.md index d17b7c5..0438972 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. Positive-side quadratic-form tail-wrapper integration is available through `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_troppPrimitive`; concrete row-moment evaluation, negative-side exact-row transfer, two-sided control, and operator-norm exact-row integration remain open. +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`, and 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`. Wrapper variants consuming the generic centered-square chain bridge remain open. 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 @@ -137,7 +137,7 @@ or conditional-expectation inputs themselves. support-domination providers, support-construction certificates, true effective-rank/support trace certificates, and dimension/rank refinements beyond explicit star-projection rank consumers. -- A negative-side exact-row variance-proxy provider for two-sided/operator-norm sample-covariance wrappers. +- Two-sided/operator-norm sample-covariance wrappers that consume exact-row variance proxies on both signs. - A public-friendly Matrix Bernstein wrapper directly over the natural-state route. From ef464d367bc54e28fbca467b66799a1e96c1923b Mon Sep 17 00:00:00 2001 From: HighDimProb Dev Date: Sat, 20 Jun 2026 05:48:07 +0000 Subject: [PATCH 2/2] Expose centered-square chain wrappers for exact-row sample covariance Route sample-covariance tail wrappers through the generic centered-square variance-proxy chain while preserving explicit Tropp and analytic premises.\n\nConstraint: Keep generic centered-square chain, Tropp/Lieb, trace-MGF, and Matrix Bernstein boundaries explicit.\nRejected: Proving or hiding the centered-square chain inside tail wrappers | That would overstate the current hardbone boundary.\nConfidence: high\nScope-risk: narrow\nDirective: Future wrappers should derive sample-specific sharp-chain premises before reusing exact-row routes, not duplicate variance-proxy proofs.\nTested: RED unknown identifiers in concentration API and MatrixBernstein judge; 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 PR checks were not refreshed after this local commit. --- .../RandomMatrix/ConcentrationStatements.lean | 246 ++++++++++++++++++ .../RandomMatrix/MatrixBernsteinUse.lean | 2 + .../RandomMatrixConcentrationAPI.lean | 2 + docs/JudgeSystem.md | 6 +- docs/LeafPlan.md | 15 +- docs/RandomMatrixAPI.md | 13 +- docs/Status.md | 15 +- docs/TODO.md | 11 +- docs/TestPlan.md | 2 +- docs/TheoremAtlas.md | 6 +- 10 files changed, 292 insertions(+), 26 deletions(-) diff --git a/HighDimProb/RandomMatrix/ConcentrationStatements.lean b/HighDimProb/RandomMatrix/ConcentrationStatements.lean index 4e019fb..a54401c 100644 --- a/HighDimProb/RandomMatrix/ConcentrationStatements.lean +++ b/HighDimProb/RandomMatrix/ConcentrationStatements.lean @@ -2823,6 +2823,100 @@ theorem sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound (P := P) (A := A) (R := R) (t := t) (sigmaSq := rowSqNormVarianceProxyNormRHS Rvar) hm hMeas hLp hSq hIndep hIntSq hExpInt hTraceInt hSigma hR ht hNorm hTropp + +/-- Sample-covariance quadratic-form upper-tail wrapper consuming the generic +centered-square variance-proxy chain. + +This is the centered-square-chain variant of +`sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_troppPrimitive`. +It keeps the same positive-side Tropp primitive and analytic assumptions, but +replaces the sample-specific sharp-chain premise by +`varianceProxyNormBound_of_centeredSquareChain_statement` for the rank-one row +family. The generic centered-square chain itself remains explicit. -/ +theorem sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppPrimitive + {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) + (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) + (hSqVar : + forall k : Fin m, forall omega, + vectorSqNorm (rowVector A k omega) <= Rvar k) + (hIndep : + IndependentRandomMatrices P + (centeredSampleCovarianceRowRankOneFamily (P := P) A)) + (hExpInt : + forall k : Fin m, + IntegrableRandomMatrix P + (matrixExpScaledFamily + (centeredSampleCovarianceRowRankOneFamily (P := P) A) + (sampleCovarianceTailTheta (m := m) R t + (rowSqNormVarianceProxyNormRHS Rvar)) + k)) + (hTraceInt : + IntegrableRealRandomVariable P + (traceExpIntegrand + (centeredSampleCovarianceRowRankOneSum (P := P) A) + (sampleCovarianceTailTheta (m := m) R t + (rowSqNormVarianceProxyNormRHS Rvar)))) + (hSigma : 0 < rowSqNormVarianceProxyNormRHS Rvar) + (hR : 0 <= R) + (hRvar : forall i : Fin m, 0 <= Rvar i) + (ht : 0 < t) + (hChain : + @varianceProxyNormBound_of_centeredSquareChain_statement + Omega _ P _ (Fin m) _ (n + 1) + (rankOneRandomMatrixFamily (rowVector A)) + (fun i => matrixSecondMoment P (rankOneRandomMatrix (rowVector A i))) + (rowSqNormVarianceProxyNormRHS Rvar)) + (hTropp : + 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)) : + P (quadraticFormUpperTailEvent + (centeredRandomMatrix P (sampleCovariance A)) t) <= + sampleCovarianceQuadraticFormTailRHS + (m := m) (n := n + 1) R t + (rowSqNormVarianceProxyNormRHS Rvar) := by + have hRowsLp : + forall k : Fin m, forall j : Fin (n + 1), + MemLpRealRandomVariable P (coord (rowVector A k) j) 2 := by + intro k j + change MemLpRealRandomVariable P (matrixEntry A k j) 2 + exact hLp k j + have hSharp : + sampleCovarianceVarianceProxy_sharp_statement (P := P) (X := rowVector A) + (fun i => matrixSecondMoment P (rankOneRandomMatrix (rowVector A i))) + (rowSqNormVarianceProxyNormRHS Rvar) := + sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two + (P := P) (X := rowVector A) (R := Rvar) + hChain + (fun k => isRandomVector_rowVector hMeas k) + hRowsLp + hSqVar + exact + sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_troppPrimitive + (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 using the crude bounded-row variance-proxy norm bound. @@ -3794,6 +3888,158 @@ theorem sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos (sampleCovarianceCenteredRankOneRadius Rneg)) hTroppNeg +/-- Sample-covariance self-adjoint operator-norm tail wrapper consuming the +generic centered-square variance-proxy chain on both signs. + +This is the centered-square-chain variant of +`sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives`. +It keeps both sign-specific Tropp primitives and analytic assumptions explicit, +but replaces the two sample-specific sharp-chain premises by generic +`varianceProxyNormBound_of_centeredSquareChain_statement` premises for the +rank-one row family. The generic centered-square chains themselves remain +explicit. -/ +theorem sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppPrimitives + {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) + (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) + (hSqVar : + forall k : Fin m, forall omega, + vectorSqNorm (rowVector A k omega) <= Rvar k) + (hSqVarNeg : + forall k : Fin m, forall omega, + vectorSqNorm (rowVector A k omega) <= RvarNeg k) + (hIndep : + IndependentRandomMatrices P + (centeredSampleCovarianceRowRankOneFamily (P := P) A)) + (hExpInt : + forall k : Fin m, + IntegrableRandomMatrix P + (matrixExpScaledFamily + (centeredSampleCovarianceRowRankOneFamily (P := P) A) + (sampleCovarianceTailTheta (m := m) R t + (rowSqNormVarianceProxyNormRHS Rvar)) + k)) + (hTraceInt : + IntegrableRealRandomVariable P + (traceExpIntegrand + (centeredSampleCovarianceRowRankOneSum (P := P) A) + (sampleCovarianceTailTheta (m := m) R t + (rowSqNormVarianceProxyNormRHS Rvar)))) + (hSigma : 0 < rowSqNormVarianceProxyNormRHS Rvar) + (hR : 0 <= R) + (hRvar : forall i : Fin m, 0 <= Rvar i) + (ht : 0 < t) + (hChain : + @varianceProxyNormBound_of_centeredSquareChain_statement + Omega _ P _ (Fin m) _ n + (rankOneRandomMatrixFamily (rowVector A)) + (fun i => matrixSecondMoment P (rankOneRandomMatrix (rowVector A i))) + (rowSqNormVarianceProxyNormRHS Rvar)) + (hTropp : + 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)) + (hExpIntNeg : + forall k : Fin m, + IntegrableRandomMatrix P + (matrixExpScaledFamily + (centeredSampleCovarianceRowRankOneFamilyNeg (P := P) A) + (sampleCovarianceTailTheta (m := m) Rneg t + (rowSqNormVarianceProxyNormRHS RvarNeg)) + k)) + (hTraceIntNeg : + IntegrableRealRandomVariable P + (traceExpIntegrand + (centeredSampleCovarianceRowRankOneSumNeg (P := P) A) + (sampleCovarianceTailTheta (m := m) Rneg t + (rowSqNormVarianceProxyNormRHS RvarNeg)))) + (hSigmaNeg : 0 < rowSqNormVarianceProxyNormRHS RvarNeg) + (hRNeg : 0 <= Rneg) + (hRvarNeg : forall i : Fin m, 0 <= RvarNeg i) + (hChainNeg : + @varianceProxyNormBound_of_centeredSquareChain_statement + Omega _ P _ (Fin m) _ n + (rankOneRandomMatrixFamily (rowVector A)) + (fun i => matrixSecondMoment P (rankOneRandomMatrix (rowVector A i))) + (rowSqNormVarianceProxyNormRHS RvarNeg)) + (hTroppNeg : + 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)) : + 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 + have hRowsLp : + forall k : Fin m, forall j : Fin n, + MemLpRealRandomVariable P (coord (rowVector A k) j) 2 := by + intro k j + change MemLpRealRandomVariable P (matrixEntry A k j) 2 + exact hLp k j + have hSharp : + sampleCovarianceVarianceProxy_sharp_statement (P := P) (X := rowVector A) + (fun i => matrixSecondMoment P (rankOneRandomMatrix (rowVector A i))) + (rowSqNormVarianceProxyNormRHS Rvar) := + sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two + (P := P) (X := rowVector A) (R := Rvar) + hChain + (fun k => isRandomVector_rowVector hMeas k) + hRowsLp + hSqVar + have hSharpNeg : + sampleCovarianceVarianceProxy_sharp_statement (P := P) (X := rowVector A) + (fun i => matrixSecondMoment P (rankOneRandomMatrix (rowVector A i))) + (rowSqNormVarianceProxyNormRHS RvarNeg) := + sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two + (P := P) (X := rowVector A) (R := RvarNeg) + hChainNeg + (fun k => isRandomVector_rowVector hMeas k) + hRowsLp + hSqVarNeg + exact + sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives + (P := P) (A := A) (R := R) (Rneg := Rneg) (t := t) + (Rvar := Rvar) (RvarNeg := RvarNeg) + hm hMeas hLp hSq hSqNeg hSqVar hSqVarNeg hIndep hExpInt hTraceInt + hSigma hR hRvar ht hSharp hTropp hExpIntNeg hTraceIntNeg hSigmaNeg + hRNeg hRvarNeg hSharpNeg hTroppNeg + /-- 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 bb923d6..539a20b 100644 --- a/HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean +++ b/HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean @@ -45,6 +45,7 @@ open HighDimProb #check HighDimProb.sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound #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.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 @@ -55,6 +56,7 @@ open HighDimProb #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.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.negRandomMatrixFamily #check HighDimProb.matrixExpScaledFamily_negRandomMatrixFamily #check HighDimProb.integrableRandomMatrix_matrixExpScaledFamily_negRandomMatrixFamily diff --git a/HighDimProbTest/RandomMatrixConcentrationAPI.lean b/HighDimProbTest/RandomMatrixConcentrationAPI.lean index 1d3f681..3674221 100644 --- a/HighDimProbTest/RandomMatrixConcentrationAPI.lean +++ b/HighDimProbTest/RandomMatrixConcentrationAPI.lean @@ -159,6 +159,7 @@ variable (R theta sigma2 c c1 c2 t bound K : Real) #check sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound #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 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 @@ -168,6 +169,7 @@ 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 #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 centeredSampleCovarianceRowRankOneFamilyNeg #check centeredSampleCovarianceRowRankOneSumNeg #check isRandomMatrix_negRandomMatrixFamily diff --git a/docs/JudgeSystem.md b/docs/JudgeSystem.md index 42628b7..6b75668 100644 --- a/docs/JudgeSystem.md +++ b/docs/JudgeSystem.md @@ -73,9 +73,9 @@ 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 negative exact-row - variance-proxy provider visibility, and its main structural/analytic - dependencies. + `matrixBernsteinTraceMGF_statement`, sample-covariance exact-row and centered-square-chain wrapper visibility, + negative exact-row variance-proxy provider visibility, and their main + structural/analytic dependencies. ## How It Differs From Normal Tests diff --git a/docs/LeafPlan.md b/docs/LeafPlan.md index 2ed577e..8908669 100644 --- a/docs/LeafPlan.md +++ b/docs/LeafPlan.md @@ -35,10 +35,11 @@ - Stage M-real-1: real-exponent `SubGaussianMoment` bridge - Stage M-real-2: real-exponent `SubExponentialMoment` bridge - Stage SC-final-update: scalar closeout refreshed after both moment bridges - - Current repository next task: - RM-VP-centered-square-chain-wrapper-integration-contract. Natural-state - assumption bundling, negative trace-MGF provider cleanup, Matrix Bernstein, - Hanson-Wright, and WLLN/SLLN remain separate future directions. + - Current repository closeout: + PR/check review for RM-VP-centered-square-chain-wrapper-integration-contract. + Natural-state assumption bundling, negative trace-MGF provider cleanup, + Matrix Bernstein, Hanson-Wright, and WLLN/SLLN remain separate future + directions. - OrliczToTail - TailToOrlicz - MomentImplications @@ -258,9 +259,13 @@ `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two_of_centeredSquareChain` as the exact-row bridge from the generic centered-square variance-proxy chain to the sample-specific sharp-chain statement and consumer. +- Follow-up completed proof leaf: + `RM-VP-centered-square-chain-wrapper-integration-contract`, adding + positive-side quadratic-form and two-sided/operator-norm wrappers that consume + generic centered-square variance-proxy chains over the row-rank-one family. - Boundary preserved: this does not prove the generic centered-square chain, Tropp/Lieb, Golden-Thompson, Bernstein CFC, or Matrix Bernstein. -- Next safe leaf: `RM-VP-centered-square-chain-wrapper-integration-contract`. +- Next safe leaf: PR/check closeout, then select the next RandomMatrix leaf. ## Process diff --git a/docs/RandomMatrixAPI.md b/docs/RandomMatrixAPI.md index 97446ea..7ebfbdc 100644 --- a/docs/RandomMatrixAPI.md +++ b/docs/RandomMatrixAPI.md @@ -114,6 +114,8 @@ Variance-proxy / centered-square chain: - `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` - `varianceProxyNormBound_of_centeredSquareChain_statement` - `varianceProxyNormBound_of_centeredSquareChain_expansion` @@ -165,7 +167,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`, `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` | wrapper variants consuming the generic centered-square chain bridge; full hardbone chain proof remains external | +| 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 | | 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 | @@ -277,8 +279,13 @@ The exact-row quadratic-form wrapper additionally removes the direct `MatrixVarianceProxyNormBound` premise on the positive-side route by using the hardbone exact-row consumer; it keeps the hardbone sharp-variance chain explicit and separates the uniform Bernstein radius from the row-specific variance-proxy -radii. 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`. These wrappers do not prove Tropp/Lieb, Golden-Thompson, trace-exp +radii. The centered-square-chain positive-side variant is +`sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppPrimitive`. +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`. +These wrappers do not prove Tropp/Lieb, Golden-Thompson, trace-exp integrability, variance-proxy control beyond existing named adapters, or unconditional sample-covariance concentration. diff --git a/docs/Status.md b/docs/Status.md index bcadda6..c9a4c1c 100644 --- a/docs/Status.md +++ b/docs/Status.md @@ -260,7 +260,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, and 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`; 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 @@ -364,11 +364,14 @@ Low-level prefix/state, reindex, negative-family, nullspace/decomposition, exact `RM-VP-concrete-row-moment-evaluation-contract`, adding the exact-row concrete row-moment bridge from the generic centered-square variance-proxy chain to the sample-specific sharp-chain statement and consumer. -- Next safe hardbone task: - `RM-VP-centered-square-chain-wrapper-integration-contract`, focused on adding - thin sample-covariance wrapper variants that consume the generic - centered-square chain bridge instead of the sample-specific sharp-chain - premise, without changing Tropp/Lieb or Matrix Bernstein boundaries. +- Completed hardbone proof leaf: + `RM-VP-centered-square-chain-wrapper-integration-contract`, adding + positive-side quadratic-form and two-sided/operator-norm sample-covariance + wrappers that consume generic centered-square variance-proxy chains instead + of sample-specific sharp-chain premises. +- Next safe hardbone task: PR/check closeout for this wrapper integration, then + select the next RandomMatrix leaf without changing Tropp/Lieb or Matrix + Bernstein boundaries. ## Verification diff --git a/docs/TODO.md b/docs/TODO.md index f96c2a9..96ba05e 100644 --- a/docs/TODO.md +++ b/docs/TODO.md @@ -17,13 +17,12 @@ 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. -- Next RandomMatrix hardbone task: +- Current RandomMatrix hardbone closeout: finish PR/check review for `RM-VP-centered-square-chain-wrapper-integration-contract`. -- The concrete exact-row row-moment bridge is available. The next task should - add thin sample-covariance wrapper variants that consume the generic - centered-square variance-proxy chain bridge instead of the sample-specific - sharp-chain premise, without claiming new Tropp/Lieb or full Matrix Bernstein - proofs. +- 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. ## Active Documentation Work diff --git a/docs/TestPlan.md b/docs/TestPlan.md index adf16ee..0b08583 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 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, the two-sided/operator-norm exact-row wrappers, 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 0438972..9db21e7 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`, and 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`. Wrapper variants consuming the generic centered-square chain bridge remain open. +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`. 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 @@ -111,7 +111,9 @@ CFC-free `_of_troppPrimitive` / `_of_troppPrimitives` wrappers that reuse `bernsteinMatrixExp_le_quadratic` while keeping Tropp/Lieb and integrability assumptions explicit. The positive-side quadratic-form wrapper `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_troppPrimitive` uses the exact-row variance-proxy hardbone consumer and keeps -the sharp-chain premise explicit. The local matrix-exp/log normalization leaf is proved as +the sharp-chain premise explicit. Its centered-square-chain variant replaces +that premise by the generic centered-square variance-proxy chain over +`rankOneRandomMatrixFamily (rowVector A)`. 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. The log/order-to-`K` route now includes the proved thin bridge `matrixLog_le_of_le_matrixExp`, which