diff --git a/HighDimProb/RandomMatrix/HardboneStatements.lean b/HighDimProb/RandomMatrix/HardboneStatements.lean index 358b640..59a0f36 100644 --- a/HighDimProb/RandomMatrix/HardboneStatements.lean +++ b/HighDimProb/RandomMatrix/HardboneStatements.lean @@ -1,4 +1,5 @@ import HighDimProb.RandomMatrix.TraceExp +import HighDimProb.RandomMatrix.MatrixOrder import HighDimProb.RandomMatrix.Assumptions import HighDimProb.Analysis.RealInequalities @@ -639,6 +640,61 @@ abbrev varianceProxyNormBound_of_centeredSquareChain_statement sigma2 -> MatrixVarianceProxyNormBound P (centeredRandomMatrixFamily P A) sigma2 +/-- Typed blocker for Loewner-to-operator-norm monotonicity of deterministic +variance proxies. + +The centered-square provider can prove the finite-sum Loewner comparison from +per-summand comparisons. Turning that comparison into a scalar operator-norm +bound still requires a PSD/order-to-norm monotonicity theorem, kept explicit by +this contract. -/ +abbrev deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement {n : Nat} + (U V : Matrix (Fin n) (Fin n) Real) : Prop := + IsPSDMatrix U -> + MatrixLE U V -> + deterministicMatrixVarianceProxyNorm U <= deterministicMatrixVarianceProxyNorm V + +/-- Centered-square variance-proxy provider under an explicit norm-monotonicity +contract. + +This theorem proves the available bookkeeping part of the generic +centered-square chain: per-summand Loewner comparisons sum to a variance-proxy +Loewner comparison. The remaining conversion from Loewner order to deterministic +operator norm is exactly the `hNormMono` premise. -/ +theorem varianceProxyNormBound_of_centeredSquareChain_of_normMono + {Omega : Type*} [mOmega : MeasurableSpace Omega] + {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] + {I : Type*} [Fintype I] {n : Nat} + (A : I -> RandomMatrix Omega n n) + (V : I -> Matrix (Fin n) (Fin n) Real) + (sigma2 : Real) + (hNormMono : + deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement + (Finset.univ.sum fun i : I => + matrixSecondMoment P (centeredRandomMatrix P (A i))) + (Finset.univ.sum fun i : I => V i)) + (hPSD : IsPSDMatrix + (Finset.univ.sum fun i : I => + matrixSecondMoment P (centeredRandomMatrix P (A i)))) + (hLE : forall i, + MatrixLE (matrixSecondMoment P (centeredRandomMatrix P (A i))) (V i)) + (hNorm : deterministicMatrixVarianceProxyNorm (Finset.univ.sum fun i => V i) <= + sigma2) : + MatrixVarianceProxyNormBound P (centeredRandomMatrixFamily P A) sigma2 := by + have hSumLE : MatrixLE + (Finset.univ.sum fun i : I => + matrixSecondMoment P (centeredRandomMatrix P (A i))) + (Finset.univ.sum fun i : I => V i) := + matrixLE_sum hLE + have hNormLe : + deterministicMatrixVarianceProxyNorm + (Finset.univ.sum fun i : I => + matrixSecondMoment P (centeredRandomMatrix P (A i))) <= + deterministicMatrixVarianceProxyNorm (Finset.univ.sum fun i : I => V i) := + hNormMono hPSD hSumLE + simpa [MatrixVarianceProxyNormBound, matrixVarianceProxyNorm, + deterministicMatrixVarianceProxyNorm, matrixVarianceProxy, centeredRandomMatrixFamily] + using hNormLe.trans hNorm + /-- Thin consumer for the centered-square variance-proxy provider chain. This theorem only applies the explicit provider-chain statement. It does not diff --git a/HighDimProb/RandomMatrix/MatrixOrder.lean b/HighDimProb/RandomMatrix/MatrixOrder.lean index fdc09ba..2b19c09 100644 --- a/HighDimProb/RandomMatrix/MatrixOrder.lean +++ b/HighDimProb/RandomMatrix/MatrixOrder.lean @@ -289,6 +289,24 @@ theorem matrixLE_add {n : Nat} rw [hEq] exact hsum +/-- Finite sums preserve the explicit Loewner-style matrix comparison. -/ +theorem matrixLE_sum {I : Type*} [Fintype I] {n : Nat} + {A B : I -> Matrix (Fin n) (Fin n) Real} + (hAB : forall i, MatrixLE (A i) (B i)) : + MatrixLE (Finset.univ.sum fun i : I => A i) + (Finset.univ.sum fun i : I => B i) := by + unfold MatrixLE at * + have hsum : IsPSDMatrix (Finset.univ.sum fun i : I => B i - A i) := + isPSDMatrix_sum hAB + have hEq : + (Finset.univ.sum fun i : I => B i) - + (Finset.univ.sum fun i : I => A i) = + Finset.univ.sum fun i : I => B i - A i := by + ext r c + simp [Matrix.sub_apply, Matrix.sum_apply, Finset.sum_sub_distrib] + rw [hEq] + exact hsum + /-- Adding the same matrix on the left preserves `MatrixLE`. -/ theorem matrixLE_add_left {n : Nat} (C : Matrix (Fin n) (Fin n) Real) diff --git a/HighDimProbJudge/RandomMatrix/TraceExpUse.lean b/HighDimProbJudge/RandomMatrix/TraceExpUse.lean index ad5127a..928e4b7 100644 --- a/HighDimProbJudge/RandomMatrix/TraceExpUse.lean +++ b/HighDimProbJudge/RandomMatrix/TraceExpUse.lean @@ -127,6 +127,8 @@ open scoped MatrixOrder Matrix.Norms.Operator #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.deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement +#check HighDimProb.varianceProxyNormBound_of_centeredSquareChain_of_normMono #check HighDimProb.varianceProxyNormBound_of_centeredSquareChain #check HighDimProb.varianceProxyNormBound_of_centeredSquareChain_expansion #check HighDimProb.traceMatrixExp_le_rank_exp_lambdaMax_statement diff --git a/HighDimProbJudge/RandomMatrix/VarianceProxyUse.lean b/HighDimProbJudge/RandomMatrix/VarianceProxyUse.lean index fe83432..b6fda6e 100644 --- a/HighDimProbJudge/RandomMatrix/VarianceProxyUse.lean +++ b/HighDimProbJudge/RandomMatrix/VarianceProxyUse.lean @@ -54,6 +54,7 @@ import HighDimProb.RandomMatrix #check HighDimProb.matrixLE_sub_right_of_isPSD #check HighDimProb.matrixLE_trans #check HighDimProb.matrixLE_add +#check HighDimProb.matrixLE_sum #check HighDimProb.matrixLE_add_left #check HighDimProb.matrixLE_add_right #check HighDimProb.matrixLE_smul_of_nonneg diff --git a/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean b/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean index f3cf618..adbdb80 100644 --- a/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean +++ b/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean @@ -54,6 +54,8 @@ variable (mHist : Fin m -> MeasurableSpace Omega) #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 deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement +#check varianceProxyNormBound_of_centeredSquareChain_of_normMono #check traceMatrixExp_le_rank_exp_lambdaMax_statement #check traceMatrixExp_le_supportDim_exp_lambdaMax_statement #check matrixExpSupportDomination_identity_statement diff --git a/HighDimProbTest/RandomMatrixVarianceProxyAPI.lean b/HighDimProbTest/RandomMatrixVarianceProxyAPI.lean index 62c4145..6f81172 100644 --- a/HighDimProbTest/RandomMatrixVarianceProxyAPI.lean +++ b/HighDimProbTest/RandomMatrixVarianceProxyAPI.lean @@ -65,6 +65,7 @@ variable (hRnonneg : 0 <= R) #check matrixLE_sub_right_of_isPSD #check matrixLE_trans #check matrixLE_add +#check matrixLE_sum #check matrixLE_add_left #check matrixLE_add_right #check matrixLE_smul_of_nonneg diff --git a/docs/JudgeSystem.md b/docs/JudgeSystem.md index c60624b..e5c5b7e 100644 --- a/docs/JudgeSystem.md +++ b/docs/JudgeSystem.md @@ -65,7 +65,8 @@ theorems or typed statements without relying on local test internals. nonnegativity bridges, random self-adjoint trace-exp moment nonnegativity, real/lintegral bridge theorem, natural-state Tropp/trace-MGF route checks, the hardbone matrix-exp/log normalization theorem, the proved matrix log/order - bridge, and remaining typed statement APIs. + bridge, centered-square provider/norm-monotonicity contract APIs, and + remaining typed statement APIs. - `HighDimProbJudge/RandomMatrix/LaplaceUse.lean`: matrix Laplace RHS and lintegral RHS vocabulary, trace-exp threshold events, MB-S5 conditional Markov/Laplace bridge APIs, MB-S6 explicit-dominance conditional wrappers, @@ -256,7 +257,7 @@ MB-S9-matrixle-algebra-proof adds variance-proxy judge checks for `matrixQuadraticForm_add`, `matrixQuadraticForm_smul`, `isPSDMatrix_zero`, `isPSDMatrix_add`, `isPSDMatrix_smul_of_nonneg`, `matrixLE_refl`, `matrixLE_of_eq`, -`matrixLE_trans`, `matrixLE_add`, `matrixLE_add_left`, +`matrixLE_trans`, `matrixLE_add`, `matrixLE_sum`, `matrixLE_add_left`, `matrixLE_add_right`, and `matrixLE_smul_of_nonneg`. The examples use only explicit MatrixLE/PSD hypotheses and do not claim the single-summand MGF theorem, Bernstein CFC proof, trace-mgf provider, Golden-Thompson, Lieb, or diff --git a/docs/RandomMatrixAPI.md b/docs/RandomMatrixAPI.md index b2c4a38..def7ad3 100644 --- a/docs/RandomMatrixAPI.md +++ b/docs/RandomMatrixAPI.md @@ -122,6 +122,8 @@ Variance-proxy / centered-square chain: - `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppAssumptions` - `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two` - `varianceProxyNormBound_of_centeredSquareChain_statement` +- `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement` +- `varianceProxyNormBound_of_centeredSquareChain_of_normMono` - `varianceProxyNormBound_of_centeredSquareChain_expansion` Dimension / rank / effective-rank chain: @@ -153,6 +155,7 @@ Thin hardbone consumers: - `troppMasterTraceMGFConditionalStep_of_conditioningBridge` - `traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider` - `varianceProxyNormBound_of_centeredSquareChain` +- `varianceProxyNormBound_of_centeredSquareChain_of_normMono` - `traceMatrixExp_le_rank_exp_lambdaMax` - `traceMatrixExp_le_rank_exp_lambdaMax_of_isStarProjection` - `traceMatrixExp_le_supportDim_exp_lambdaMax` @@ -171,7 +174,7 @@ Hardbone status table: | Tropp/Lieb/GT one-step | `troppMasterTraceMGFStep_of_liebJensen_statement` | typed-prop | `troppMasterTraceMGFStep_of_liebJensen` | Lieb concavity, probability-measure Jensen, log-exp normalization; Golden-Thompson is separate | | Conditioning / independence | `troppConditionalStep_of_iIndepFun_statement` | proven by `troppConditionalStep_of_iIndepFun` | `troppMasterTraceMGFConditionalStep_of_conditioningBridge` | thin forwarder only; generated histories, history/current-step independence, finite-family independence, and conditional expectation reduction remain explicit premises | | Trace-exp integrability | `traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider_statement` | typed-prop with proved thin consumer | `traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider` | automatic absolute domination, Golden-Thompson/product, or boundedness provider | -| Variance proxy / centered square | `varianceProxyNormBound_of_centeredSquareChain_statement`, `matrixSquare_centeredRandomMatrix_expectation_expansion_statement`, `centeredRankOneSquare_le_rankOneSecondMoment_statement` | centered-square expectation expansion and centered rank-one second-moment comparison proved; typed-prop chain has proved thin consumers | `matrixSquare_centeredRandomMatrix_expectation_expansion`, `matrixSecondMoment_centeredRandomMatrix_le_matrixSecondMoment`, `centeredRankOneSquare_le_rankOneSecondMoment`, `varianceProxyNormBound_of_centeredSquareChain`, `varianceProxyNormBound_of_centeredSquareChain_expansion`, `sampleCovarianceVarianceProxy_sharp_of_rankOneSecondMoment`, `sampleCovarianceVarianceProxy_sharp_of_exactRowSecondMoment`, `deterministicMatrixVarianceProxyNorm_sum_le_sum`, `deterministicMatrixVarianceProxyNorm_matrixSecondMoment_rankOneRandomMatrix_le_sq_of_sqNorm_bound`, `deterministicMatrixVarianceProxyNorm_sum_matrixSecondMoment_rankOneRandomMatrix_le_sum_sq_of_sqNorm_bound`, `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two`, `sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two`, `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two_of_centeredSquareChain`, `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppPrimitive`, `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppPrimitives`, `SampleCovarianceExactRowCenteredSquareTroppAssumptions`, `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppAssumptions`, `SampleCovarianceExactRowCenteredSquareTwoSidedTroppAssumptions`, `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppAssumptions`, `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two`, `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives`, `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_integrable_four_products`, `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_memLp_four`, `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_sqNorm_bound_memLp_two`, `integrableRandomMatrix_randomMatrixSquare_centeredRankOneRandomMatrixFamily_of_memLp_four`, `integrableRandomMatrix_randomMatrixSquare_centeredRankOneRandomMatrixFamily_of_sqNorm_bound_memLp_two`, `MatrixVarianceProxyNormBound_centeredRankOneRandomMatrixFamily_of_sqNorm_bound_memLp_two` | full generic centered-square-chain proof remains external; wrappers and bundles still require Tropp/Lieb and analytic integrability premises | +| Variance proxy / centered square | `varianceProxyNormBound_of_centeredSquareChain_statement`, `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement`, `matrixSquare_centeredRandomMatrix_expectation_expansion_statement`, `centeredRankOneSquare_le_rankOneSecondMoment_statement` | centered-square expectation expansion, finite-sum MatrixLE bookkeeping, 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_of_normMono`, `varianceProxyNormBound_of_centeredSquareChain_expansion`, `sampleCovarianceVarianceProxy_sharp_of_rankOneSecondMoment`, `sampleCovarianceVarianceProxy_sharp_of_exactRowSecondMoment`, `deterministicMatrixVarianceProxyNorm_sum_le_sum`, `deterministicMatrixVarianceProxyNorm_matrixSecondMoment_rankOneRandomMatrix_le_sq_of_sqNorm_bound`, `deterministicMatrixVarianceProxyNorm_sum_matrixSecondMoment_rankOneRandomMatrix_le_sum_sq_of_sqNorm_bound`, `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two`, `sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two`, `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two_of_centeredSquareChain`, `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppPrimitive`, `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppPrimitives`, `SampleCovarianceExactRowCenteredSquareTroppAssumptions`, `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppAssumptions`, `SampleCovarianceExactRowCenteredSquareTwoSidedTroppAssumptions`, `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppAssumptions`, `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two`, `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives`, `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_integrable_four_products`, `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_memLp_four`, `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_sqNorm_bound_memLp_two`, `integrableRandomMatrix_randomMatrixSquare_centeredRankOneRandomMatrixFamily_of_memLp_four`, `integrableRandomMatrix_randomMatrixSquare_centeredRankOneRandomMatrixFamily_of_sqNorm_bound_memLp_two`, `MatrixVarianceProxyNormBound_centeredRankOneRandomMatrixFamily_of_sqNorm_bound_memLp_two` | full generic centered-square-chain proof remains external; the norm-monotonicity provider is an explicit blocker, and wrappers/bundles still require Tropp/Lieb and analytic integrability premises | | Dimension / support / effective rank | `traceMatrixExp_le_rank_exp_lambdaMax_statement`, `traceMatrixExp_le_supportDim_exp_lambdaMax_statement`, `traceMatrixExp_effectiveRank_bound_statement`, `matrixExpSupportDomination_identity_statement`, `traceMatrixExp_excess_supportDim_exp_lambdaMax_statement` | rank/support targets and effective-rank consumer proved under explicit support, PSD, lambda-max, and trace-certificate assumptions; ambient trace certificate and star-projection rank/PSD consumer proved; identity support provider target named only; excess trace bridge and supportDim consumer proved under explicit excess certificate | `traceMatrixExp_le_rank_exp_lambdaMax`, `traceMatrixExp_le_rank_exp_lambdaMax_of_isStarProjection`, `traceMatrixExp_le_supportDim_exp_lambdaMax`, `traceMatrixExp_excess_supportDim_exp_lambdaMax`, `traceMatrixExp_effectiveRank_bound`, `traceMatrixExp_effectiveRank_bound_of_ambientTraceCertificate`; deterministic helpers include `MatrixExpSupportDomination`, `MatrixExpExcessSupportDomination`, `traceMatrixExp_le_card_add_trace_support_mul_exp_sub_one_of_excessSupportDomination`, `traceMatrixExp_eq_sum_exp_eigenvalues`, `traceMatrixExp_smul_le_card_add_trace_div_mul_exp_sub_one_of_psd_lambdaMax_le`, `matrixTrace_le_card_mul_of_isPSD_lambdaMaxOrdered_le`, `matrixTrace_eq_rank_of_isStarProjection`, `isPSDMatrix_of_isStarProjection` | identity/excess support-domination providers and support-construction certificates; true effective-rank trace certificate provider beyond ambient dimension | | Thin consumers | `troppMasterTraceMGFConditionalStep_of_conditioningBridge` | proven | public API/test/judge/example checks | thin wrapper only; no hard fact is discharged | @@ -325,6 +328,7 @@ and they are not tail wrappers by themselves. - `integrableRandomMatrix_randomMatrixSquare_centeredRankOneRandomMatrixFamily_of_memLp_four` - `integrableRandomMatrix_randomMatrixSquare_centeredRankOneRandomMatrixFamily_of_sqNorm_bound_memLp_two` - `matrixSecondMoment_centeredRandomMatrix` +- `matrixLE_sum` - `deterministicMatrixVarianceProxyNorm_sum_le_sum` - `deterministicMatrixVarianceProxyNorm_matrixSecondMoment_rankOneRandomMatrix_le_sq_of_sqNorm_bound` - `deterministicMatrixVarianceProxyNorm_sum_matrixSecondMoment_rankOneRandomMatrix_le_sum_sq_of_sqNorm_bound` diff --git a/docs/Status.md b/docs/Status.md index 93288f4..3ecacc9 100644 --- a/docs/Status.md +++ b/docs/Status.md @@ -117,6 +117,9 @@ Hardbone proved leaves, deterministic bridges, statement targets, and thin consu - `traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider` - `varianceProxyNormBound_of_centeredSquareChain` - `matrixSquare_centeredRandomMatrix_expectation_expansion` +- `matrixLE_sum` +- `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement` +- `varianceProxyNormBound_of_centeredSquareChain_of_normMono` - `varianceProxyNormBound_of_centeredSquareChain_expansion` - `matrixTrace_smul` - `matrixTrace_le_of_matrixLE` @@ -215,10 +218,14 @@ Low-level prefix/state, reindex, negative-family, nullspace/decomposition, exact hardbone-consumer providers only; they do not duplicate the crude variance-proxy norm theorem. The variance-proxy provider-chain consumer is - proved as `varianceProxyNormBound_of_centeredSquareChain`; the newer - `varianceProxyNormBound_of_centeredSquareChain_expansion` removes the explicit - centered-square expansion argument but still requires Loewner comparison and - deterministic norm-control assumptions. The rank/support trace-bound bridge is now proved through + proved as `varianceProxyNormBound_of_centeredSquareChain`. The provider route + `varianceProxyNormBound_of_centeredSquareChain_of_normMono` now proves the + finite-sum Loewner bookkeeping with `matrixLE_sum`, while keeping + Loewner-to-deterministic-operator-norm monotonicity as the explicit + `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement` blocker. The + newer `varianceProxyNormBound_of_centeredSquareChain_expansion` removes the + explicit centered-square expansion argument but still requires Loewner + comparison and deterministic norm-control assumptions. The rank/support trace-bound bridge is now proved through `traceMatrixExp_le_trace_support_exp_lambdaMax_of_supportDomination` and the `traceMatrixExp_le_rank_exp_lambdaMax` / `traceMatrixExp_le_supportDim_exp_lambdaMax` consumers. Explicit diff --git a/docs/TODO.md b/docs/TODO.md index c66e772..bfdfafc 100644 --- a/docs/TODO.md +++ b/docs/TODO.md @@ -17,8 +17,9 @@ This is the active short list. Old completed task logs were collapsed into Matrix Bernstein proofs. - Prefer shared RandomMatrix APIs over unfolded formulas in examples, tests, judge files, and docs. -- Current RandomMatrix hardbone branch: example-usage follow-up for - `RM-SC-centered-square-bundle-example-usage-contract`. +- Current RandomMatrix hardbone branch: centered-square provider contract + `RM-VP-centered-square-chain-provider-contract`, splitting finite-sum + Loewner bookkeeping from the remaining norm-monotonicity blocker. - The centered-square-chain wrapper variants are available for both the positive-side quadratic-form route and the two-sided/operator-norm route; natural assumption bundles now package those exact-row routes without diff --git a/docs/TestPlan.md b/docs/TestPlan.md index b61273f..e81c835 100644 --- a/docs/TestPlan.md +++ b/docs/TestPlan.md @@ -56,8 +56,9 @@ git diff --check 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, the row-specific exact-row - sample-covariance hardbone consumer, and the generic-centered-square-chain - exact-row bridge in + sample-covariance hardbone consumer, the finite-sum `matrixLE_sum` order + helper, the explicit norm-monotonicity blocker surface, 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 5a39140..a71b00c 100644 --- a/docs/TheoremAtlas.md +++ b/docs/TheoremAtlas.md @@ -52,10 +52,14 @@ domination assumption. The centered-square expectation expansion is proved by matrix expectation helpers `matrixExpect_const_mul` and `matrixExpect_mul_const` and the identity `matrixSecondMoment_centeredRandomMatrix`. The variance-proxy centered-square-chain consumers -`varianceProxyNormBound_of_centeredSquareChain` and -`varianceProxyNormBound_of_centeredSquareChain_expansion` are proved; the latter -removes the explicit expansion premise but still requires Loewner comparison -and deterministic norm-control assumptions. The centered rank-one second-moment +`varianceProxyNormBound_of_centeredSquareChain`, +`varianceProxyNormBound_of_centeredSquareChain_of_normMono`, and +`varianceProxyNormBound_of_centeredSquareChain_expansion` are proved. The +`of_normMono` route proves the finite-sum Loewner bookkeeping via +`matrixLE_sum`, but keeps Loewner-to-operator-norm monotonicity as the explicit +`deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement` blocker; the +expansion route removes the explicit expansion premise but still requires +Loewner comparison and deterministic norm-control assumptions. The centered rank-one second-moment comparison is proved by `centeredRankOneSquare_le_rankOneSecondMoment`, using `matrixSecondMoment_centeredRandomMatrix_le_matrixSecondMoment` and `matrixLE_sub_right_of_isPSD`. The sample-covariance consumer