# Theorem Atlas This page owns family-level proved/open status for the theorem atlas. Use it to read route-level theorem coverage and blockers, not to select active tasks or caller imports. Old atlas detail was collapsed into [`archive.md`](../archive/README.md); use git history for exact old wording. For supported scope, see [`Status.md`](../user/Status.md); for active work, see [`TODO.md`](../maintainers/TODO.md); for module ownership and dependency direction, see [`RandomMatrixArchitecture.md`](../architecture/RandomMatrixArchitecture.md); and for caller endpoints, imports, and assumptions, see [`RandomMatrixAPI.md`](../user/RandomMatrixAPI.md). ## Status Vocabulary - `proven`: implemented as a Lean theorem or lemma. - `typed-prop`: represented as a compiled statement object, not proved. - `scaffold`: vocabulary or statement layer only. - `blocked`: waiting on real mathematical infrastructure. ## Scalar Concentration The scalar concentration layer is the most mature part of the library. It contains proved Markov/Chebyshev wrappers, Orlicz-to-tail and tail-to-Orlicz bridges, moment implications, Rademacher/Hoeffding routes, and scalar Bernstein families. The Lean source, focused tests, and judge files are the detailed index; this atlas stays route-level. ## Random Object Vocabulary The random-family layer is `scaffold`: `RandomFamily`, real-valued variants, process/sample aliases, endpoint accessors, and deterministic map preservation lemmas are compiled vocabulary over Mathlib `Measurable`. It intentionally does not add filtrations, adaptedness, martingales, or conditioning providers. ## SubGaussian Process And Finite Chaining `HighDimProb.SubGaussianProcess` defines the metric increment predicate `HasSubGaussianMGFIncrements` and proves the radius adapter `HasSubGaussianMGFIncrements.centeredSubGaussianMGF_of_dist_le`. The predicate allows the zero `NNReal` proxy at equal indices and does not assume `0 < σ`; the adapter requires `0 < σ`, `0 < r`, and `dist s t ≤ r`. It uses the proved monotonicity bridge `hasSubgaussianMGF_mono` from `HighDimProb.SubGaussian`. ## Proved Metric-Entropy Surface The proved surface consists of three deliberately separated layers: - finite chaining: `chain_sub_eq_sum_range`, `expect_abs_sub_chain_le_sum_of_level_sup`, and `expect_abs_sub_chain_le_sum_of_level_sup_of_subGaussianMGFIncrements`; - finite-dimensional volumetric covering bounds: `l1Ball`, `coveringNumber_euclideanBall_le`, and `coveringNumber_l1Ball_le` give the internal `ENat` bounds `ceil((1 + 2R/eps)^card)` and `ceil((1 + 4R/eps)^card)` under `R >= 0`, `eps > 0`, and finite nonempty index assumptions. The l1 bound is obtained volumetrically from `B1 ⊆ B2` (`l1Ball` inside the Euclidean closed ball) plus Mathlib subset comparison, not from the sharper Maurey estimate; - minimal-cover adapter: the existing `exists_finset_isInternalEpsilonNet_of_totallyBounded` supplies the totally-bounded-to-exact-finite internal-net facade; no duplicate theorem was added; - finite entropy sums: `finiteEntropySum`, `expect_abs_sub_chain_le_finiteEntropySum`, and `expect_abs_sub_chain_le_finiteEntropySum_of_path`; - finite anchored supremum (D1): `expect_finset_sup'_abs_sub_anchor_le_finiteEntropySum` and `expect_finset_sup'_abs_sub_anchor_le_truncatedEntropyIntegral` retain a supplied common-anchor path family, shared finite levels, and an explicit integrable terminal-residual envelope; - truncated entropy-integral comparison: `sum_mul_sub_le_intervalIntegral_of_antitoneOn`, `finiteEntropySum_dyadic_le_four_mul_intervalIntegral_coveringNumber`, and `expect_abs_sub_dyadic_path_le_truncatedEntropyIntegral`; - D2 deterministic integral passage: `tendsto_intervalIntegral_of_leftEndpoint_tendsto`, `tendsto_dyadicRadius_atTop`, and `tendsto_intervalIntegral_dyadicRadius_atTop`, together with `le_intervalIntegral_of_le_residual_add_of_tendsto_zero`; these retain explicit endpoint, residual-convergence, and `IntervalIntegrable` hypotheses. The compact residual bridges `tendstoUniformlyOn_abs_sub_of_isCompact`, `tendsto_edist_uniformFun_abs_sub_of_isCompact`, and `tendsto_toReal_edist_uniformFun_abs_sub_of_isCompact` are also proved under explicit compactness, continuity, uniform-approximation, and mapping inputs; - deterministic dense-sup bridge: `HighDimProb.ciSup_eq_ciSup_of_denseRange`; - supplied dense-sequence/full anchored supremum passage (D3): `expect_iSup_abs_sub_anchor_le_of_denseRange_of_prefix_bound` transfers a uniform expected finite-prefix bound by Mathlib partial-supremum and monotone integral convergence, retaining explicit continuity, boundedness, measurability, and full-supremum integrability assumptions. The D2-to-D3 assembly bridge `expect_iSup_abs_sub_anchor_le_mul_intervalIntegral_of_denseRange_of_prefix_bound` is proved only under supplied prefix bounds and supplied residual expectation convergence; - full anchored Dudley endpoint: `dudleyEntropyIntegral` constructs dyadic internal nets and compatible paths, makes the finite-prefix residual vanish through the finite subGaussian maximum estimate, and applies the D2-to-D3 assembly theorem. It retains explicit dense-sequence, singleton-anchor-net, total-boundedness, measurability, increment, continuity, boundedness, full-supremum integrability, and entropy `IntervalIntegrable` hypotheses. Thus the Dudley endpoint is proved under its stated boundary conditions. The theorem does not manufacture sample regularity, full-supremum integrability, or entropy integrability from the increment MGF assumption alone. Direct Mathlib dominated-convergence use remains tested independently without a duplicate project wrapper. Current prioritization is tracked in [`TODO.md`](../maintainers/TODO.md). ## Hanson-Wright The finite-dimensional Hanson-Wright endpoint is `proven` through `HighDimProb.HansonWright.hanson_wright_inequality_hdp_explicit_constant`. For a finite real matrix `A` and finite coordinate family `X` on a probability space, it assumes `K > 0`, `iIndepFun X μ`, and coordinate `HasSubgaussianMGF` bounds at `K^2`. It returns the centered quadratic-form two-sided tail at rate `min(t^2 / (K^4 * Frobenius^2), t / (K^2 * operator))` with the public, parameter-independent `hansonWrightUniversalConstant`. The existential `hanson_wright_inequality_hdp` remains a compatibility wrapper. No matrix symmetry premise or infinite-dimensional extension is claimed. The source and focused consumer are [`HansonWright.lean`](../../HighDimProb/Concentration/HansonWright.lean) and [`HansonWrightAPI.lean`](../../HighDimProbTest/HansonWrightAPI.lean). ## Uniform-Continuity Dudley Consumer - manual finite certificates (expert/support): `SubGaussianMax` retains the path, parent-map, level-cardinality, finite-entropy-sum, and truncated entropy-integral theorems for callers that need a custom chain; - finite-net consumer: `Dudley.truncatedBound` constructs the internal dyadic nets and parent maps from total boundedness and returns a terminal-net supremum bound without asking the caller for certificate data; - full consumer: `Dudley.supremum` is the actual set supremum `sSup (|X t omega - X t0 omega| '' K)`, while `Dudley.fullBound` proves measurability, integrability, and `E sup ≤ 4 * sigma * ∫_0^R sqrt(2 * log(2 * N(K,t))) dt`. `Dudley.Inputs` bundles the geometry, increment, path-regularity, and entropy assumptions, and `Dudley.Inputs.bound` is the preferred downstream call. `Dudley.entropyIntegrand` and `Dudley.entropyIntegral` name the real-valued covering-number entropy expression. `ENat.toNat` totalizes an infinite covering number, so this definition is used by the full theorem only with a totally bounded set at positive radii; it is not an extended-valued entropy definition for arbitrary sets. The full endpoint uses the explicit every-sample path contract and entropy integrability premise. It does not claim an a.e.-only path weakening, separable modifications, or removal of the entropy-integrability assumption. ## Gaussian Functional Foundations `HighDimProb.GaussianFunctional.IntegrationByParts` proves `integral_id_mul_eq_integral_deriv_of_gaussianReal_zero_one` for real `C^1`, compactly supported functions. `HighDimProb.GaussianFunctional.AffineStability` proves `gaussianReal_prod_map_add_linear`, its zero-variance and unit-variance specializations, measurable/integrable integral transport, and `gaussianReal_prod_map_ouLinear` for nonnegative time. Gaussian Poincare, log-Sobolev, and Lipschitz-concentration inequalities remain outside this proved surface. ## RandomMatrix The RandomMatrix layer has a supported finite-dimensional base and the public downstream facade `HighDimProb.RandomMatrix.Concentration`; scoped `Provider.*` facades remain internal/expert maintenance imports. The theorem contracts remain explicit; support does not mean that arbitrary-history or unconditional extensions are proved. The current Matrix Bernstein route includes proved wrappers under explicit assumptions: trace-MGF, quadratic-form, optimized scalar RHS, positive-threshold operator-norm, sample-covariance, crude variance-proxy routes, and prefix/state endpoint bookkeeping wrappers for the Tropp conditional-step route. The TraceExp layer also has a natural `Fin m` trace-state route that derives the finite-family Tropp provider and trace-MGF provider from explicit natural conditional-step data. The sample-covariance surface includes named negative-side provider-transfer adapters for opposite-parameter exp/trace/CFC assumptions; these are adapter lemmas, not unconditional provider proofs. The main layer now has a proven scalar inversion surface: `bernsteinAdditiveTailThreshold` with its nonnegativity, square, positivity, and exponent-equality lemmas, plus the matrix `matrixBernsteinLogFactor`, `matrixBernsteinHighProbabilityThreshold`, and `matrixBernsteinTwoSidedOptimizedScalarTailRHS_highProbabilityThreshold`. The `matrixBernsteinSelfAdjointHighProbabilityStatement` is a typed public contract, and `matrixBernsteinSelfAdjointHighProbabilityStatement_of_optimizedStatement` is its scalar-threshold consumer. The generated-history proof is now exposed by `MatrixBernstein.optimized_of_primitives` and `MatrixBernstein.highProbability_of_primitives`. These APIs preserve `0 < n`, `0 < delta <= 1`, `0 <= sigmaSq`, `0 <= R`, and `0 < sigmaSq or 0 < R`; they do not prove unconditional Matrix Bernstein. Exact endpoint names and caller assumptions are listed in [`RandomMatrixAPI.md`](../user/RandomMatrixAPI.md). ### Matrix Sub-Gaussian Route The focused route has a four-declaration public surface: `MatrixSubGaussianMGF`, `MatrixSubGaussianMGF.neg`, `traceMGFVarianceProxyBound_of_matrixSubGaussian_under_troppPrimitive`, and `subGaussian_quadraticFormUpperTail_under_troppPrimitive`. The predicate is only a conditional Loewner MGF inequality; centeredness, PSD, self-adjointness, measurability, integrability, and probability are not bundled. The finite-family trace-MGF and tail consumers retain the explicit Tropp comparison, random/self-adjoint/independence, variance-proxy self-adjointness, and unbounded matrix/trace-exponential integrability assumptions; the tail endpoint additionally retains the aggregate proxy spectral bound, with its integrability premises required at the optimizer. This is not unconditional Matrix Chernoff or full Tropp, and there is no infinite-dimensional result. ### Directional Matrix Sub-Gaussian Route `DirectionallySubGaussianSelfAdjointMatrix` controls every fixed unit-vector quadratic form by the scalar centered sub-Gaussian MGF contract and is closed under independent finite sums with scale `sqrt (sum_i K_i^2)`. The separate epsilon-net layer exposes `IsUnitSphereNet`, `deterministicOperatorNorm_le_of_isUnitSphereNet`, and single-matrix and independent-sum operator-norm tails with prefactor `2 * N.card` and the scalar layer's `4 * K^2` denominator. The tail theorems are positive-dimensional and retain explicit net, radius, threshold, probability, and entrywise-integrability premises. No finite-net construction, dimension-only cardinality estimate, Loewner matrix-MGF implication, or trace-prefactor theorem is claimed. The hardbone statement atlas in [`HardboneStatements.lean`](../../HighDimProb/RandomMatrix/HardboneStatements.lean) names CFC, log/order, Tropp/Lieb, conditioning, integrability, variance-proxy, and dimension/rank blockers as `typed-prop` targets. Selected consumer wrappers are proven thin applications of those targets; they do not close the hard theorem families. The trace-exp domination-provider consumer `traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider` is proved under an explicit nonnegative integrable dominator and pointwise absolute domination assumption. The centered-square expectation expansion is proved by `matrixSquare_centeredRandomMatrix_expectation_expansion`, using the reusable matrix expectation helpers `matrixExpect_const_mul` and `matrixExpect_mul_const` and the identity `matrixSecondMoment_centeredRandomMatrix`. The variance-proxy centered-square-chain consumers `varianceProxyNormBound_of_centeredSquareChain` and `varianceProxyNormBound_of_centeredSquareChain_expansion` are proved; the latter removes the explicit expansion premise but still requires Loewner comparison and deterministic norm-control assumptions. The centered rank-one second-moment comparison is proved by `centeredRankOneSquare_le_rankOneSecondMoment`, using `matrixSecondMoment_centeredRandomMatrix_le_matrixSecondMoment` and `matrixLE_sub_right_of_isPSD`. The sample-covariance consumer `sampleCovarianceVarianceProxy_sharp_of_rankOneSecondMoment` supplies that comparison to the abstract sharp-variance chain, and `sampleCovarianceVarianceProxy_sharp_of_exactRowSecondMoment` chooses the exact uncentered row second moments so the row comparison is reflexive. The generic deterministic finite-sum norm-control bridge is exposed as `deterministicMatrixVarianceProxyNorm_sum_le_sum`. The exact rank-one second-moment norm providers `deterministicMatrixVarianceProxyNorm_matrixSecondMoment_rankOneRandomMatrix_le_sq_of_sqNorm_bound` and `deterministicMatrixVarianceProxyNorm_sum_matrixSecondMoment_rankOneRandomMatrix_le_sum_sq_of_sqNorm_bound` give row-specific `rowSqNormVarianceProxyNormRHS R` control under explicit square-integrability of the rank-one squares. The direct provider `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_integrable_four_products` supplies that premise from explicit four-coordinate product integrability, and `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_memLp_four` supplies it from coordinate `MemLp 4` assumptions via Mathlib Holder product APIs. The bounded-row provider `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_sqNorm_bound_memLp_two` supplies it from coordinate `MemLp 2` plus pointwise `vectorSqNorm <= R`. Centered rank-one square-integrability providers are proved for coordinate `MemLp 4` and bounded-row `MemLp 2` routes. The direct row-specific provider `MatrixVarianceProxyNormBound_centeredRankOneRandomMatrixFamily_of_rowSqNorm_bound_memLp_two` supplies `rowSqNormVarianceProxyNormRHS R` without an abstract sharp-chain premise. Positive and negative sample-covariance adapters expose the same bound, and `MatrixBernstein.centeredRankOneExactRow` / `MatrixBernstein.sampleCovarianceExactRow` compose it with generated-history Matrix Bernstein. `MatrixBernstein.centeredRankOneExactRowHighProbability` closes the centered rank-one scalar-threshold specialization, while `MatrixBernstein.sampleCovarianceExactRowHighProbability` closes the normalized sample-covariance endpoint. Both high-probability endpoints are exported through the public import `HighDimProb.RandomMatrix.Concentration`; their input bundles and scalar-side conditions remain explicit, so these are not unconditional Matrix Bernstein results. `iIndepFun_centeredRankOne` transports raw vector-family independence, and the `CenteredRankOneInputs.ofIIndepFun` / `CenteredRankOneExactRowInputs.ofIIndepFun` constructors package it so callers state only vector-level `iIndepFun`. The general centering-independence bridge `iIndepFun_centeredRandomMatrix` and the `MatrixBernstein.CenteredSelfAdjointObservationInputs` / `centeredSelfAdjointObservations` route extend the same pattern to self-adjoint observations under explicit centered-square-integrability, centered operator-norm, and variance-proxy assumptions; centeredness, self-adjointness, and centered entrywise integrability are derived from the uncentered family, while `ofIIndepFun` discharges only the centered independence obligation. This is a conditional facade, not an unconditional integrable/self-adjoint Bernstein theorem. The deterministic PSD Loewner-to-operator-norm bridge remains `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE`. Generic variance sharpening outside the centered rank-one setting and unconditional Matrix Bernstein remain open. The rank/support trace-bound bridge is proved by `traceMatrixExp_le_trace_support_exp_lambdaMax_of_supportDomination`, with rank/support consumers for the hardbone targets. Deterministic trace/rank certificates now include the ambient PSD lambda-max certificate `matrixTrace_le_card_mul_of_isPSD_lambdaMaxOrdered_le` and the explicit star-projection certificate `matrixTrace_eq_rank_of_isStarProjection`; the thin consumer `traceMatrixExp_le_rank_exp_lambdaMax_of_isStarProjection` routes that certificate together with `isPSDMatrix_of_isStarProjection` into the rank-bound theorem while keeping the named `MatrixExpSupportDomination` certificate explicit. The remaining support-side work is split into the ambient identity-support provider target and the corrected excess-support target `MatrixExpExcessSupportDomination` / `traceMatrixExp_excess_supportDim_exp_lambdaMax_statement`. The deterministic excess trace bridge `traceMatrixExp_le_card_add_trace_support_mul_exp_sub_one_of_excessSupportDomination` and consumer `traceMatrixExp_excess_supportDim_exp_lambdaMax` are proved under explicit excess certificate, trace support-dimension, and nonnegative coefficient assumptions. Concrete support providers and true effective-rank trace certificates beyond the ambient fallback remain open. The Bernstein CFC route is now proved as `bernsteinMatrixExp_le_quadratic`, via scalar Bernstein, spectrum localization, Bernstein-specific CFC order transfer, and expression normalization. The trace-MGF provider surface includes `matrixBernsteinTraceMGF_under_tropp`, which reuses that CFC proof while keeping Tropp/Lieb and integrability assumptions explicit. The preferred optimized Matrix Bernstein wrappers use `MatrixBernsteinPositiveSideTroppAssumptions` and `MatrixBernsteinNegativeSideTroppAssumptions` to avoid exposing pointwise CFC fields in generic call sites. The sample-covariance route now has the compact bounded-row surface `SampleCovarianceTailTarget`, `SampleCovarianceBoundedRowTroppAssumptions`, and `sampleCovariance_tail_optimized_under_boundedRowTroppAssumptions`, which route quadratic-form and self-adjoint operator-norm targets through one target axis instead of one recommended public name per combination. Lower-level CFC-free `_of_troppPrimitive` / `_of_troppPrimitives` wrappers remain available and reuse `bernsteinMatrixExp_le_quadratic` while keeping Tropp/Lieb and integrability assumptions explicit. The positive-side quadratic-form wrapper `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_troppPrimitive` uses the exact-row variance-proxy hardbone consumer and keeps the sharp-chain premise explicit. The local matrix-exp/log normalization leaf is proved as `matrixExpLogSelfAdjointNormalization`; the matrix-exp log-domain leaf is proved as `matrixExpLogDomainForSelfAdjoint`. Together they provide CFC normalization and log-domain facts needed by the Tropp/Lieb one-step chain. The log/order-to-`K` route now includes the proved thin bridge `matrixLog_le_of_le_matrixExp`, whose operator-log premise can be supplied by the proved witness `operatorLogMonotoneOnPositiveMatrices`. The downstream trace-exponential monotonicity step is proved by `traceMatrixExp_mono_add_selfAdjoint`, and `troppLogExpComparisonToK` proves the resulting deterministic comparison. The finite-family conditioning chain now has the thin witness `troppConditionalStep_of_iIndepFun`; it forwards the explicit per-index conditional-expectation provider and does not prove the history, weaker-independence, or conditional-expectation inputs themselves. The `Provider.Conditioning` separately exposes strengthened history/current-step independence from `iIndepFun` plus explicit summand measurability, together with `TroppNaturalHistory.historyStepContractOfIsRandomMatrix`, which returns the exact legacy contract under explicit random-matrix data. The conditional route is now also composed into the finite-family Bernstein trace-MGF conclusion by `traceMGFBernsteinVarianceProxyBound_of_conditioningBridge`, under explicit natural-state, integrability, MGF, and variance-proxy assumptions recorded in `docs/maintainers/STATEMENTS.md`. The S10 wrapper `matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge` threads that trace-MGF conclusion into the quadratic-form Laplace/tail route under an explicit trace-exp threshold event subset assumption, and the TailEvent provider wrappers discharge that subset premise under random self-adjointness. Its reusable assumption bundle `MatrixBernsteinConditioningTraceMGFTailAssumptions` and thin wrapper `matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFTailAssumptions` package the same tail/conditioning assumptions without proving new hard facts; this is not a full Matrix Bernstein theorem. The newer provider-compressed names `MatrixBernsteinConditioningTraceMGFProviderAssumptions`, `matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFProviderAssumptions`, and `matrixBernsteinQuadraticFormUpperTail_of_naturalStateProviderAssumptions` package the same route with less repeated bookkeeping. The provider bundle derives its exact history/current-step independence contract from explicit random-matrix data while retaining finite-family independence. `HighDimProb.RandomMatrix.Provider.Analysis` owns the ambient matrix-exp Frechet derivative layer, log-resolvent infrastructure, the left/right relative-entropy route, Lieb/Epstein facades, Golden--Thompson, and spectral endpoint monotonicity. `HighDimProb.RandomMatrix.Provider.Conditioning` owns frozen-parameter conditional expectation and natural-history bridges. `HighDimProb.RandomMatrix.Provider.Concentration` owns the left/right Tropp one-step wrappers, the compatibility closure `troppLiebJensenChain_of_leftRight`, trace-MGF-to-Laplace contracts, and Matrix Bernstein assembly. Downstream callers use the re-exporting public facade `HighDimProb.RandomMatrix.Concentration`. The restricted conditional-step route `mHist <= MeasurableSpace.comap H _` is closed by `TraceExpConditioning.troppStep_of_history_le`. The Bernstein facade `TraceExpConditioning.bernsteinStep_of_history_le` constructs the frozen-bound packet from standard single-summand primitives but leaves the exact statement's `IndepFun` premise visible. Golden--Thompson is now proved by `goldenThompsonTraceExp`. Arbitrary larger-history independence, automatic variance-proxy normalization, and unconditional full Matrix Bernstein remain open. ## Not Yet Proved - The older arbitrary-denominator Matrix Bernstein chain. - Full unconditional Matrix Bernstein theorem. - The weaker natural-history independence statement without explicit summand measurability; the explicit-random-matrix compatibility contract is proved. Conditional-expectation reduction for arbitrary larger history sigma-algebras, and trace-exp integrability propagation for the conditional-step Tropp route. The restricted `mHist <= MeasurableSpace.comap H _` route is proved. - Proofs of the remaining downstream Tropp conditioning targets, automatic trace-exp domination/integrability, automatic variance-proxy sharpening beyond centered-square expectation expansion, support-domination providers, support-construction certificates, true effective-rank/support trace certificates, and dimension/rank refinements beyond explicit star-projection rank consumers. ## Maintenance Rule Keep this file as the compact family-level proved/open ledger. Put current focus in [`Status.md`](../user/Status.md), active task planning in [`TODO.md`](../maintainers/TODO.md), module ownership in [`RandomMatrixArchitecture.md`](../architecture/RandomMatrixArchitecture.md), exact endpoint details in the relevant API index, and historical summaries in [`archive.md`](../archive/README.md).