# RandomMatrix Concentration API 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`](../archive/README.md); use git history for exact old wording. For supported scope and current status, see [`Status.md`](Status.md); for active work, see [`TODO.md`](../maintainers/TODO.md); and for module ownership and dependency direction, see [`RandomMatrixArchitecture.md`](../architecture/RandomMatrixArchitecture.md). Family-level proved/open status is owned by [`TheoremAtlas.md`](../reference/TheoremAtlas.md). Downstream users of the matrix-concentration results documented here should normally use: ```lean import HighDimProb.RandomMatrix.Concentration ``` The 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`](../architecture/RandomMatrixArchitecture.md). ## Core Modules - [`Basic.lean`](../../HighDimProb/RandomMatrix/Basic.lean) - [`Assumptions.lean`](../../HighDimProb/RandomMatrix/Assumptions.lean) - [`Sums.lean`](../../HighDimProb/RandomMatrix/Sums.lean) - [`OperatorNorm.lean`](../../HighDimProb/RandomMatrix/OperatorNorm.lean) - [`Spectral.lean`](../../HighDimProb/RandomMatrix/Spectral.lean) - [`TraceExp.lean`](../../HighDimProb/RandomMatrix/TraceExp.lean) - [`TraceExpDerivative.lean`](../../HighDimProb/RandomMatrix/TraceExpDerivative.lean) - [`TraceExpMonotonicity.lean`](../../HighDimProb/RandomMatrix/TraceExpMonotonicity.lean) - [`HardboneStatements.lean`](../../HighDimProb/RandomMatrix/HardboneStatements.lean) - [`CStarBridge.lean`](../../HighDimProb/RandomMatrix/CStarBridge.lean) - [`VarianceProxy.lean`](../../HighDimProb/RandomMatrix/VarianceProxy.lean) - [`DirectionalSubGaussian.lean`](../../HighDimProb/RandomMatrix/DirectionalSubGaussian.lean) - [`DirectionalOperatorNorm.lean`](../../HighDimProb/RandomMatrix/DirectionalOperatorNorm.lean) - [`ConcentrationStatements.lean`](../../HighDimProb/RandomMatrix/ConcentrationStatements.lean) ## Shared Helpers - `matrixBernsteinOptimizedScalarTailRHS` - `matrixBernsteinTwoSidedOptimizedScalarTailRHS` - `matrixBernsteinTwoSidedOptimizedScalarTailRHS_sameParameters` - `one_le_matrixBernsteinTwoSidedOptimizedScalarTailRHS_zero` - `MatrixBernsteinPositiveSideTroppAssumptions` - `MatrixBernsteinNegativeSideTroppAssumptions` - `sampleCovarianceCenteredRankOneRadius` - `sampleCovarianceTailTheta` - `sampleCovarianceQuadraticFormTailRHS` - `rowSqNormVarianceProxyNormRHS` - `upperTailProb_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_integrableRandomMatrix` - `matrixExpect_eq_integral_l2Operator` - `matrixExpect_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_posSemidef` - `posSemidef_of_isPSDMatrix` - `matrixLE_of_mathlib_le` - `mathlib_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: - `lambdaMax` - `lambdaMaxOrdered` - `lambdaMaxOrdered_eq_eigenvaluesâ‚€_zero` - `lambdaMaxOrdered_is_greatest_eigenvalue_statement` - `lambdaMaxOrdered_is_greatest_eigenvalue` - `lambdaMin` - `lambdaMinOrdered` - `lambdaMinOrdered_is_least_eigenvalue_statement` - `lambdaMinOrdered_is_least_eigenvalue` - `lambdaMinOrdered_le_eigenvaluesâ‚€` These wrappers keep the legacy `lambdaMax` / `lambdaMin` names while exposing the canonical ordered `eigenvaluesâ‚€` endpoints. ## Directional Sub-Gaussian Surface - `DirectionallySubGaussianSelfAdjointMatrix` - `matrixQuadraticForm_centeredRandomMatrix` - `directionallySubGaussianSelfAdjointMatrix_sum_of_iIndepFun` - `IsUnitSphereNet` - `deterministicOperatorNorm_le_of_isUnitSphereNet` - `directionallySubGaussianSelfAdjointMatrix_operatorNorm_netTail` - `directionallySubGaussianSelfAdjointMatrix_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: - `realMatrixToCStarMatrix` - `realMatrixToCStarStarAlgHom` - `realMatrixToCStar_nonneg` - `realMatrixToCStar_strictlyPositive` - `realMatrixToCStar_matrixLE` - `realMatrixToCStar_log` - `isSelfAdjointMatrix_cfc_log` - `cstarMatrixOfMatrix_posSemidef_of_nonneg` - `posSemidef_of_complexification_posSemidef` - `matrixLE_of_realMatrixToCStar_matrixLE` - `realMatrixToCStarMatrix_apply` - `realMatrixToCStarMatrix_add` - `realMatrixToCStarMatrix_sub` - `isSelfAdjoint_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. ## Zero-Variance Surface - `matrixVarianceProxy_eq_zero_of_normBound_zero` - `randomMatrixFamily_ae_eq_zero_of_matrixVarianceProxy_eq_zero` - `randomMatrixFamily_ae_eq_zero_of_matrixVarianceProxyNormBound_zero` - `randomMatrixSum_ae_eq_zero_of_family_ae_eq_zero` - `upperTailProb_operatorNorm_randomMatrixSum_eq_zero_of_ae_eq_zero` - `upperTailProb_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. ## Matrix Bernstein Surface - `bernsteinAdditiveTailThreshold` - `bernsteinAdditiveTailThreshold_nonneg` - `bernsteinAdditiveTailThreshold_sq` - `bernsteinAdditiveTailThreshold_pos` - `bernsteinAdditiveTailThreshold_exponent_eq` - `matrixBernsteinLogFactor` - `matrixBernsteinLogFactor_pos` - `matrixBernsteinHighProbabilityThreshold` - `matrixBernsteinHighProbabilityThreshold_nonneg` - `matrixBernsteinTwoSidedOptimizedScalarTailRHS_highProbabilityThreshold` - `matrixBernsteinSelfAdjointHighProbabilityStatement` - `matrixBernsteinSelfAdjointHighProbabilityStatement_of_optimizedStatement` - `MatrixBernstein.operatorNormTail_of_primitives` - `MatrixBernstein.operatorNormTail_of_primitives_nonneg` - `MatrixBernstein.operatorNormUpperTail_of_primitives` - `MatrixBernstein.optimized_of_primitives` - `MatrixBernstein.CenteredRankOneInputs` - `MatrixBernstein.CenteredRankOneInputs.ofIIndepFun` - `MatrixBernstein.CenteredRankOneExactRowInputs` - `MatrixBernstein.CenteredRankOneExactRowInputs.ofIIndepFun` - `MatrixBernstein.centeredRankOne` - `MatrixBernstein.centeredRankOneExactRow` - `MatrixBernstein.centeredRankOneExactRowHighProbability` - `MatrixBernstein.sampleCovarianceExactRow` - `MatrixBernstein.sampleCovarianceExactRowHighProbability` - `MatrixBernstein.highProbability_of_primitives` - `MatrixBernstein.CenteredSelfAdjointObservationInputs` - `MatrixBernstein.CenteredSelfAdjointObservationInputs.ofIIndepFun` - `MatrixBernstein.centeredSelfAdjointObservations` - `MatrixBernstein.centeredSelfAdjointObservationsHighProbability` - `iIndepFun_centeredRankOne` - `iIndepFun_centeredRandomMatrix` - `matrixBernsteinSelfAdjointOptimizedStatement` - `matrixBernsteinTraceMGFWithBernsteinCoeff_under_primitives` - `TraceExpConditioning.bernsteinInputs_of_primitives` - `TraceExpConditioning.bernsteinStep_of_history_le` - `troppMasterTraceMGFFiniteFamily_generatedHistory_of_bernsteinPrimitives` - `matrixBernsteinTraceMGFWithBernsteinCoeff_generatedHistory_of_bernsteinPrimitives` - `matrixBernsteinQuadraticFormUpperTail_generatedHistory_of_bernsteinPrimitives` - `matrixBernsteinQuadraticFormUpperTail_generatedHistory_of_bernsteinPrimitives_tailSubsetDischarged_of_randomSelfAdjoint` - `matrixBernsteinTraceMGF_under_tropp` - `matrixBernsteinQuadTail_trace_under_tropp` - `matrixBernsteinQuadTail_scalar_under_tropp` - `matrixBernsteinQuadTail_opt_under_tropp` - `matrixBernsteinQuadraticFormUpperTailOptimizedScalarRHSWithBernsteinCoeff_under_primitives` - `matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge` - `MatrixBernsteinConditioningTraceMGFTailAssumptions` - `matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFTailAssumptions` - `MatrixBernsteinConditioningTraceMGFProviderAssumptions` - `MatrixBernsteinConditioningTraceMGFProviderAssumptions.toTailAssumptions` - `matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFProviderAssumptions` - `matrixBernsteinQuadraticFormUpperTail_of_naturalStateProviderAssumptions` - `matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge_tailSubsetDischarged_of_randomSelfAdjoint` - `matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFProviderAssumptions_tailSubsetDischarged_of_randomSelfAdjoint` - `matrixBernsteinQuadraticFormUpperTail_of_naturalStateProviderAssumptions_tailSubsetDischarged_of_randomSelfAdjoint` - `matrixBernsteinQuadraticFormUpperTailOptimizedScalarRHSWithBernsteinCoeff_of_assumptions` - `matrixBernsteinQuadTail_opt_of_tropp` - `matrixBernsteinTwoSidedQuadraticFormTailOptimizedScalarRHSWithBernsteinCoeff_under_primitives` - `matrixBernsteinQuadTail_twoSided_opt_of_tropp` - `matrixBernsteinSelfAdjointOperatorNormTailOptimizedScalarRHSWithBernsteinCoeff_arbitrary_of_pos_under_primitives` - `matrixBernsteinOpNormTail_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. ## Matrix Sub-Gaussian Surface The focused public matrix sub-Gaussian surface is exported by the same facade: ```lean import HighDimProb.RandomMatrix.Concentration ``` It contains exactly these four declarations: - `MatrixSubGaussianMGF` - `MatrixSubGaussianMGF.neg` - `traceMGFVarianceProxyBound_of_matrixSubGaussian_under_troppPrimitive` - `subGaussian_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`](../../HighDimProbTest/SubGaussianMatrixAPI.lean). The append-only downstream consumer is `HighDimProbJudge/RandomMatrix/SubGaussianUse.lean`. ## Hardbone Statement Targets Bernstein CFC chain: - `scalarBernsteinExpQuadraticInequality_statement` - `scalarBernsteinExpQuadraticInequality` - `selfAdjointSpectrumBoundedByOperatorNorm_statement` - `selfAdjointSpectrumBoundedByOperatorNorm` - `cfcScalarInequalityToMatrixLE_statement` - `cfcScalarInequalityToMatrixLE_bernsteinExpQuadratic` - `bernsteinCFCExpressionNormalization_statement` - `bernsteinCFCExpressionNormalization` - `bernsteinMatrixExp_le_quadratic_of_cfcChain_statement` - `bernsteinMatrixExp_le_quadratic_of_cfcLeaves` - `bernsteinMatrixExp_le_quadratic` Log/order-to-`K` chain: - `operatorLogMonotoneOnPositiveMatrices_statement` - `operatorLogMonotoneOnPositiveMatrices` - `matrixExpLogDomainForSelfAdjoint_statement` - `matrixExpLogDomainForSelfAdjoint` - `matrixLog_le_of_le_matrixExp_statement` - `matrixLog_le_of_le_matrixExp` - `traceMatrixExp_mono_add_selfAdjoint_statement` - `traceMatrixExp_mono_add_selfAdjoint` - `troppLogExpComparisonToK` Tropp/Lieb/Golden-Thompson chain: - `liebTraceExpConcavity_statement` - `liebJensenTraceExp_statement` - `goldenThompsonTraceExp_statement` - `goldenThompsonTraceExp` - `matrixExpLogSelfAdjointNormalization_statement` - `matrixExpLogSelfAdjointNormalization` - `troppMasterTraceMGFStep_of_liebJensen_statement` Conditioning / independence chain: - `troppNaturalHistoryMeasurable_statement` - `troppHistoryStepIndependent_of_iIndepFun_statement` - `TroppNaturalHistory.historyStepContractOfIsRandomMatrix` - `condExp_traceExp_history_add_independent_step_statement` - `troppConditionalStep_of_iIndepFun_statement` - `troppConditionalStep_of_iIndepFun` Integrability provider chain: - `matrixExpScaledIntegrable_of_provider_statement` - `traceExpIntegrable_troppStateHistory_add_step_statement` - `traceExpIntegrable_troppStateHistory_add_K_statement` - `traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider_statement` Variance-proxy / centered-square chain: - `matrixSquare_centeredRandomMatrix_expectation_expansion_statement` - `matrixSquare_centeredRandomMatrix_expectation_expansion` - `centeredRankOneSquare_le_rankOneSecondMoment_statement` - `centeredRankOneSquare_le_rankOneSecondMoment` - `sampleCovarianceVarianceProxy_sharp_statement` - `sampleCovarianceVarianceProxy_sharp_of_rankOneSecondMoment` - `sampleCovarianceVarianceProxy_sharp_of_exactRowSecondMoment` - `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two` - `sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two` - `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two_of_centeredSquareChain` - `MatrixVarianceProxyNormBound_centeredRankOneRandomMatrixFamily_of_rowSqNorm_bound_memLp_two` - `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamily_of_exactRowSqNorm_bound_memLp_two` - `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_direct_of_exactRowSqNorm_bound_memLp_two` - `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two` - `varianceProxyNormBound_of_centeredSquareChain_statement` - `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement` - `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE` - `varianceProxyNormBound_of_centeredSquareChain_of_normMono` - `varianceProxyNormBound_of_centeredSquareChain_expansion` Dimension / rank / effective-rank chain: - `traceMatrixExp_le_rank_exp_lambdaMax_statement` - `traceMatrixExp_le_supportDim_exp_lambdaMax_statement` - `traceMatrixExp_effectiveRank_bound_statement` Deterministic trace / rank bridges: - `matrixTrace_smul` - `matrixTrace_le_of_matrixLE` - `traceMatrixExp_le_trace_support_exp_lambdaMax_of_supportDomination` (preferred reader-facing name; the older `_of_matrixExp_le_smul_support` spelling remains as a compatibility alias) - `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` Generated-history centered rank-one consumers: - `MatrixBernstein.CenteredRankOneExactRowInputs` - `MatrixBernstein.centeredRankOneExactRow` - `MatrixBernstein.sampleCovarianceExactRow` - `MatrixBernstein.sampleCovarianceExactRowHighProbability` - `iIndepFun_centeredRankOne` Thin hardbone consumers: - `bernsteinMatrixExp_le_quadratic_of_cfcChain` - `bernsteinMatrixExp_le_quadratic_of_cfcLeaves` - `bernsteinMatrixExp_le_quadratic` - `matrixLog_le_of_le_matrixExp` - `troppMasterTraceMGFStep_of_liebJensen` - `troppConditionalStep_of_iIndepFun` - `troppMasterTraceMGFConditionalStep_of_conditioningBridge` - `traceMGFBernsteinVarianceProxyBound_of_conditioningBridge` - `traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider` - `varianceProxyNormBound_of_centeredSquareChain` - `varianceProxyNormBound_of_centeredSquareChain_of_normMono` - `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE` - `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` Family-level proved/open status for these hardbone targets is maintained in [`TheoremAtlas.md`](../reference/TheoremAtlas.md). See [`Status.md`](Status.md) for current project focus, [`TODO.md`](../maintainers/TODO.md) for active work, and [`RandomMatrixArchitecture.md`](../architecture/RandomMatrixArchitecture.md) for provider ownership. The declaration lists above remain the endpoint index for callers. ## TraceExp / Tropp Bookkeeping Surface - `traceMatrixExp_randomMatrixPrefixSum_last` - `traceMatrixExp_comparisonMatrixPrefixSum_last` - `troppTraceState` - `troppStateHistory` - `troppNaturalState_zero` - `troppNaturalState_last` - `troppNaturalState_left` - `troppNaturalState_right` - `troppTraceExpFiniteFamilyIterationSkeleton_of_naturalStateConditionalSteps` - `troppMasterTraceMGFFiniteFamily_of_naturalStateConditionalSteps` - `traceMGFBernsteinVarianceProxyBound_of_naturalStateConditionalSteps` - `troppMasterTraceMGFFiniteFamily_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: ```lean import HighDimProb.RandomMatrix -- or, for the narrower module: import HighDimProb.RandomMatrix.TraceExp ``` Use the examples from: ```lean import HighDimProb.Examples.RandomMatrix.StatementRoutes ``` `StatementRoutes` 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_remainder` - `LogResolvent.trace_mul_lineDeriv_eq_cutoffKernel_add_remainder` - `LogResolvent.derivSAAtCutoffRemainder_eq_sum_conjDiagonal` - `LogResolvent.derivSAAtCutoffRemainder_eq_sum_inv_sub_kernel_conjDiagonal_of_strictlyPositive` - `LogResolvent.SameEigenbasisDiagonal` - `LogResolvent.scalarSquareKernelIntegral` - `LogResolvent.scalarSquareKernelRemainderTendstoZero` - `LogResolvent.sameEigenbasisCutoffRemainderTendstoZero` - `indepFun_of_history_entry_measurable_of_indep` - `historyCondExp_ae_eq_frozenParameterIntegral_of_indepFun` - `historyCondExp_le_of_indepFun_under_uniform_bound` - `condExp_le_of_indep_sigma_under_frozen_bound` - `condExp_traceExp_history_add_independent_step_of_indep_sigma` - `TraceExpTroppFrozenBoundInputs` - `TraceExpConditioning.troppStep_of_history_le` - `TraceExpConditioning.condExpStep_of_history_le` - `TraceExpConditioning.bernsteinInputs_of_primitives` - `TraceExpConditioning.bernsteinStep_of_history_le` - `trace_mul_mono_right_of_matrixLE_of_isPSDMatrix` - `trace_mul_inv_add_const_convex_combo_le` - `matrixExpExcessSupportDomination_of_supportDomination_of_support_le_one` - `matrixExpExcessSupportDomination_identity` - `quadraticFormUpperTailEvent_subset_traceExpThresholdEvent_of_randomSelfAdjoint` - `matrixBernsteinQuadraticFormUpperTail_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. ## Sample Covariance Surface Preferred compact bounded-row route: - `SampleCovarianceTailTarget` - `SampleCovarianceTailTarget.event` - `SampleCovarianceTailTarget.rhs` - `SampleCovarianceBoundedRowTroppAssumptions` - `sampleCovariance_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_proxy` - `sampleCovariance_quadraticForm_tail_optimized_under_explicit_variance_proxy_of_troppPrimitive` - `sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound` - `sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound_of_troppPrimitive` - `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_troppPrimitive` - `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppPrimitive` - `SampleCovarianceExactRowCenteredSquareTroppAssumptions` - `sampleCovariance_quadTail_centeredSq_exactRow_of_tropp` - `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives` - `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppPrimitives` - `SampleCovarianceExactRowCenteredSquareTwoSidedTroppAssumptions` - `sampleCovariance_opNormTail_centeredSq_exactRow_of_tropp` - `sampleCovariance_selfAdjointOperatorNormTailEvent_subset_centeredRowRankOneSum` - `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_under_explicit_variance_proxy` - `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_explicit_variance_proxy` - `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives` These wrappers still require Tropp/Lieb trace-MGF primitives and analytic integrability assumptions. 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. ### Sample covariance negative-side provider adapters - `centeredSampleCovarianceRowRankOneFamilyNeg_expIntegrable_of_expIntegrable_neg_theta` - `centeredSampleCovarianceRowRankOneSumNeg_traceExpIntegrable_of_traceExpIntegrable_neg_theta` - `centeredSampleCovarianceRowRankOneFamilyNeg_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. ## Variance Proxy Surface - `integrableRandomMatrix_const_mul` - `integrableRandomMatrix_mul_const` - `matrixExpect_const_mul` - `matrixExpect_mul_const` - `randomMatrixSquare_centeredRandomMatrix_expand` - `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_integrable_four_products` - `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_memLp_four` - `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_sqNorm_bound_memLp_two` - `integrableRandomMatrix_randomMatrixSquare_centeredRandomMatrix` - `integrableRandomMatrix_randomMatrixSquare_centeredRankOneRandomMatrixFamily_of_memLp_four` - `integrableRandomMatrix_randomMatrixSquare_centeredRankOneRandomMatrixFamily_of_sqNorm_bound_memLp_two` - `matrixSecondMoment_centeredRandomMatrix` - `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` - `MatrixVarianceProxyNormBound_of_pointwiseOperatorNormBound` - `MatrixVarianceProxyNormBound_centeredRankOneRandomMatrixFamily_of_sqNorm_bound` - `MatrixVarianceProxyNormBound_centeredRankOneRandomMatrixFamily_of_sqNorm_bound_memLp_two` - `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamily_of_rowSqNorm_bound` - `sampleCovarianceCenteredRankOneVarianceProxyBound` ## LoRA Adapter-Gradient Second-Moment Application Surface 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: - `loraEmpiricalCovariance` - `loraMeanCovariance` - `loraCovarianceDeviation` - `loraEmpiricalCovariance_sub_mean` - `LoRACovarianceInputs` / `LoRACovarianceInputs.ofIIndepFun` - `loraCovariance_operatorNormTail` - `loraCovariance_normalizedTail` - `loraCovarianceRadius` - `loraCovariance_highProbability` - `loraCovariance_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`](../maintainers/TODO.md). ## Example Style - Use `StatementRoutes` as 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_troppPrimitives` wrappers when pointwise Bernstein CFC is the only remaining explicit field. - Keep positive-side and negative-side assumptions visibly distinct when the theorem still needs both sides. - Put domain vocabulary in examples as thin wrappers over the core RandomMatrix API, not as separate theorem machinery. - Use `StatementRoutes` first. Low-level prefix/state, reindex, and negative-family bridge APIs are covered by source, tests, and judge files rather than separate reader-facing examples. ## Internal Implementation Boundary Downstream code should use only: ```lean import HighDimProb.RandomMatrix.Concentration ``` Provider module names and proof leaves are intentionally omitted from this caller guide. Contributors working on those internals should use [`RandomMatrixArchitecture.md`](../architecture/RandomMatrixArchitecture.md), the focused provider API tests, and source-level `#check` output.