This is the caller-facing endpoint, import, and assumption guide for the
RandomMatrix concentration API. Use it to choose public theorem endpoints,
imports, and the hypotheses they require. Old historical notes were collapsed
into archive.md; use git history for exact old wording.
For supported scope and current status, see Status.md; for
active work, see TODO.md; and for module ownership and dependency
direction, see RandomMatrixArchitecture.md.
Family-level proved/open status is owned by TheoremAtlas.md.
Downstream users of the matrix-concentration results documented here should normally use:
import HighDimProb.RandomMatrix.ConcentrationThe public HighDimProb.RandomMatrix.Concentration facade is the downstream
caller endpoint. The HighDimProb.RandomMatrix.Provider.* modules are
internal/expert proof boundaries; use the narrowest provider import only when
developing or auditing provider proofs. Their ownership and dependency rules
are defined in RandomMatrixArchitecture.md.
Basic.leanAssumptions.leanSums.leanOperatorNorm.leanSpectral.leanTraceExp.leanTraceExpDerivative.leanTraceExpMonotonicity.leanHardboneStatements.leanCStarBridge.leanVarianceProxy.leanConcentrationStatements.lean
matrixBernsteinOptimizedScalarTailRHSmatrixBernsteinTwoSidedOptimizedScalarTailRHSmatrixBernsteinTwoSidedOptimizedScalarTailRHS_sameParametersone_le_matrixBernsteinTwoSidedOptimizedScalarTailRHS_zeroMatrixBernsteinPositiveSideTroppAssumptionsMatrixBernsteinNegativeSideTroppAssumptionssampleCovarianceCenteredRankOneRadiussampleCovarianceTailThetasampleCovarianceQuadraticFormTailRHSrowSqNormVarianceProxyNormRHS
Use these helpers in examples and tests instead of copying RHS formulas.
Expectation / integrability bridges:
integrable_matrix_of_integrableRandomMatrixmatrixExpect_eq_integral_l2OperatormatrixExpect_eq_integral
These connect the public entrywise IntegrableRandomMatrix and matrixExpect
API to Mathlib's Bochner Integrable / integral lemmas. Use them when provider
proofs need linear-map, measure-map, or Jensen-style integral machinery without
duplicating entrywise-to-Bochner boilerplate.
Order / PSD representation bridges:
isPSDMatrix_of_posSemidefposSemidef_of_isPSDMatrixmatrixLE_of_mathlib_lemathlib_le_of_matrixLE
These bridge HighDimProb's explicit quadratic-form PSD vocabulary and Mathlib's ordered-matrix API without installing a new matrix order abstraction.
Spectral endpoints:
lambdaMaxlambdaMaxOrderedlambdaMaxOrdered_eq_eigenvalues₀_zerolambdaMaxOrdered_is_greatest_eigenvalue_statementlambdaMaxOrdered_is_greatest_eigenvaluelambdaMinlambdaMinOrderedlambdaMinOrdered_is_least_eigenvalue_statementlambdaMinOrdered_is_least_eigenvaluelambdaMinOrdered_le_eigenvalues₀
These wrappers keep the legacy lambdaMax / lambdaMin names while exposing
the canonical ordered eigenvalues₀ endpoints.
CStar representation bridge:
realMatrixToCStarMatrixrealMatrixToCStarStarAlgHomrealMatrixToCStar_nonnegrealMatrixToCStar_strictlyPositiverealMatrixToCStar_matrixLErealMatrixToCStar_logisSelfAdjointMatrix_cfc_logcstarMatrixOfMatrix_posSemidef_of_nonnegposSemidef_of_complexification_posSemidefmatrixLE_of_realMatrixToCStar_matrixLErealMatrixToCStarMatrix_applyrealMatrixToCStarMatrix_addrealMatrixToCStarMatrix_subisSelfAdjoint_realMatrixToCStarMatrix
These expose the real-matrix to CStarMatrix representation layer needed to
reuse Mathlib CStar functional-calculus order results. Strict positivity,
Loewner-order, and strictly-positive self-adjoint CFC.log transport are now
proved in the main repository; realMatrixToCStar_log is intentionally restricted to that domain.
matrixVarianceProxy_eq_zero_of_normBound_zerorandomMatrixFamily_ae_eq_zero_of_matrixVarianceProxy_eq_zerorandomMatrixFamily_ae_eq_zero_of_matrixVarianceProxyNormBound_zerorandomMatrixSum_ae_eq_zero_of_family_ae_eq_zeroupperTailProb_operatorNorm_randomMatrixSum_eq_zero_of_ae_eq_zeroupperTailProb_operatorNorm_randomMatrixSum_eq_zero_of_varianceNormBound_zero
These declarations live in HighDimProb.RandomMatrix.VarianceZero. They prove
the degenerate variance branch exactly: a zero variance-proxy norm bound for
self-adjoint square-integrable summands forces each summand and their finite
sum to vanish almost everywhere, hence every positive operator-norm upper tail
has probability zero. They do not supply the positive-variance Tropp branch.
bernsteinAdditiveTailThresholdbernsteinAdditiveTailThreshold_nonnegbernsteinAdditiveTailThreshold_sqbernsteinAdditiveTailThreshold_posbernsteinAdditiveTailThreshold_exponent_eqmatrixBernsteinLogFactormatrixBernsteinLogFactor_posmatrixBernsteinHighProbabilityThresholdmatrixBernsteinHighProbabilityThreshold_nonnegmatrixBernsteinTwoSidedOptimizedScalarTailRHS_highProbabilityThresholdmatrixBernsteinSelfAdjointHighProbabilityStatementmatrixBernsteinSelfAdjointHighProbabilityStatement_of_optimizedStatementMatrixBernstein.operatorNormTail_of_primitivesMatrixBernstein.operatorNormTail_of_primitives_nonnegMatrixBernstein.operatorNormUpperTail_of_primitivesMatrixBernstein.optimized_of_primitivesMatrixBernstein.CenteredRankOneInputsMatrixBernstein.CenteredRankOneExactRowInputsMatrixBernstein.centeredRankOneMatrixBernstein.centeredRankOneExactRowMatrixBernstein.sampleCovarianceExactRowMatrixBernstein.sampleCovarianceExactRowHighProbabilityMatrixBernstein.highProbability_of_primitivesmatrixBernsteinSelfAdjointOptimizedStatementmatrixBernsteinTraceMGFWithBernsteinCoeff_under_primitivesTraceExpConditioning.bernsteinInputs_of_primitivesTraceExpConditioning.bernsteinStep_of_history_letroppMasterTraceMGFFiniteFamily_generatedHistory_of_bernsteinPrimitivesmatrixBernsteinTraceMGFWithBernsteinCoeff_generatedHistory_of_bernsteinPrimitivesmatrixBernsteinQuadraticFormUpperTail_generatedHistory_of_bernsteinPrimitivesmatrixBernsteinQuadraticFormUpperTail_generatedHistory_of_bernsteinPrimitives_tailSubsetDischarged_of_randomSelfAdjointmatrixBernsteinTraceMGF_under_troppmatrixBernsteinQuadTail_trace_under_troppmatrixBernsteinQuadTail_scalar_under_troppmatrixBernsteinQuadTail_opt_under_troppmatrixBernsteinQuadraticFormUpperTailOptimizedScalarRHSWithBernsteinCoeff_under_primitivesmatrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridgeMatrixBernsteinConditioningTraceMGFTailAssumptionsmatrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFTailAssumptionsMatrixBernsteinConditioningTraceMGFProviderAssumptionsMatrixBernsteinConditioningTraceMGFProviderAssumptions.toTailAssumptionsmatrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFProviderAssumptionsmatrixBernsteinQuadraticFormUpperTail_of_naturalStateProviderAssumptionsmatrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge_tailSubsetDischarged_of_randomSelfAdjointmatrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFProviderAssumptions_tailSubsetDischarged_of_randomSelfAdjointmatrixBernsteinQuadraticFormUpperTail_of_naturalStateProviderAssumptions_tailSubsetDischarged_of_randomSelfAdjointmatrixBernsteinQuadraticFormUpperTailOptimizedScalarRHSWithBernsteinCoeff_of_assumptionsmatrixBernsteinQuadTail_opt_of_troppmatrixBernsteinTwoSidedQuadraticFormTailOptimizedScalarRHSWithBernsteinCoeff_under_primitivesmatrixBernsteinQuadTail_twoSided_opt_of_troppmatrixBernsteinSelfAdjointOperatorNormTailOptimizedScalarRHSWithBernsteinCoeff_arbitrary_of_pos_under_primitivesmatrixBernsteinOpNormTail_opt_of_tropp
The scalar threshold API is the exact positive-root inversion for the
additive-denominator exponent
t^2 / (2 * varianceProxy + (2 / 3) * maxScale * t). Its nonnegativity,
square identity, positivity, and exponent-equality lemmas expose the sign
boundary explicitly. The matrix
surface sets logFactor = log (2 * n / delta). matrixBernsteinLogFactor_pos
requires 0 < n and 0 < delta <= 1; the exact RHS equality and the public
self-adjoint contract additionally require 0 <= sigmaSq, 0 <= R, and
0 < sigmaSq or 0 < R. The contract keeps integrability,
centered self-adjointness, independence, norm, and variance-proxy assumptions
explicit.
matrixBernsteinSelfAdjointHighProbabilityStatement_of_optimizedStatement
is the scalar-threshold consumer: it evaluates an optimized tail contract at the
canonical threshold and converts its RHS to ENNReal.ofReal delta.
MatrixBernstein.optimized_of_primitives constructs that optimized contract
from the standard finite-dimensional Bernstein primitives, and
MatrixBernstein.highProbability_of_primitives exposes the closed
high-probability route. These theorems do not prove unconditional Matrix
Bernstein.
MatrixBernstein.sampleCovarianceExactRowHighProbability specializes the
row-specific sample-covariance tail at
matrixBernsteinHighProbabilityThreshold / m, matching the normalization in
sampleCovariance. Its nondegeneracy and delta hypotheses are exactly the
ones used by the scalar inversion theorem. If a caller has
ProbabilityTheory.iIndepFun X P for the original row vectors,
iIndepFun_centeredRankOne supplies independence of their centered rank-one
matrix family.
These are under explicit primitive assumptions. The pointwise Bernstein CFC
primitive is now proved by bernsteinMatrixExp_le_quadratic; the
under_troppPrimitive trace-MGF wrapper uses that proof so callers no longer
pass pointwise CFC at the trace-MGF provider layer. The
matrixBernsteinSelfAdjointOptimizedStatement fixes the canonical two-sided
RHS over an arbitrary finite index type; MatrixBernstein.optimized_of_primitives
proves it by reindexing through Fin (Fintype.card I). The preferred public
consumer surface is the
*_of_troppAssumptions family, which uses
MatrixBernsteinPositiveSideTroppAssumptions and
MatrixBernsteinNegativeSideTroppAssumptions to expose Tropp/Lieb and
bookkeeping assumptions without a user-supplied CFC field. The older
*_of_assumptions and _under_primitives names remain compatibility surfaces.
The generated-history Bernstein wrappers live behind
HighDimProb.RandomMatrix.Provider.Concentration and are re-exported by the
public HighDimProb.RandomMatrix.Concentration facade; they derive current-step
exponential-mean self-adjointness and strict positivity from centered
self-adjoint bounded summands. The base quadratic-form tail wrapper keeps tail
measurability explicit, while MatrixBernstein.operatorNormUpperTail_of_primitives,
MatrixBernstein.optimized_of_primitives, and
MatrixBernstein.highProbability_of_primitives perform the finite-family
operator-norm and threshold assembly.
The S10 conditioning-to-tail route also records the developer-facing scaffold
MatrixBernsteinConditioningTraceMGFTailAssumptions and the thin
matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFTailAssumptions
wrapper for provider-target bookkeeping. The compressed provider-assumption
and natural-state wrappers are
MatrixBernsteinConditioningTraceMGFProviderAssumptions,
matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFProviderAssumptions,
and matrixBernsteinQuadraticFormUpperTail_of_naturalStateProviderAssumptions.
Their provider bundle derives the exact history/current-step independence
contract from explicit random-matrix data while retaining finite-family
independence as an input; their TailEvent variants discharge only the subset
premise. These names are not the preferred reader-facing Matrix Bernstein API.
The route still does not prove
Tropp/Lieb, Golden-Thompson, trace-exp integrability, variance-proxy control,
tail measurability, operator-norm endpoint assembly, or a full unconditional
Matrix Bernstein theorem. The raw conditioning-to-tail wrapper
matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge is a thin
composition from the S9 conditioning trace-MGF consumer to the existing
quadratic-form Laplace route under an explicit tail-event subset assumption.
Bernstein CFC chain:
scalarBernsteinExpQuadraticInequality_statementscalarBernsteinExpQuadraticInequalityselfAdjointSpectrumBoundedByOperatorNorm_statementselfAdjointSpectrumBoundedByOperatorNormcfcScalarInequalityToMatrixLE_statementcfcScalarInequalityToMatrixLE_bernsteinExpQuadraticbernsteinCFCExpressionNormalization_statementbernsteinCFCExpressionNormalizationbernsteinMatrixExp_le_quadratic_of_cfcChain_statementbernsteinMatrixExp_le_quadratic_of_cfcLeavesbernsteinMatrixExp_le_quadratic
Log/order-to-K chain:
operatorLogMonotoneOnPositiveMatrices_statementoperatorLogMonotoneOnPositiveMatricesmatrixExpLogDomainForSelfAdjoint_statementmatrixExpLogDomainForSelfAdjointmatrixLog_le_of_le_matrixExp_statementmatrixLog_le_of_le_matrixExptraceMatrixExp_mono_add_selfAdjoint_statementtraceMatrixExp_mono_add_selfAdjointtroppLogExpComparisonToK
Tropp/Lieb/Golden-Thompson chain:
liebTraceExpConcavity_statementliebJensenTraceExp_statementgoldenThompsonTraceExp_statementgoldenThompsonTraceExpmatrixExpLogSelfAdjointNormalization_statementmatrixExpLogSelfAdjointNormalizationtroppMasterTraceMGFStep_of_liebJensen_statement
Conditioning / independence chain:
troppNaturalHistoryMeasurable_statementtroppHistoryStepIndependent_of_iIndepFun_statementTroppNaturalHistory.historyStepContractOfIsRandomMatrixcondExp_traceExp_history_add_independent_step_statementtroppConditionalStep_of_iIndepFun_statementtroppConditionalStep_of_iIndepFun
Integrability provider chain:
matrixExpScaledIntegrable_of_provider_statementtraceExpIntegrable_troppStateHistory_add_step_statementtraceExpIntegrable_troppStateHistory_add_K_statementtraceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider_statement
Variance-proxy / centered-square chain:
matrixSquare_centeredRandomMatrix_expectation_expansion_statementmatrixSquare_centeredRandomMatrix_expectation_expansioncenteredRankOneSquare_le_rankOneSecondMoment_statementcenteredRankOneSquare_le_rankOneSecondMomentsampleCovarianceVarianceProxy_sharp_statementsampleCovarianceVarianceProxy_sharp_of_rankOneSecondMomentsampleCovarianceVarianceProxy_sharp_of_exactRowSecondMomentsampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_twosampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_twosampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two_of_centeredSquareChainMatrixVarianceProxyNormBound_centeredRankOneRandomMatrixFamily_of_rowSqNorm_bound_memLp_twoMatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamily_of_exactRowSqNorm_bound_memLp_twoMatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_direct_of_exactRowSqNorm_bound_memLp_twoMatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_twovarianceProxyNormBound_of_centeredSquareChain_statementdeterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statementdeterministicMatrixVarianceProxyNorm_mono_of_matrixLEvarianceProxyNormBound_of_centeredSquareChain_of_normMonovarianceProxyNormBound_of_centeredSquareChain_expansion
Dimension / rank / effective-rank chain:
traceMatrixExp_le_rank_exp_lambdaMax_statementtraceMatrixExp_le_supportDim_exp_lambdaMax_statementtraceMatrixExp_effectiveRank_bound_statement
Deterministic trace / rank bridges:
matrixTrace_smulmatrixTrace_le_of_matrixLEtraceMatrixExp_le_trace_support_exp_lambdaMax_of_supportDomination(preferred reader-facing name; the older_of_matrixExp_le_smul_supportspelling remains as a compatibility alias)traceMatrixExp_le_card_add_trace_support_mul_exp_sub_one_of_excessSupportDominationtraceMatrixExp_eq_sum_exp_eigenvaluestraceMatrixExp_smul_le_card_add_trace_div_mul_exp_sub_one_of_psd_lambdaMax_lematrixTrace_le_card_mul_of_isPSD_lambdaMaxOrdered_lematrixTrace_eq_rank_of_isStarProjection
Generated-history centered rank-one consumers:
MatrixBernstein.CenteredRankOneExactRowInputsMatrixBernstein.centeredRankOneExactRowMatrixBernstein.sampleCovarianceExactRowMatrixBernstein.sampleCovarianceExactRowHighProbabilityiIndepFun_centeredRankOne
Thin hardbone consumers:
bernsteinMatrixExp_le_quadratic_of_cfcChainbernsteinMatrixExp_le_quadratic_of_cfcLeavesbernsteinMatrixExp_le_quadraticmatrixLog_le_of_le_matrixExptroppMasterTraceMGFStep_of_liebJensentroppConditionalStep_of_iIndepFuntroppMasterTraceMGFConditionalStep_of_conditioningBridgetraceMGFBernsteinVarianceProxyBound_of_conditioningBridgetraceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvidervarianceProxyNormBound_of_centeredSquareChainvarianceProxyNormBound_of_centeredSquareChain_of_normMonodeterministicMatrixVarianceProxyNorm_mono_of_matrixLEtraceMatrixExp_le_rank_exp_lambdaMaxtraceMatrixExp_le_rank_exp_lambdaMax_of_isStarProjectiontraceMatrixExp_le_supportDim_exp_lambdaMaxtraceMatrixExp_excess_supportDim_exp_lambdaMaxtraceMatrixExp_effectiveRank_boundtraceMatrixExp_effectiveRank_bound_of_ambientTraceCertificate
Family-level proved/open status for these hardbone targets is maintained in
TheoremAtlas.md. See Status.md for current
project focus, TODO.md for active work, and
RandomMatrixArchitecture.md for provider
ownership. The declaration lists above remain the endpoint index for callers.
traceMatrixExp_randomMatrixPrefixSum_lasttraceMatrixExp_comparisonMatrixPrefixSum_lasttroppTraceStatetroppStateHistorytroppNaturalState_zerotroppNaturalState_lasttroppNaturalState_lefttroppNaturalState_righttroppTraceExpFiniteFamilyIterationSkeleton_of_naturalStateConditionalStepstroppMasterTraceMGFFiniteFamily_of_naturalStateConditionalStepstraceMGFBernsteinVarianceProxyBound_of_naturalStateConditionalStepstroppMasterTraceMGFFiniteFamily_statement_of_reindexedFin
The two trace-exp wrappers convert final prefix endpoints into the state
equation shapes used by the conditional-step route. The reindex bridge
transports an existing Fin (Fintype.card I) Tropp finite-family statement to
an arbitrary finite index type; it does not prove that primitive.
The natural-state route fixes the Fin m state, history, and current-step
objects to the prefix/suffix construction and discharges the raw endpoint
equalities. Separately, TraceExpConditioning.troppStep_of_history_le closes
the exact conditional-step contract whenever
mHist <= MeasurableSpace.comap H _, using the contract's own IndepFun H Z
premise and an explicit TraceExpTroppFrozenBoundInputs packet. For the
standard Bernstein current step,
TraceExpConditioning.bernsteinStep_of_history_le constructs that packet from
centeredness, integrability, the pointwise operator-norm bound, and the Bernstein
parameter range. It does not remove the exact statement's IndepFun premise.
History measurability, arbitrary-larger-history independence, trace-exp
integrability, log/K, CFC, and variance-proxy obligations remain separate.
Use the core wrappers from:
import HighDimProb.RandomMatrix
-- or, for the narrower module:
import HighDimProb.RandomMatrix.TraceExpUse the examples from:
import HighDimProb.Examples.RandomMatrix.StatementRoutesStatementRoutes is the preferred reader entry point. It imports a small set of focused route examples and avoids exposing every intermediate bridge as a separate public example.
Provider-compression APIs:
LogResolvent.trace_mul_derivSAAt_eq_cutoffKernel_add_remainderLogResolvent.trace_mul_lineDeriv_eq_cutoffKernel_add_remainderLogResolvent.derivSAAtCutoffRemainder_eq_sum_conjDiagonalLogResolvent.derivSAAtCutoffRemainder_eq_sum_inv_sub_kernel_conjDiagonal_of_strictlyPositiveLogResolvent.SameEigenbasisDiagonalLogResolvent.scalarSquareKernelIntegralLogResolvent.scalarSquareKernelRemainderTendstoZeroLogResolvent.sameEigenbasisCutoffRemainderTendstoZeroindepFun_of_history_entry_measurable_of_indephistoryCondExp_ae_eq_frozenParameterIntegral_of_indepFunhistoryCondExp_le_of_indepFun_under_uniform_boundcondExp_le_of_indep_sigma_under_frozen_boundcondExp_traceExp_history_add_independent_step_of_indep_sigmaTraceExpTroppFrozenBoundInputsTraceExpConditioning.troppStep_of_history_leTraceExpConditioning.condExpStep_of_history_leTraceExpConditioning.bernsteinInputs_of_primitivesTraceExpConditioning.bernsteinStep_of_history_letrace_mul_mono_right_of_matrixLE_of_isPSDMatrixtrace_mul_inv_add_const_convex_combo_lematrixExpExcessSupportDomination_of_supportDomination_of_support_le_onematrixExpExcessSupportDomination_identityquadraticFormUpperTailEvent_subset_traceExpThresholdEvent_of_randomSelfAdjointmatrixBernsteinQuadraticFormUpperTail_of_naturalStateProviderAssumptions_tailSubsetDischarged_of_randomSelfAdjoint
These are provider-compression APIs. They remove local bookkeeping and selected
tail, support, and conditioning premises. The focused LiebProvider facade
separately closes the finite-dimensional left/right Lieb/Epstein route and
Golden--Thompson; MatrixBernsteinProvider closes generated-history endpoints
under explicit primitives. These compression names do not by themselves remove
arbitrary-history conditional expectation, automatic variance-proxy
normalization, or produce unconditional full Matrix Bernstein.
Preferred compact bounded-row route:
SampleCovarianceTailTargetSampleCovarianceTailTarget.eventSampleCovarianceTailTarget.rhsSampleCovarianceBoundedRowTroppAssumptionssampleCovariance_tail_optimized_under_boundedRowTroppAssumptions
Use the compact theorem with target
SampleCovarianceTailTarget.quadraticFormUpper or
SampleCovarianceTailTarget.selfAdjointOperatorNorm. This keeps the target axis
explicit without publishing a separate recommended theorem name for every
combination of target, sign, CFC route, negative adapter, and provider route.
The compact record is the full bounded-row Tropp route: it exposes the common
row assumptions and the remaining negative-side Tropp/integrability providers,
but it does not include a finite-family tail conclusion as a field.
Advanced bridge-layer routes also expose exact-row centered-square infrastructure. Those declarations connect generic centered-square variance-proxy chains and negative-family transfer adapters to sample-covariance wrappers. They are public proof infrastructure for later provider compression, not a replacement for the compact reader-facing bounded-row route.
Lower-level compatibility wrappers remain available when a proof needs fewer assumptions or a more explicit proof boundary:
sampleCovariance_quadraticForm_tail_optimized_under_explicit_variance_proxysampleCovariance_quadraticForm_tail_optimized_under_explicit_variance_proxy_of_troppPrimitivesampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_boundsampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound_of_troppPrimitivesampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_troppPrimitivesampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppPrimitiveSampleCovarianceExactRowCenteredSquareTroppAssumptionssampleCovariance_quadTail_centeredSq_exactRow_of_troppsampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitivessampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppPrimitivesSampleCovarianceExactRowCenteredSquareTwoSidedTroppAssumptionssampleCovariance_opNormTail_centeredSq_exactRow_of_troppsampleCovariance_selfAdjointOperatorNormTailEvent_subset_centeredRowRankOneSumsampleCovariance_selfAdjointOperatorNorm_tail_optimized_under_explicit_variance_proxysampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_explicit_variance_proxysampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives
These wrappers still require Tropp/Lieb trace-MGF primitives and analytic
integrability assumptions. The CFC-free wrappers remove the user-supplied
pointwise Bernstein CFC fields by applying bernsteinMatrixExp_le_quadratic.
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.
centeredSampleCovarianceRowRankOneFamilyNeg_expIntegrable_of_expIntegrable_neg_thetacenteredSampleCovarianceRowRankOneSumNeg_traceExpIntegrable_of_traceExpIntegrable_neg_thetacenteredSampleCovarianceRowRankOneFamilyNeg_cfcPrimitive_of_cfcPrimitive_neg_theta
These 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.
integrableRandomMatrix_const_mulintegrableRandomMatrix_mul_constmatrixExpect_const_mulmatrixExpect_mul_constrandomMatrixSquare_centeredRandomMatrix_expandintegrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_integrable_four_productsintegrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_memLp_fourintegrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_sqNorm_bound_memLp_twointegrableRandomMatrix_randomMatrixSquare_centeredRandomMatrixintegrableRandomMatrix_randomMatrixSquare_centeredRankOneRandomMatrixFamily_of_memLp_fourintegrableRandomMatrix_randomMatrixSquare_centeredRankOneRandomMatrixFamily_of_sqNorm_bound_memLp_twomatrixSecondMoment_centeredRandomMatrixdeterministicMatrixVarianceProxyNorm_sum_le_sumdeterministicMatrixVarianceProxyNorm_matrixSecondMoment_rankOneRandomMatrix_le_sq_of_sqNorm_bounddeterministicMatrixVarianceProxyNorm_sum_matrixSecondMoment_rankOneRandomMatrix_le_sum_sq_of_sqNorm_boundsampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_twoMatrixVarianceProxyNormBound_of_pointwiseOperatorNormBoundMatrixVarianceProxyNormBound_centeredRankOneRandomMatrixFamily_of_sqNorm_boundMatrixVarianceProxyNormBound_centeredRankOneRandomMatrixFamily_of_sqNorm_bound_memLp_twoMatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamily_of_rowSqNorm_boundsampleCovarianceCenteredRankOneVarianceProxyBound
The focused import
HighDimProb.Examples.RandomMatrix.LoRAAdapterSubspaceCovarianceUsage exposes:
loraEmpiricalCovarianceloraMeanCovarianceloraCovarianceDeviationloraEmpiricalCovariance_sub_meanloraCovariance_normalizedTailloraCovarianceRadiusloraCovariance_highProbabilityloraCovariance_matrixLESandwich
For a positive batch size m, adapter dimension r + 1, squared-norm radius R, and epsilon >= 0, the normalized tail wrapper states
P(||SigmaHat_Q - SigmaBar_Q|| >= epsilon)
<= 2 (r + 1) exp(-m epsilon^2 / (8 R^2 + (4/3) R epsilon)).
This is the exact consequence of the generic centered rank-one variance
proxy 4 m R^2. It gives the expected
R * (sqrt(log((r + 1)/delta) / m) + log((r + 1)/delta) / m) rate and the
Loewner sandwich around loraMeanCovariance. It does not claim the sharper
m R^2 rank-one proxy; that separate improvement is required to match the
smaller square-root constant.
-
Use
StatementRoutesas a build-checked index of theorem-family routes before importing a focused example module. -
Name matrix families before using them in public wrappers.
-
Prefer named adapters over anonymous lambdas.
-
Prefer the sample-covariance
_of_troppPrimitive/_of_troppPrimitiveswrappers when pointwise Bernstein CFC is the only remaining explicit field. -
Keep positive-side and negative-side assumptions visibly distinct when the theorem still needs both sides.
-
Put domain vocabulary in examples as thin wrappers over the core RandomMatrix API, not as separate theorem machinery.
-
Use
StatementRoutesfirst. Low-level prefix/state, reindex, and negative-family bridge APIs are covered by source, tests, and judge files rather than separate reader-facing examples.
The public concentration facade is the caller endpoint and re-exports the provider concentration assembly:
import HighDimProb.RandomMatrix.ConcentrationImport the following implementation layers only for provider-proof development:
import HighDimProb.RandomMatrix.Provider.Analysis
import HighDimProb.RandomMatrix.Provider.Conditioning
import HighDimProb.RandomMatrix.Provider.ConcentrationImport the narrowest provider layer needed by the proof. The broad
HighDimProb.RandomMatrix.Provider facade imports all three;
HighDimProb.RandomMatrix.LiebProvider remains a compatibility import. The
full ownership and dependency contract is in
RandomMatrixArchitecture.md.
The analysis layer exposes ambient and self-adjoint
matrix-exp derivatives, first-order strictly-positive CFC.log affine-line
APIs, short inverse/trace-resolvent derivatives, finite-cutoff log-resolvent
identities, inverse-convexity segment/MatrixLE identities, full-matrix-Klein
relative-entropy APIs, the fixed-t left/right relative-entropy integrand
joint-convexity leaf, the left/right scalar, quadratic, spectral-overlap,
density, and integral-representation route to relative-entropy joint convexity
and Lieb/Epstein facades, the exact goldenThompsonTraceExp endpoint,
conditional relative-entropy/Gibbs bridges, derivative-level Epstein consumers,
trace-exp domain positivity, CFC-log resolvent cutoff/remainder bridges, and
fixed-numerator trace-resolvent convexity.
The conditioning layer exposes frozen-parameter conditional expectation,
independent-step trace-exponential conditioning, and natural-history
measurability and independence bridges. The concentration provider assembles
the conditional and left/right Tropp/Lieb bridges, integrability compression,
generated-history Bernstein finite-family/trace-MGF/tail wrappers, canonical
operator-norm/high-probability endpoints, support-to-excess compression, and
tail-event subset-discharge wrappers. These implementation surfaces are
re-exported for downstream use by HighDimProb.RandomMatrix.Concentration.
Matrix-exp and divided-difference API:
matrixExpFDerivhasFDerivAt_matrix_exphasStrictFDerivAt_matrix_exphasFDerivAt_matrix_exp_truncmatrixExpSelfAdjointmatrixExpFDerivSelfAdjointmatrixExpFDerivSelfAdjoint_spectral_equivhasFDerivAt_matrix_exp_selfAdjointhasStrictFDerivAt_matrix_exp_selfAdjointmatrixExpDividedDifferenceSeriesmatrixExpDividedDifferenceSeries_posmatrixExpDividedDifferenceSeries_ne_zeromatrixQuadraticForm_integrable_of_integrableRandomMatrixmatrixQuadraticForm_eq_star_dotProduct_mulVecmatrixExp_isStrictlyPositive_of_selfAdjointisStrictlyPositive_matrixExpect_matrixExp_of_randomSelfAdjoint
Preferred spectral adapter aliases:
MatrixExpFDeriv.conjDiagonalSymmTraceSum
Backing low-level theorem names, kept for exact proof work and compatibility:
matrixExpFDerivSelfAdjoint_diagonal_symm_entry_multrace_mul_matrixExpFDerivSelfAdjoint_conj_diagonal_symm_eq_sum
Strictly-positive CFC.log derivative API:
cfcLogSelfAdjointCFCLog.CarrierCFCLog.DerivOpCFCLog.derivSAAtCFCLog.hasStrictFDerivAt_derivSAAtCFCLog.lineDerivCFCLog.lineDeriv_one_zeroCFCLog.hasDerivAt_lineexists_hasDerivAt_cfcLog_affineLine_of_strictlyPositivehasDerivAt_cfcLog_affineLine_of_strictlyPositive
Preferred diagonal and trace-paired spectral adapter aliases:
CFCLog.diagonalDerivEntryMulCFCLog.diagonalLineDerivEntryMulCFCLog.diagonalLineDerivTraceSum
Backing low-level theorem names, kept for exact proof work and compatibility:
CFCLog.derivSAAt_matrixExpSelfAdjoint_diagonal_entry_mulCFCLog.lineDerivSA_matrixExpSelfAdjoint_diagonal_entry_mulCFCLog.trace_mul_lineDerivSA_matrixExpSelfAdjoint_diagonal_eq_sum
Resolvent and finite-cutoff log-resolvent API:
hasDerivAt_inverse_affineLinehasDerivAt_inverse_affineLine_of_strictlyPositivetrace_resolvent_derivative_cycleneg_trace_resolvent_derivative_cyclehasDerivAt_trace_mul_inverse_affineLine_generalhasDerivAt_trace_mul_inverse_affineLine_general_neg_cyclehasDerivAt_trace_mul_inverse_affineLine_general_of_strictlyPositivehasDerivAt_trace_mul_inverse_affineLine_general_neg_cycle_of_strictlyPositivehasDerivAt_trace_mul_inverse_affineLinehasDerivAt_trace_mul_inverse_affineLine_of_strictlyPositiveLogResolvent.kernelFixedSumLogResolvent.kernelCutoffSumLogResolvent.shiftedInvTraceSumLogResolvent.identityCutoffSumLogResolvent.identityCutoffTraceLogSubLogResolvent.weightedCutoffSumLogResolvent.weightedCutoffTraceLogSubLogResolvent.weightedTraceLogEqShiftSubCutoffLogResolvent.weightedShiftTraceLogSubScalarLog_tendsto_zeroLogResolvent.weightedCutoffSubScalarLog_tendsto_negTraceLogLogResolvent.weightedShiftRemainderTendstoZeroLogResolvent.weightedCutoffRenormTendstoNegTraceLogLogResolvent.SameEigenbasisDiagonalLogResolvent.scalarSquareKernelIntegralLogResolvent.scalarSquareKernelRemainderTendstoZeroLogResolvent.sameEigenbasisCutoffRemainderTendstoZero
The SameEigenbasisDiagonal predicate packages the repeated conjugation-to-diagonal
hypothesis. The final cutoff-removal theorem removes the explicit cutoff only for
that same-eigenbasis diagonal remainder exposed by
CFCLogResolventRemainderProvider; it does not prove the general two-index
weighted cutoff limit.
Inverse-convexity positive-definite segment API:
inv_quadraticForm_affine_le_of_posDefinv_quadraticForm_iSup_affine_of_posDefconvexCombo_posDef_of_posDefinv_quadraticForm_convex_combo_le_of_posDefinv_matrixLE_convex_combo_le_of_posDef
These are quadratic-form variational and segment identities for positive
definite matrices, including the explicit MatrixLE packaging. They do not
prove full operator convexity of inverse or relative-entropy joint convexity.
Relative-entropy route API:
inversePerspectiveBlock_posSemidefinversePerspective_jointConvextrace_inversePerspective_jointConvexRelativeEntropy.tracePairedInversePerspectiveIntegrandRelativeEntropy.tracePairedInversePerspectiveIntegrand_jointConvexRelativeEntropy.leftRightDenominatorMatrixRelativeEntropy.leftRightDenominatorMatrix_posDefRelativeEntropy.leftRightDenominatorMatrix_affineRelativeEntropy.leftRightRelativeEntropyIntegrandRelativeEntropy.leftRightRelativeEntropyIntegrand_jointConvexRelativeEntropy.real_log_perspective_integralRelativeEntropy.real_relativeEntropy_integral_representationRelativeEntropy.real_relativeEntropy_integral_representation_densityRelativeEntropy.real_relativeEntropy_integrand_integrableOnRelativeEntropy.rowMatrixOfVecRelativeEntropy.trace_rowMatrixOfVec_mul_mul_conjTransposeRelativeEntropy.leftRightRelativeEntropyIntegrand_eq_rowTraceRelativeEntropy.leftRightRelativeEntropyIntegrand_eq_quadraticRelativeEntropy.leftRightRelativeEntropyIntegrand_posDef_spectralRelativeEntropy.posDef_spectral_difference_twoSided_entriesRelativeEntropy.leftRightRelativeEntropyIntegrand_posDef_spectral_overlapRelativeEntropy.traceMatrixRelativeEntropyPlainRelativeEntropy.relativeEntropyUnnormalized_eq_traceMatrixRelativeEntropyPlainTraceMatrixRelativeEntropyPlainJointConvexityrelativeEntropyJointConvexity_of_traceMatrixRelativeEntropyPlain_jointConvexLeftRightRelativeEntropyIntegrandDensityIntegrableTraceMatrixRelativeEntropyPlainLeftRightIntegralRepresentationleftRightRelativeEntropyIntegrandDensityIntegrabletraceMatrixRelativeEntropyPlainLeftRightIntegralRepresentationtraceMatrixRelativeEntropyPlain_jointConvex_of_leftRight_density_integral_representationrelativeEntropyJointConvexity_of_leftRight_density_integral_representationtraceMatrixRelativeEntropyPlain_jointConvex_of_leftRightrelativeEntropyJointConvexity_of_leftRightRelativeEntropy.fullKlein_liebCarrierConcavity_of_leftRight_density_integral_representationRelativeEntropy.fullKlein_liebConcavity_of_leftRight_density_integral_representationRelativeEntropy.fullKlein_epsteinConcavity_of_leftRight_density_integral_representationliebTraceExpConcavity_statement_of_leftRight_density_integral_representationepsteinAffineLineConcavity_of_leftRight_density_integral_representationRelativeEntropy.fullKlein_liebCarrierConcavity_of_leftRightRelativeEntropy.fullKlein_liebConcavity_of_leftRightRelativeEntropy.fullKlein_epsteinConcavity_of_leftRightliebTraceExpConcavity_statement_of_leftRightepsteinAffineLineConcavity_of_leftRightRelativeEntropy.scalarTermRelativeEntropy.diagonalTermRelativeEntropy.diagonalMatrixTermRelativeEntropy.diagonalMatrixTerm_cfcLog_nonnegRelativeEntropy.weightedSpectralKlein_nonnegRelativeEntropy.fullMatrixKlein_nonneg_of_isHermitian_of_strictlyPositiveRelativeEntropy.kleinInequality_relativeEntropy_nonnegkleinInequality_relativeEntropy_nonnegRelativeEntropy.logShiftRelativeEntropy.expLogMatrixRelativeEntropy.carrierGibbs_le_traceMatrixExp_of_kleinPremiseRelativeEntropy.carrierGibbs_eq_traceMatrixExp_at_matrixExp_logPointRelativeEntropyJointConvexityGibbsKleinPremisegibbsVariationalUpperBoundPremise_of_fullMatrixKleinRelativeEntropy.fullKlein_liebCarrierConcavityRelativeEntropy.fullKlein_liebConcavityRelativeEntropy.fullKlein_epsteinConcavityepsteinAffineLineConcavity_of_liebTraceExpConcavity_selfAdjointCarrier
These expose the finite-dimensional inverse-perspective leaf behind the
fixed-t left/right relative-entropy integrand, scalar/diagonal Klein
nonnegativity, full finite-dimensional matrix Klein under Hermitian
strictly-positive hypotheses, Gibbs/full-Klein bridge adapters, the proved
left/right density/integral representation, unconditional relative-entropy
joint convexity, and the resulting Lieb/Epstein facades. Tropp one-step
wrappers are exposed below. The separate identity-tangent consumer now proves
Golden--Thompson; the conditional-expectation step for arbitrary larger
histories, automatic variance-proxy normalization, tail-event domination, and
unconditional full Matrix Bernstein remain separate.
Golden--Thompson endpoint:
CFCLog.lineDeriv_one_zerogoldenThompsonTraceExp
Epstein/Tropp conditional consumers and support APIs:
cfcLogLineDerivTraceSecondEpsteinLine.traceSlopeEpsteinLine.traceSecondEpsteinLine.hasDerivAt_traceSlope_of_lineDerivSAEpsteinLine.hasDerivAt_traceSlope_of_hasDerivAt_evalEpsteinLine.concavity_of_traceSecond_nonpos_of_lineDerivSAEpsteinLine.concavity_of_traceSecond_nonpos_of_evalmatrixLog_le_of_le_matrixExp_of_providerLogMonotonetroppLogExpComparisonToK_of_providerLogOrderEpsteinAffineLineConcavityliebTraceExpConcavity_of_epsteinAffineLineliebJensenTraceExp_statement_of_epsteinAffineLinetroppMasterTraceMGFStep_of_epsteinAffineLinetroppMasterTraceMGFStep_trace_bound_of_epsteinAffineLine_and_providerLogOrdertroppMasterTraceMGFStep_of_leftRighttroppLiebJensenChain_of_leftRight(legacy compatibility)troppMasterTraceMGFStep_trace_bound_of_leftRight_and_providerLogOrderTroppNaturalHistory.suffixMeasurableTroppNaturalHistory.historyStepIndependenttroppNaturalHistoryMeasurable_of_suffix_entry_measurabletroppHistoryStepIndependent_of_iIndepFun_of_measurableTraceExpTroppFrozenBoundInputsTraceExpConditioning.troppStep_of_history_leTraceExpConditioning.condExpStep_of_history_leTraceExpConditioning.bernsteinInputs_of_primitivesTraceExpConditioning.bernsteinStep_of_history_lematrixExpScaledIntegrable_of_provider_finiteMeasureisSelfAdjointMatrix_matrixExpect_matrixExp_troppCurrentRandomStep_of_centeredSelfAdjointisStrictlyPositive_matrixExpect_matrixExp_troppCurrentRandomStep_of_centeredSelfAdjointtraceExpIntegrable_troppStateHistory_add_step_of_operatorNormBounds_finiteMeasuretraceExpIntegrable_troppStateHistory_add_K_of_operatorNormBounds_finiteMeasuretroppCurrentRandomStep_operatorNorm_le_of_summand_boundtroppStateHistory_operatorNorm_le_of_summand_and_comparison_boundstraceExpIntegrable_troppStateHistory_add_step_of_summand_and_comparison_bounds_finiteMeasuretraceExpIntegrable_troppStateHistory_add_K_of_summand_and_comparison_bounds_finiteMeasuretraceExpIntegrable_randomMatrixSum_of_operatorNormBounds_finiteMeasurelambdaMaxOrdered_le_of_matrixLE_selfAdjointlambdaMinOrdered_le_of_matrixLE_selfAdjointtraceMGFBernsteinVarianceProxyBoundLIntegral_of_realmatrixBernsteinTraceMGFToLaplaceContractmatrixBernsteinTraceMGFToLaplaceContract_under_primitivesMatrixBernsteinConditioningTraceMGFProviderAssumptionsMatrixBernsteinConditioningTraceMGFProviderAssumptions.toTailAssumptionsmatrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFProviderAssumptionsmatrixBernsteinQuadraticFormUpperTail_of_naturalStateProviderAssumptions
Interface audit: CFCLog.DerivOp is pointwise derivative bookkeeping only, not a
stable second-level Frechet codomain. The inverse-convexity API now includes
positive-definite segment and MatrixLE packaging, and the relative-entropy
route includes fixed-t left/right integrand joint convexity, full matrix
Klein, the proved density/integral representation, unconditional
relative-entropy joint convexity, unconditional Lieb/Epstein facades, and the
left/right Tropp one-step wrappers. The
LogResolvent layer gives spectral sum, CFC-log cutoff, and renormalized
cutoff-limit handles; it does not yet give a weighted CFCLog.lineDeriv /
CFCLog.derivSAAt resolvent-kernel adapter or the alternative Epstein sign
proof. The provider layer now closes Golden--Thompson through
goldenThompsonTraceExp; exact conditioning expectation for arbitrary
larger histories, automatic variance-proxy normalization, and unconditional
full Matrix Bernstein remain open. Self-adjoint quadratic-form tail subset
discharge is available through the TailEvent provider wrappers.
It is intentionally separate from reader-facing examples and the core
HighDimProb.RandomMatrix aggregate.