OAI/Probability/SKGap/Gaussian/
452 declarations, 0 contain sorry, 0 declared as axioms; 56 files
Files
- AdaptiveInnovationSquareTails.lean 1 declarations
- ConditionalGramTail.lean 6 declarations
- ConditionalUniformTail.lean 1 declarations
- DiagonalNormTail.lean 1 declarations
- FourierMoment.lean 6 declarations
- GOEGaussian.lean 5 declarations
- GOERowTail.lean 4 declarations
- GOEScalarTail.lean 4 declarations
- GaussMoment.lean 27 declarations
- GaussianCompactTailRate.lean 3 declarations
- GaussianCoordinateMemLp.lean 4 declarations
- GaussianCoordinates.lean 10 declarations
- GaussianDisintegration.lean 3 declarations
- GaussianFiniteIBPError.lean 1 declarations
- GaussianGramMomentsJoined.lean 16 declarations
- GaussianLinearDensity.lean 10 declarations
- GaussianMarginal.lean 10 declarations
- GaussianMatrixChaining.lean 3 declarations
- GaussianPDFMoment.lean 2 declarations
- GaussianPartition.lean 12 declarations
- GaussianProductIntegral.lean 4 declarations
- GaussianProductPower.lean 16 declarations
- GaussianProductUpperTailLipschitz.lean 1 declarations
- GaussianQuadratic.lean 13 declarations
- GaussianQuadraticSupComparison.lean 4 declarations
- GaussianRankCorrection.lean 17 declarations
- GaussianRecipeEvent.lean 8 declarations
- GaussianReductionPointwise.lean 2 declarations
- GaussianRegression.lean 11 declarations
- GaussianSign.lean 7 declarations
- GaussianSquareTail.lean 9 declarations
- GaussianTailScale.lean 9 declarations
- GaussianTiltIdentity.lean 4 declarations
- GaussianTiltMass.lean 5 declarations
- GaussianVectorMoments.lean 4 declarations
- IndependentBoundedAverageTailLaw.lean 5 declarations
- LiteralWeakTail.lean 1 declarations
- LocalGaussianMoments.lean 15 declarations
- MatrixNormTail.lean 7 declarations
- MatrixWordMoments.lean 4 declarations
- PartitionSecondMoment.lean 11 declarations
- PhiMoments.lean 14 declarations
- PhiStein.lean 17 declarations
- ProductGaussianDensity.lean 2 declarations
- RegressionMoments.lean 3 declarations
- ReplicaTailWeight.lean 18 declarations
- SampledInnerTailScaled.lean 3 declarations
- ScalarGaussianReductionAlgebra.lean 7 declarations
- ScalarMomentGram.lean 5 declarations
- SquareTail.lean 11 declarations
- SquareTail2.lean 27 declarations
- SquaredGaussianFourth.lean 35 declarations
- StandardGaussianProduct.lean 10 declarations
- StdGaussianMgfLipschitz.lean 4 declarations
- SteinRecipeRegularity.lean 4 declarations
- SubgaussianAbsTail.lean 6 declarations