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. Provider modules are implementation details and are not part
of this caller contract. Their ownership and dependency rules are defined in
RandomMatrixArchitecture.md.
Basic.leanAssumptions.leanSums.leanOperatorNorm.leanSpectral.leanTraceExp.leanTraceExpDerivative.leanTraceExpMonotonicity.leanHardboneStatements.leanCStarBridge.leanVarianceProxy.leanDirectionalSubGaussian.leanDirectionalOperatorNorm.leanConcentrationStatements.lean
matrixBernsteinOptimizedScalarTailRHSmatrixBernsteinTwoSidedOptimizedScalarTailRHSmatrixBernsteinTwoSidedOptimizedScalarTailRHS_sameParametersone_le_matrixBernsteinTwoSidedOptimizedScalarTailRHS_zeroMatrixBernsteinPositiveSideTroppAssumptionsMatrixBernsteinNegativeSideTroppAssumptionssampleCovarianceCenteredRankOneRadiussampleCovarianceTailThetasampleCovarianceQuadraticFormTailRHSrowSqNormVarianceProxyNormRHSupperTailProb_operatorNorm_smul_one_div_natCast
Use these helpers in examples and tests instead of copying RHS formulas.
upperTailProb_operatorNorm_smul_one_div_natCast is the shared normalized
operator-norm tail-scaling step reused by the normalized empirical-covariance
and NTK Gram endpoints.
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.
DirectionallySubGaussianSelfAdjointMatrixmatrixQuadraticForm_centeredRandomMatrixdirectionallySubGaussianSelfAdjointMatrix_sum_of_iIndepFunIsUnitSphereNetdeterministicOperatorNorm_le_of_isUnitSphereNetdirectionallySubGaussianSelfAdjointMatrix_operatorNorm_netTaildirectionallySubGaussianSelfAdjointMatrix_operatorNorm_netTail_sum_of_iIndepFun
This is the finite-dimensional fixed-direction route. It packages scalar
sub-Gaussian control of every fixed unit-vector quadratic form, closes the
predicate under independent finite sums, and converts it to an operator-norm
tail using an explicit finite unit-sphere net. The tail prefactor is
2 * N.card; the API does not yet construct N or replace its cardinality by
a dimension-only bound. The tail theorems use Fin (n + 1), require
0 <= eps < 1 / 2, 0 <= t, a probability measure, and explicit entrywise
integrability. This route does not imply MatrixSubGaussianMGF, a Loewner MGF
bound, or an n-prefactor trace-MGF theorem.
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.CenteredRankOneInputs.ofIIndepFunMatrixBernstein.CenteredRankOneExactRowInputsMatrixBernstein.CenteredRankOneExactRowInputs.ofIIndepFunMatrixBernstein.centeredRankOneMatrixBernstein.centeredRankOneExactRowMatrixBernstein.centeredRankOneExactRowHighProbabilityMatrixBernstein.sampleCovarianceExactRowMatrixBernstein.sampleCovarianceExactRowHighProbabilityMatrixBernstein.highProbability_of_primitivesMatrixBernstein.CenteredSelfAdjointObservationInputsMatrixBernstein.CenteredSelfAdjointObservationInputs.ofIIndepFunMatrixBernstein.centeredSelfAdjointObservationsMatrixBernstein.centeredSelfAdjointObservationsHighProbabilityiIndepFun_centeredRankOneiIndepFun_centeredRandomMatrixmatrixBernsteinSelfAdjointOptimizedStatementmatrixBernsteinTraceMGFWithBernsteinCoeff_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. Older compatibility
names may still exist, but they are not the recommended downstream surface.
The generated-history Bernstein wrappers are assembled internally and
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.
The focused public matrix sub-Gaussian surface is exported by the same facade:
import HighDimProb.RandomMatrix.ConcentrationIt contains exactly these four declarations:
MatrixSubGaussianMGFMatrixSubGaussianMGF.negtraceMGFVarianceProxyBound_of_matrixSubGaussian_under_troppPrimitivesubGaussian_quadraticFormUpperTail_under_troppPrimitive
MatrixSubGaussianMGF states only a conditional Loewner matrix-MGF inequality.
It does not bundle centeredness, self-adjointness, positive semidefiniteness,
measurability, integrability, or a probability-measure assumption. The
finite-family trace-MGF and quadratic-form tail declarations still require an
explicit finite-family Tropp comparison primitive, random-matrix,
self-adjointness, and independence assumptions, self-adjoint variance proxies,
and matrix/trace-exponential integrability for the unbounded summands. The tail
declaration additionally requires the aggregate proxy spectral bound and uses
the optimizer theta = t / sigmaSq, with those integrability premises required
at that value. This surface is not unconditional Matrix Chernoff or full
Tropp, and it makes no infinite-dimensional claim.
The focused compile-time consumer is
SubGaussianMatrixAPI.lean.
The append-only downstream consumer is
HighDimProbJudge/RandomMatrix/SubGaussianUse.lean.
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 controls
the uncentered second moment (Gram / empirical-Fisher-style outer product)
(1 / m) * sum_b x_b x_b^T of the adapter-coordinate gradients, not the gradient
covariance (they agree only when E[x_b] = 0). The Covariance in the
identifier names below is a legacy label. It exposes:
loraEmpiricalCovarianceloraMeanCovarianceloraCovarianceDeviationloraEmpiricalCovariance_sub_meanLoRACovarianceInputs/LoRACovarianceInputs.ofIIndepFunloraCovariance_operatorNormTailloraCovariance_normalizedTailloraCovarianceRadiusloraCovariance_highProbabilityloraCovariance_matrixLESandwich
The normalized tail is stated in the reusable
matrixBernsteinTwoSidedOptimizedScalarTailRHS form with the row-specific
variance proxy rowSqNormVarianceProxyNormRHS Rvar = sum_b Rvar_b^2.
Instantiated with a uniform Rvar_b = R (proxy m R^2) it reads
P(||Mhat_Q - Mbar_Q|| >= epsilon)
<= 2 (r + 1) exp(-m epsilon^2 / (2 R^2 + (4/3) R epsilon)),
together with the high-probability radius and the Loewner sandwich around
loraMeanCovariance. The centered summand radius 2 R and the proxy
sum_b Rvar_b^2 are valid upper bounds, not the optimal rank-one constants:
the PSD structure gives the sharp radius R and variance bound
(1/4) sum_b r_b^2. Formalizing those sharper providers is tracked in
TODO.md.
-
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.
Downstream code should use only:
import HighDimProb.RandomMatrix.ConcentrationProvider module names and proof leaves are intentionally omitted from this
caller guide. Contributors working on those internals should use
RandomMatrixArchitecture.md,
the focused provider API tests, and source-level #check output.