Library

470 Lean files, 1,807 theorems, and 1,035 supporting lemmas, organized around the main StatFoundation, HighDim, and Nonparametric boards with additional supporting packages in the full tree. Browse the structure below, then a few selected results from each area.

Structure

— the full Statlib/ tree (click to expand)
Statlib/
  • Causal/
    • SCM/
      • Backdoor.lean
      • DoConditionalLaws.lean
      • Frontdoor.lean
      • FrontdoorCriterion.lean
      • GFormula.lean
      • GFormulaGraph.lean
      • GraphSurgery.lean
      • InterventionalSoundness.lean
      • MoralizedGraph.lean
      • ObservationalChain.lean
      • ObservationalCollider.lean
      • ObservationalSoundness.lean
      • Theorems.lean
      • Vocabulary.lean
    • Identification.lean
    • SCM.lean
    • Vocabulary.lean
  • HighDim/
    • Concentration/
      • FrobeniusNormSqConcentration.lean
      • GaussianQuadraticForm.lean
      • HansonWright.lean
      • MatrixBernstein.lean
      • OperatorNormSubgaussian.lean
      • SubGaussianMax.lean
    • CovarianceMatrix/
      • L1QuadraticProcess/
        • RadiusFluctuation.lean
      • CovarianceGap.lean
      • CovDiagonalConcentration.lean
      • CovQuadraticDeviation.lean
      • CovTraceConcentration.lean
      • L1QuadraticProcess.lean
      • Properties.lean
      • SampleCovariance.lean
      • SampleCovEigenvalueLower.lean
      • SampleCovEigenvalueUpper.lean
    • Geometry/
      • CoveringNumbers.lean
      • JohnsonLindenstrauss.lean
      • RIPConstruction.lean
      • SubGaussianRIPTailAnisotropic.lean
    • MatrixAnalysis/
      • AndoVocabulary.lean
      • ArakiHeinzK3.lean
      • CStarBridge.lean
      • FenchelDualNuclearNormProx.lean
      • Fischer.lean
      • FrobeniusNormSvdRelation.lean
      • GoldenThompson.lean
      • Hadamard.lean
      • HansenPedersenJensenMulLog.lean
      • HardSvThreshold.lean
      • KleinTraceExpVariationalLb.lean
      • KyFan.lean
      • LiebRuskaiConjInvJointlyConvex.lean
      • LiebThirring.lean
      • LiebThirringK3Blocks.lean
      • LiebThirringK3Trace.lean
      • LiebThirringReduction.lean
      • LiebTraceConcavity.lean
      • LowRankFrobeniusErrorDecomposition.lean
      • MatrixLogIntegralRep.lean
      • NuclearNormLeSqrtRank.lean
      • NuclearNormProperties.lean
      • OperatorConvexMulLog.lean
      • PowerTraceConcavity.lean
      • RankOneSinTheta.lean
      • RelativeEntropyJointConvex.lean
      • SingularValueProperties.lean
      • SoftThresholdDenoisingHelpers.lean
      • SVDFoundation.lean
      • SvdSortedExists.lean
      • SvSoftThreshold.lean
      • TraceExp.lean
      • TraceExpVariationalFormula.lean
      • VonNeumann.lean
      • WedinSinTheta.lean
      • Weyl.lean
    • MatrixCompletion/
      • BatchUnionFreshness.lean
      • BernoulliMaskAlgebra.lean
      • CompactFactorBridge.lean
      • DeterministicBernoulliScalarTail.lean
      • DualCertificateCriterion.lean
      • FiniteCoordinateTailUnion.lean
      • GolfingParameterBudget.lean
      • NuclearSubgradientCompact.lean
      • OffTangentSamplingBound.lean
      • ProjectedCoordinateSpreadBricks.lean
      • TangentEntryIncoherence.lean
      • TangentProjection.lean
      • TangentRankoneVectorization.lean
      • TangentSamplingIsometry.lean
    • MatrixRecovery/
      • EmpiricalProcessNuclearNormBound.lean
      • MatrixRipRecoveryBound.lean
      • RankConstrainedDenoising.lean
      • RankOneSpectralInitialization.lean
      • SoftThresholdDenoisingGuarantee.lean
      • SpectralInitialization.lean
    • Regression/
      • DebiasingLasso.lean
      • DesignNoiseInnerSubexponential.lean
      • DesignNoiseSecondMoment.lean
      • Incoherence.lean
      • L1RSEFromCovariance.lean
      • LassoOracle.lean
      • LassoRSEOracle.lean
      • SampleCovarianceDesignBridge.lean
    • SpectralPerturbation/
      • DavisKahan.lean
      • Eigenvalues.lean
      • PCA.lean
      • Weyl.lean
    • Vocabulary/
      • CStarBridge.lean
      • DebiasingLasso.lean
      • DesignMatrix.lean
      • MatrixCompletion.lean
      • Norms.lean
      • QuadraticForms.lean
      • Quantum.lean
      • RandomMatrix.lean
      • RandomVector.lean
      • Restrictions.lean
      • Sparse.lean
      • Spectral.lean
      • SVD.lean
    • Basic.lean
    • Concentration.lean
    • CovarianceMatrix.lean
    • Geometry.lean
    • MatrixAnalysis.lean
    • MatrixCompletion.lean
    • MatrixRecovery.lean
    • Regression.lean
    • SpectralPerturbation.lean
    • Vocabulary.lean
  • HypothesisTesting/
    • Asymptotic/
      • ChiSquareAsymptotics.lean
      • MultivariateChiSquareAsymptotics.lean
      • TTestAsymptotic.lean
      • Vocabulary.lean
      • ZTestAsymptotic.lean
    • Inference/
      • ConfidenceInterval.lean
      • NormalTheoryConfidence.lean
    • MLR/
      • KarlinRubin.lean
      • NPConditions.lean
    • MultipleTesting/
      • BenjaminiHochberg.lean
      • Bonferroni.lean
      • Holm.lean
    • NeymanPearson/
      • Complete.lean
      • Existence.lean
      • IntegralInequality.lean
      • IntegrandInequality.lean
      • Optimality.lean
      • ToTestFunction.lean
    • Nonparametric/
      • MannWhitney.lean
      • MannWhitneyCLT.lean
      • SignedRank.lean
      • SignTest.lean
    • NormalTheory/
      • ANOVA.lean
      • SampleMean.lean
      • TTest.lean
      • VarianceTest.lean
      • ZTest.lean
    • PValue/
      • DecisionRule.lean
      • Validity.lean
    • Randomization/
      • OrbitCounting.lean
      • PermutationMW.lean
      • Validity.lean
      • Vocabulary.lean
    • UMPU/
      • Basic.lean
      • Boundary.lean
    • Bridge.lean
    • Vocabulary.lean
  • Nonparametric/
    • Approximation/
      • FunctionClasses.lean
      • Holder.lean
      • Kernel.lean
      • Metric.lean
      • NeuralNetwork.lean
      • NeuralNetworkAlgebra.lean
      • ReLUNetworkConstruction.lean
      • ReLUStateMachine.lean
      • RKHS.lean
      • ShallowReLUApproximation.lean
      • ShallowReLUApproximationGeometry.lean
      • Sieve.lean
      • Spline.lean
      • SplineFacts.lean
      • Wavelet.lean
      • WaveletFacts.lean
    • FunctionalData/
      • Mean.lean
      • Regression.lean
      • Vocabulary.lean
    • KernelRegression/
      • KernelRate.lean
      • KRRClosedForm.lean
      • Representer.lean
    • OracleInterface/
      • Risk.lean
    • Spectral/
      • Embedding.lean
    • Vocabulary/
      • ConformalQuantileRegression.lean
      • Estimator.lean
      • FunctionClasses.lean
      • Kernel.lean
      • KernelMethods.lean
      • KernelRegression.lean
      • Loss.lean
      • Models.lean
      • NeuralNetwork.lean
      • Risk.lean
      • RKHS.lean
      • Sieve.lean
      • Spline.lean
      • Wavelet.lean
    • Approximation.lean
    • Basic.lean
    • ConformalQuantileRegression.lean
    • FunctionalData.lean
    • KernelRegression.lean
    • OracleInterface.lean
    • Spectral.lean
    • Vocabulary.lean
  • RandomMatrix/
    • SampleCovariance/
      • LeaveOneOut/
        • AverageBiasAssembly.lean
        • CondMeanBias.lean
        • FullResolventQuadraticBound.lean
        • OffdiagMomentBound.lean
        • PairwiseCondMeanBound.lean
        • ResolventEntryBound.lean
        • ResolventFunctionalIntegrable.lean
        • ResolventUpdatePairwise.lean
        • RowInnovationBound.lean
        • RowReplacementIntegralTransfer.lean
        • RowSquareSumIntegrable.lean
      • ComplexCondExpNormSqDecomp.lean
      • ComplexConditionalEfronStein.lean
      • ComplexEfronStein.lean
      • ComplexNormSqIntegralDecomp.lean
      • CoordinateSwap.lean
      • CoordinateSwapPolarRewrite.lean
      • IndependentEnvRowScalarConditionalES.lean
      • LeaveOneOutCoordinateSwap.lean
      • LeaveOneOutMatrixPsd.lean
      • LOOCoordinateSwapSquared.lean
      • ResidualSwap.lean
      • ResidualSwapCoordFactorSum.lean
      • ResidualSwapPointwise.lean
      • ResidualSwapSumMoment.lean
      • ResolventCone.lean
      • ResolventEfronSteinBound.lean
    • Vocabulary/
      • Distributions.lean
      • Ensemble.lean
      • SpectralMeasure.lean
      • StieltjesTransform.lean
    • Basic.lean
    • MeasuresAreProbability.lean
    • MPSceLemmas.lean
    • SampleCovariance.lean
    • SpectralMoment.lean
    • StieltjesAnalysis.lean
    • StieltjesTransformBound.lean
    • Vocabulary.lean
  • StatFoundation/
    • BasicAnalysis/
      • CompactSelfAdjoint.lean
      • ENNRealBridge.lean
      • exp_neg_sq_div_le_exp_neg_sq_div_of_den_le.lean
      • ExponentialBounds.lean
      • measure_le_ofReal_of_measureReal_le.lean
      • SpectralEntropy.lean
      • sub_le_abs_sub_of_gap_near.lean
      • TailIntegral.lean
      • TaylorExpansions.lean
    • Concentration/
      • ExponentialType/
        • azuma_sum_meas_abs_ge_le_two_exp.lean
        • azuma_sum_meas_ge_le_exp.lean
        • bennett_sum_meas_ge_le_exp.lean
        • bernstein_bounded_sum_meas_abs_ge_le_two_exp.lean
        • bernstein_bounded_sum_meas_ge_le_exp.lean
        • bernstein_martingale_bounded_sum_meas_abs_ge_le_two_exp.lean
        • bernstein_martingale_bounded_sum_meas_ge_le_exp.lean
        • bernstein_martingale_sum_meas_abs_ge_le_two_exp.lean
        • bernstein_martingale_sum_meas_ge_le_exp.lean
        • bernstein_sum_meas_abs_ge_le_two_exp.lean
        • bernstein_sum_meas_ge_le_exp.lean
        • FiniteMaxBernsteinExpectation.lean
        • hoeffding_bounded_mean_meas_ge_le_exp.lean
        • hoeffding_bounded_sum_meas_abs_ge_le_two_exp.lean
        • hoeffding_bounded_sum_meas_ge_le_exp.lean
        • hoeffding_mean_meas_ge_le_exp.lean
        • hoeffding_mgf_le.lean
        • hoeffding_sum_meas_abs_ge_le_two_exp.lean
        • hoeffding_sum_meas_ge_le_exp.lean
        • mcdiarmid_meas_ge_le_exp.lean
        • subexp_max_meas_ge_le_exp.lean
        • subexp_mean_meas_ge_le_exp.lean
        • subexp_sum_mgf_le_of_indep.lean
        • subgaussian_abs_tail_real.lean
        • subgaussian_max_expectation_le.lean
        • subgaussian_max_meas_ge_le_exp.lean
        • subgaussian_sum_mgf_le_of_indep.lean
      • MomentType/
        • bdg_upper_l2.lean
        • cramer_chernoff.lean
        • efron_stein_inequality.lean
        • jensen_inequality_prob.lean
        • khintchine_inequality.lean
        • lyapunov_moment_ineq.lean
        • Markov.lean
        • moment_tail_bound.lean
        • paley_zygmund.lean
        • rosenthal_inequality.lean
        • von_bahr_esseen.lean
      • ExponentialType.lean
      • MomentType.lean
    • Convergence/
      • AnalysisTools/
        • StochasticOrder/
          • Algebra.lean
          • AlgebraAdd.lean
          • AlgebraAddLittle.lean
          • AlgebraDeterministicScale.lean
          • AlgebraFiniteSum.lean
          • AlgebraMap.lean
          • AlgebraProduct.lean
          • AlgebraProductBig.lean
          • AlgebraProductMixedLittleBig.lean
          • AlgebraProductMixedOBigLittle.lean
          • AlgebraSubBig.lean
          • AlgebraSubLittle.lean
          • Basic.lean
          • ConvergenceBridges.lean
          • Rate.lean
          • RateBig.lean
          • RateBounds.lean
          • RateLittle.lean
          • RateRefinement.lean
          • SlutskyProduct.lean
          • TailGates.lean
        • AsymptoticLinear.lean
        • CdfQuantile.lean
        • CharacteristicFunction.lean
        • ConvergenceModes.lean
        • CramerWold.lean
        • GaussianMaxAnticoncentration.lean
        • GaussianStein.lean
        • IntegralConvergence.lean
        • LevyContinuity.lean
        • MappingTheorems.lean
        • Nazarov.lean
        • Scheffe.lean
        • SmoothComparison.lean
        • SmoothCutoff.lean
        • SmoothMax.lean
        • Tightness.lean
        • UniformIntegrability.lean
      • CentralLimitTheorem/
        • FiniteLinearCombination.lean
        • IID.lean
        • LindebergFeller.lean
        • Lyapunov.lean
        • MartingaleTriangularArray.lean
        • MaxType.lean
        • Multivariate.lean
      • LawOfLargeNumbers/
        • GlivenkoCantelli.lean
        • UniformStrongLaw.lean
      • Resampling/
        • AntiConcentration.lean
        • BootstrapInterface.lean
        • GaussianMaxComparison.lean
      • AnalysisTools.lean
      • CentralLimitTheorem.lean
      • LawOfLargeNumbers.lean
      • Resampling.lean
    • EmpiricalProcess/
      • BoundedDifference.lean
      • DudleyEntropyIntegral.lean
      • DudleyRademacher.lean
      • FiniteClassRademacherComplexity.lean
      • GlivenkoCantelliQuantitative.lean
      • RademacherContraction.lean
      • RademacherGeneralizationBound.lean
      • RademacherSecondMoment.lean
      • RademacherSignMGF.lean
      • Symmetrization.lean
      • UniformDeviationFiniteClass.lean
    • Probability/
      • ChiSquared.lean
      • CondMgfFreezing.lean
      • FDistribution.lean
      • TDistribution.lean
    • RandomVariable/
      • Gaussian/
        • Hermite.lean
        • HilbertSpace.lean
        • LipschitzConcentration.lean
        • LogSobolev.lean
        • Slepian.lean
        • Standard.lean
        • Stein.lean
      • HilbertValue/
        • Covariance.lean
        • Vocabulary.lean
      • SubExponential/
        • scalar_sq_centered_exp_integrable.lean
        • scalar_sq_centered_subexponential_explicit.lean
        • subexp_closure.lean
        • subexp_cond_mgf_le_of_indep.lean
        • subexp_exp_tail_of_subexp.lean
        • subexp_meas_abs_ge_le_two_exp.lean
        • subexp_meas_ge_le_exp.lean
        • subexp_mgf_finite.lean
        • subexp_mgf_finite_of_exp_tail.lean
        • subexp_mgf_finite_of_moment_le.lean
        • subexp_mgf_le_of_bounded.lean
        • subexp_mgf_le_of_exponential.lean
        • subexp_mgf_le_of_sq_subgaussian.lean
        • subexp_mgf_le_of_subgaussian.lean
        • subexp_moment_le_of_mgf_finite.lean
        • subexp_of_mgf_finite.lean
        • subexp_variance_le.lean
        • subexponential_mgf_const_mul.lean
        • subgaussian_prod_subexponential.lean
      • SubGaussian/
        • cond_subgaussian_linear_form_of_indep.lean
        • sq_le_two_mul_exp.lean
        • subgaussian_even_moment_le.lean
        • subgaussian_even_moment_le_of_tail.lean
        • subgaussian_exp_sq_le.lean
        • subgaussian_exp_sq_le_at_one_third.lean
        • subgaussian_fourth_moment_le.lean
        • subgaussian_integral_eq_zero.lean
        • subgaussian_meas_abs_ge_le_two_exp.lean
        • subgaussian_meas_ge_le_exp.lean
        • subgaussian_mgf_eq_of_gaussian.lean
        • subgaussian_mgf_le_of_bounded.lean
        • subgaussian_mgf_le_of_even_moment.lean
        • subgaussian_mgf_le_of_exp_sq.lean
        • subgaussian_mgf_mono_param.lean
        • subgaussian_variance_le.lean
      • Gaussian.lean
      • HilbertValue.lean
      • SubExponential.lean
      • SubGaussian.lean
    • Statistics/
      • Asymptotic/
        • Contiguity.lean
        • LAN.lean
        • Power.lean
        • ScoreCLT.lean
        • Vocabulary.lean
      • Estimation/
        • AsymptoticLinear.lean
        • Consistency.lean
        • CramerRao.lean
        • MLE.lean
        • MultiParameter.lean
        • UStatistic.lean
        • Vocabulary.lean
      • Sufficiency/
        • LehmannScheffe/
          • CompleteUnique.lean
          • CondExp.lean
          • MSE.lean
          • UMVUE.lean
        • Basic.lean
        • Basu.lean
        • LehmannScheffe.lean
      • Asymptotic.lean
      • Conformal.lean
      • Estimation.lean
      • Sufficiency.lean
    • Vocabulary/
      • Conformal.lean
      • CoveringNumbers.lean
      • EmpiricalProcess.lean
      • FiniteCoordinate.lean
      • GaussianCriticalValue.lean
      • Independence.lean
      • MaxType.lean
      • OrliczNorm.lean
      • ParametricFamily.lean
      • RandomVariable.lean
      • Resampling.lean
      • StochasticOrder.lean
      • UniformIntegrability.lean
      • VCDimension.lean
    • Basic.lean
    • BasicAnalysis.lean
    • Concentration.lean
    • Convergence.lean
    • EmpiricalProcess.lean
    • Probability.lean
    • RandomVariable.lean
    • Statistics.lean
    • Vocabulary.lean
  • Basic.lean
  • Causal.lean
  • HighDim.lean
  • HypothesisTesting.lean
  • Nonparametric.lean
  • RandomMatrix.lean
  • StatFoundation.lean
  • Vocabulary.lean

Selected results

— curated per area; see Featured for deep dives
1

Statistical foundations

Statlib.StatFoundation
1.1

Statistical inference & sufficiency

  • Lehmann-Scheffé theorem
    proved
    ∃h,  Eθ[(h∘T−g(θ))2]≤Eθ[(δ′−g(θ))2] ∀δ′ unbiased\exists h,\; \mathbb{E}_\theta[(h\circ T - g(\theta))^2] \le \mathbb{E}_\theta[(\delta' - g(\theta))^2]\ \forall \delta'\text{ unbiased}

    If T is a complete sufficient statistic and δ is unbiased for g(θ), then a function of T is the unique uniformly minimum-variance unbiased estimator (UMVUE) of g(θ).

    lehmannScheffe_umvue
  • Basu's theorem
    proved
    T complete sufficient, V ancillary  ⟹  T⊥ ⁣ ⁣ ⁣⊥V under each PiT \text{ complete sufficient},\ V \text{ ancillary} \implies T \perp\!\!\!\perp V \text{ under each } P_i

    A boundedly complete sufficient statistic is independent of every ancillary statistic under each measure in the family.

    basu_indepFun
1.2

Convergence & limit theorems

  • Uniform Strong Law of Large Numbers
    proved
    sup⁡θ∈Θ∣1n∑j<nU(Xj,θ)−EU(X,θ)∣→a.s.0\sup_{\theta \in \Theta}\left|\frac1n\sum_{j<n} U(X_j,\theta) - \mathbb{E}U(X,\theta)\right| \xrightarrow{a.s.} 0

    For i.i.d. samples and a compact parameter space, continuous dominated criterion functions satisfy uniform almost-sure convergence of sample averages to population means.

    uniform_strong_law
  • Lindeberg-Feller Central Limit Theorem
    proved
    ∑jXn,jsn→dN(0,1) under Lindeberg’s condition\frac{\sum_{j} X_{n,j}}{s_n} \xrightarrow{d} \mathcal{N}(0,1) \text{ under Lindeberg's condition}

    A triangular array of independent, centered row-variables whose normalized sums satisfy the Lindeberg condition converges in distribution to the standard normal.

    lindeberg_feller_central_limit_theorem
  • Gaussian maximum comparison (diagonal case)
    proved
    sup⁡t∣Pr⁡(max⁡jVj≤t)−Pr⁡(max⁡jYj≤t)∣≤C(c1,C1) Δ1/3(1∨log⁡(p/Δ))2/3\sup_t\left|\Pr(\max_j V_j\le t)-\Pr(\max_j Y_j\le t)\right|\le C(c_1,C_1)\,\Delta^{1/3}\left(1\vee\log(p/\Delta)\right)^{2/3}

    For independent centered Gaussian vectors with diagonal variances bounded above and away from zero, a covariance gap Δ in (0, 1) controls the difference between their maximum distributions.

    gaussianMax_cube_root_comparison_diagonal
1.3

Stochastic-order asymptotics

  • Slutsky product theorem (big-O × little-o)
    proved
    Xn=OP(1), Yn=oP(1)⇒XnYn=oP(1)X_n = O_{\mathbb{P}}(1),\ Y_n = o_{\mathbb{P}}(1) \Rightarrow X_n Y_n = o_{\mathbb{P}}(1)

    The product of a probabilistically bounded sequence and a sequence converging in probability to zero also converges to zero in probability.

    isBigOInProbability_mul_isLittleOInProbability
  • Little-o rate refinement under deterministic scaling
    proved
    Yn=oP(rn)⇒anYn=oP(anrn)Y_n = o_{\mathbb{P}}(r_n) \Rightarrow a_n Y_n = o_{\mathbb{P}}(a_n r_n)

    Little-o probability rates scale linearly with deterministic sequences, enabling rate transfer across normalizations.

    isLittleOInProbability_mul_rate
1.4

Uniform integrability

  • Vitali convergence theorem
    proved
    Xn→PX, {Xn} UI⇒Xn→L1XX_n\xrightarrow{\mathbb{P}}X,\ \{X_n\}\ \text{UI} \Rightarrow X_n\xrightarrow{L^1}X

    Convergence in probability plus uniform integrability implies L¹ convergence.

    inLpConvergence_one_of_inProbabilityConvergence_of_isUniformIntegrable
  • Integral convergence under UI domination
    proved
    {Xn} UI, Xn→PX⇒E[Xn]→E[X]\{X_n\}\ \text{UI},\ X_n\xrightarrow{\mathbb{P}}X \Rightarrow \mathbb{E}[X_n]\to\mathbb{E}[X]

    For uniformly integrable sequences converging in probability, expectations converge.

    tendsto_integral_continuousLinearMap_of_inProbabilityConvergence_of_isUniformIntegrable
1.5

Empirical processes

  • Uniform deviation for finite classes
    proved
    Pr⁡ ⁣(sup⁡f∈F∣Pnf−Pf∣>t)≤∣F∣ e−cnt2\Pr\!\left(\sup_{f\in\mathcal{F}} |P_n f-P f|>t\right) \le |\mathcal{F}|\,e^{-c n t^2}

    A union-bound finite-class uniform deviation theorem for bounded measurable functions.

    uniform_deviation_finite_class
  • Quantitative Glivenko-Cantelli bound
    proved
    Pr⁡ ⁣(sup⁡t∣Fn(t)−F(t)∣>ε)≤C(ε,n)\Pr\!\left(\sup_t |F_n(t)-F(t)|>\varepsilon\right) \le C(\varepsilon,n)

    A finite-sample Glivenko-Cantelli theorem giving an explicit tail bound for the empirical distribution function.

    glivenko_cantelli_quantitative
  • Dudley entropy integral
    proved
    Esup⁡t∈TXt≤C∫0diam⁡(T)log⁡N(T,ρ,ε) dε\mathbb{E}\sup_{t\in T} X_t \le C\int_0^{\operatorname{diam}(T)}\sqrt{\log N(T,\rho,\varepsilon)}\,d\varepsilon

    A chaining-style entropy integral control for finite sub-Gaussian processes.

    dudley_entropy_integral
1.6

Tail behavior of random variables

  • Gaussian concentration for Lipschitz functions
    proved
    P ⁣(∣f(X)−Ef(X)∣≥t)≤2exp⁡ ⁣(−t22L2)\mathbb{P}\!\left(|f(X)-\mathbb{E}f(X)|\ge t\right) \le 2\exp\!\left(-\frac{t^2}{2L^2}\right)

    An L-Lipschitz function of a vector with independent standard Gaussian coordinates has a dimension-free two-sided Gaussian tail around its mean.

    gaussian_lipschitz_concentration
  • Sub-exponential MGF bound for squared sub-Gaussian
    proved
    X sub-Gaussian  ⟹  X2 is sub-exponentialX \text{ sub-Gaussian} \implies X^2 \text{ is sub-exponential}

    The square of a sub-Gaussian random variable is sub-exponential, with an explicit moment generating function bound.

    subexp_mgf_le_of_sq_subgaussian
  • Ornstein-Uhlenbeck Mehler formula
    proved
    Ptf(x)=E f(e−tx+1−e−2tZ)P_t f(x)=\mathbb{E}\,f(e^{-t}x+\sqrt{1-e^{-2t}}Z)

    The Gaussian Mehler semigroup is formalized as the analytic backbone of the functional-inequality and concentration chain.

    standardReal_ou_mehler_basic
1.7

Concentration inequalities

  • Bernstein's inequality (sub-exponential sum)
    proved
    P ⁣(∑iXi≥t)≤exp⁡ ⁣(−12min⁡ ⁣(t2∑iσi2, tbmax⁡))\mathbb{P}\!\left(\sum_i X_i \ge t\right) \le \exp\!\left(-\tfrac12 \min\!\left(\tfrac{t^2}{\sum_i \sigma_i^2},\, \tfrac{t}{b_{\max}}\right)\right)

    For independent zero-mean sub-exponential variables, the tail interpolates between Gaussian and exponential decay depending on the deviation scale.

    bernstein_sum_meas_ge_le_exp
  • McDiarmid's bounded-differences inequality
    proved
    P ⁣(f(X)−Ef(X)≥t)≤exp⁡ ⁣(−2t2∑ici2)\mathbb{P}\!\left(f(X) - \mathbb{E}f(X) \ge t\right) \le \exp\!\left(\frac{-2t^2}{\sum_i c_i^2}\right)

    A function of independent variables that changes by at most c_i when one coordinate changes concentrates sharply around its mean.

    mcdiarmid_meas_ge_le_exp
1.8

Conformal prediction

  • Prediction coverage from score coverage
    proved
    ScoreCoveredBy⁡(s,t)⊆E,HasScoreCoverage⁡(s,t,α)⇒MarginalCoverage⁡(E,α)\operatorname{ScoreCoveredBy}(s,t)\subseteq E,\quad \operatorname{HasScoreCoverage}(s,t,\alpha)\Rightarrow\operatorname{MarginalCoverage}(E,\alpha)

    A proved score-coverage event transfers its marginal coverage bound to any prediction event containing it.

    prediction_coverage_of_score_subset
  • Prediction miscoverage from score miscoverage
    proved
    Ebad⊆ScoreMiscoveredBy⁡(s,t),HasScoreMiscoverageBound⁡(s,t,α)⇒MarginalEventBound⁡(Ebad,α)E_{\mathrm{bad}}\subseteq\operatorname{ScoreMiscoveredBy}(s,t),\quad \operatorname{HasScoreMiscoverageBound}(s,t,\alpha)\Rightarrow\operatorname{MarginalEventBound}(E_{\mathrm{bad}},\alpha)

    A score miscoverage bound transfers to any smaller bad-prediction event.

    prediction_miscoverage_of_subset
2

High-dimensional statistics

Statlib.HighDim
2.1

Matrix analysis

  • Operator convexity of A log A
    proved
    (θA+(1−θ)B)log⁡(θA+(1−θ)B)⪯θAlog⁡A+(1−θ)Blog⁡B(\theta A+(1-\theta)B)\log(\theta A+(1-\theta)B) \preceq \theta A\log A+(1-\theta)B\log B

    The operator-convexity step that now replaces the former matrix Lieb trace axiom path.

    op_convex_mul_log
  • Simple-function Jensen step for Lieb trace
    proved
    tr⁡exp⁡ ⁣(H+log⁡EA)≥Etr⁡exp⁡(H+log⁡A)\operatorname{tr}\exp\!\left(H+\log\mathbb{E}A\right) \ge \mathbb{E}\operatorname{tr}\exp(H+\log A)

    The positive-definite simple-function Jensen step feeding the matrix Bernstein Laplace-transform argument.

    trace_exp_add_log_simpleFunc_jensen_posDef
  • Wedin sin-theta theorem for singular subspaces
    proved
    max⁡{∥UU⊤−U^U^⊤∥F,∥VV⊤−V^V^⊤∥F}≤2r ∥E∥op/δ\max\{\|UU^\top-\hat U\hat U^\top\|_F,\|VV^\top-\hat V\hat V^\top\|_F\}\le \sqrt{2r}\,\|E\|_{\mathrm{op}}/\delta

    For Ahat = A + E with a separated top-r singular spectrum and small operator-norm perturbation, the left and right singular subspace projectors move by at most a Wedin sin-theta bound.

    wedin_sin_theta
2.2

Low-rank matrix recovery and completion tools

  • Stable nuclear-norm matrix recovery under RIP
    proved
    ∥A^−A⋆∥F≤C0(δ) ∥A⋆−Ar⋆∥∗r+C1(δ) ε\|\widehat A-A^\star\|_F\le C_0(\delta)\,\frac{\|A^\star-A_r^\star\|_*}{\sqrt r}+C_1(\delta)\,\varepsilon

    Under rank-4r restricted isometry with δ below √2−1, a feasible nuclear-norm minimizer has Frobenius error bounded by the rank-r approximation tail and observation noise. The positive constants depend on δ.

    matrix_rip_recovery_bound
  • Compact-factor nuclear-norm subgradient
    proved
    ∂∥⋅∥∗(M)={UV⊤+W:U⊤W=0, WV=0, ∥W∥op≤1}\partial\|\cdot\|_*(M)=\{UV^\top+W:U^\top W=0,\ WV=0,\ \|W\|_{\mathrm{op}}\le1\}

    For a positive-singular-value compact factorization M = U diag(σ) Vᵀ with orthonormal factor columns, characterizes the nuclear-norm subdifferential and supplies tangent-space certificate inequalities.

    nuclear_subgradient_compact
2.3

High-dimensional concentration

  • Rectangular matrix Bernstein inequality
    proved
    P ⁣(∥∑kXk∥≥t)≤(p+q) exp⁡ ⁣(−t2/2σ2+Rt/3)\mathbb{P}\!\left(\Big\|\sum_k X_k\Big\| \ge t\right) \le (p+q)\,\exp\!\left(\frac{-t^2/2}{\sigma^2 + Rt/3}\right)

    The matrix Bernstein bound extended to sums of independent centered rectangular p×q random matrices via Hermitian dilation, with variance the max of the two one-sided second-moment norms.

    matrix_bernstein_rect
  • Hanson-Wright inequality (isotropic)
    proved
    P(∣X⊤AX−tr⁡A∣≥t)≤2exp⁡ ⁣(−cmin⁡ ⁣(t2σ4∥A∥F2,tσ2∥A∥))\mathbb{P}\big(|X^\top A X - \operatorname{tr}A| \ge t\big) \le 2\exp\!\left(-c\min\!\Big(\tfrac{t^2}{\sigma^4\|A\|_F^2}, \tfrac{t}{\sigma^2\|A\|}\Big)\right)

    The isotropic specialization of Hanson-Wright, where the centering term is exactly the trace of A.

    hanson_wright_isotropic
2.4

Covariance estimation

  • Sample covariance matrix concentration
    proved
    P(∥Σ^−Σ∥≥Cσ2((n+t)/m+(n+t)/m))≤2e−t\mathbb{P}\big(\|\hat\Sigma - \Sigma\| \ge C\sigma^2(\sqrt{(n+t)/m} + (n+t)/m)\big) \le 2e^{-t}

    For i.i.d. centered sub-Gaussian vectors there is a universal constant so the sample second-moment matrix concentrates around the true covariance in operator norm with exponential tails.

    sampleCovariance_concentration
  • Isotropic norm concentration
    proved
    P(∣∥X∥2−n∣≥t)≤2exp⁡ ⁣(−cmin⁡(t2/(σ4n), t/σ2))\mathbb{P}\big(\big|\|X\|^2 - n\big| \ge t\big) \le 2\exp\!\big(-c\min(t^2/(\sigma^4 n),\, t/\sigma^2)\big)

    An isotropic sub-Gaussian vector has squared norm tightly concentrated about its dimension n, with Bernstein-type sub-exponential tails.

    isotropic_norm_concentration
2.5

High-dimensional geometry

  • Anisotropic sub-Gaussian RIP tail bound
    proved
    m≳σ4κ2slog⁡(en/s)δ2⇒Pr⁡ ⁣[∀s-sparse β, (1±δ)β⊤Σβ]≥1−2e−cδ2mκ2/σ4m \gtrsim \frac{\sigma^4}{\kappa^2}\frac{s\log(en/s)}{\delta^2}\Rightarrow \Pr\!\left[\forall s\text{-sparse }\beta,\ (1\pm\delta)\beta^\top\Sigma\beta\right]\ge 1-2e^{-c\delta^2m\kappa^2/\sigma^4}

    A heterogeneous-covariance RIP concentration inequality: sub-Gaussian rows concentrate around their covariance quadratic form under a covariance lower bound κ.

    subgaussian_rip_tail_anisotropic
  • Restricted isometry property of sub-Gaussian matrices
    proved
    m≳σ4s log⁡(en/s)/δ2  ⇒  Pr⁡[X is (s,δ)-RIP]≥1−2e−cδ2m/σ4m \gtrsim \sigma^4 s\,\log(en/s)/\delta^2 \;\Rightarrow\; \Pr[X \text{ is } (s,\delta)\text{-RIP}] \ge 1 - 2e^{-c\delta^2 m/\sigma^4}

    An m-by-n matrix with i.i.d. isotropic sub-Gaussian rows satisfies the (s,delta) restricted isometry property with high probability once m exceeds order s·log(en/s)/delta^2.

    subgaussian_rip_sample_complexity
2.6

High-dimensional regression

  • Fixed-design LASSO oracle bound under L1-RSE
    proved
    1m∥X(β^−β⋆)∥22+λ∥β^−β⋆∥1≲sλ2κ2\frac1m\|X(\hat\beta-\beta^\star)\|_2^2+\lambda\|\hat\beta-\beta^\star\|_1 \lesssim \frac{s\lambda^2}{\kappa^2}

    A fixed-design LASSO oracle inequality stated through an L1 restricted-strong-eigenvalue condition.

    fixed_design_lasso_oracle_of_l1RSE
  • Debiased LASSO standard Wald interval coverage
    proved
    P ⁣(βj∈b^j±c s^j/an)→1−α\mathbb{P}\!\left(\beta_j\in \hat b_j \pm c\,\hat s_j/a_n\right)\to 1-\alpha

    An iid-score debiased LASSO theorem: row-approximation error, L1 consistency, studentization, and Gaussian critical-value calibration imply asymptotic standard Wald confidence-interval coverage.

    tendsto_measure_debiasedLasso_standardWaldCI_coverage_iidScoreSum_real
  • LASSO oracle prediction-error bound
    proved
    1m∥X(β^−β⋆)∥22≤16 λ2sκ2\tfrac{1}{m}\|X(\hat\beta-\beta^\star)\|_2^2 \le \frac{16\,\lambda^2 s}{\kappa^2}

    Under the Restricted Eigenvalue condition RE(s,3,κ) and a noise control on λ, the in-sample prediction error of the LASSO is bounded by a sparsity-scaled multiple of λ².

    lasso_oracle_prediction
2.7

Spectral perturbation

  • Weyl's inequality (per-index form)
    proved
    ∣λ~k(A+E)−λ~k(A)∣≤∥E∥op|\tilde\lambda_k(A+E) - \tilde\lambda_k(A)| \le \lVert E\rVert_{\mathrm{op}}

    Each sorted eigenvalue of a Hermitian matrix moves by at most the operator norm of the perturbation.

    weyl_sorted
  • Davis-Kahan eigenvector bound
    proved
    ∃ u^: ∥u^−u∥2≤4∥E∥opΔ\exists\,\hat u:\ \lVert \hat u - u\rVert_2 \le \tfrac{4\lVert E\rVert_{\mathrm{op}}}{\Delta}

    For a simple eigenvalue with eigengap Δ and a small symmetric perturbation, the perturbed unit eigenvector stays within 4‖E‖/Δ of the original.

    davis_kahan_eigvec
3

Nonparametric statistics

Statlib.Nonparametric
3.1

Nonparametric approximation

  • Holder-smooth ReLU approximation at the -2s/d rate
    proved
    f∈Hr+β([0,1]d)  ⟹  ∃g∈NL,W: sup⁡x∈[0,1]d∣g(x)−f(x)∣≤c (LW2)−2(r+β)/df\in\mathcal{H}^{r+\beta}([0,1]^d) \implies \exists g\in\mathcal{N}_{L,W}:\ \sup_{x\in[0,1]^d}|g(x)-f(x)|\le c\,(LW^2)^{-2(r+\beta)/d}

    An explicit fixed-width construction is converted into the architecture-scale ReLU approximation rate (L W^2)^(-2(r+beta)/d) for high-dimensional Holder-smooth functions.

    holderSmoothBall_unitCube_LW2_rate_from_fixed_width_M_rate
  • High-order multivariate B-spline Holder rate
    proved
    f0∈Hr+β([0,1]d)  ⟹  EmK(f0)≤M mK−2(r+β)/df_0\in\mathcal{H}^{r+\beta}([0,1]^d) \implies \mathcal{E}_{m_K}(f_0) \le M\,m_K^{-2(r+\beta)/d}

    A positive-degree tensor-product B-spline system on the high-dimensional unit cube achieves the uniform squared-error sieve rate m^(-2(r+beta)/d) over the trace Holder-smooth ball.

    unit_cube_bspline_high_order_holder_smooth_uniform_sieve_approximation_rate
  • Zero-order Holder selector-indicator sieve rate
    proved
    ∃ϕ: ∀f0∈Hα(C,B), Em(f0)≤ν(X)(CAα)2m−2α/d\exists\phi:\ \forall f_0\in\mathcal{H}^{\alpha}(C,B),\ \mathcal{E}_m(f_0)\le \nu(X)(C A^{\alpha})^2 m^{-2\alpha/d}

    A measurable m-cell selector cover gives a piecewise-constant selector-indicator sieve with integrated squared-error rate m^{-2 alpha / d} over a Holder ball.

    selector_indicator_uniform_sieve_holder_approximation_rate_of_cover