OAI/Probability/SKRatio/Matrices/
853 declarations, 0 contain sorry, 0 declared as axioms; 85 files
Files
- AbsMulEntryBound.lean 2 declarations
- AugmentedBounds.lean 10 declarations
- AugmentedSquares.lean 15 declarations
- BrownianUnitLaw.lean 4 declarations
- ClosedConvexNonempty.lean 9 declarations
- CompactMatrixMasks.lean 8 declarations
- ConditionalAffineSquares.lean 4 declarations
- ConditionalGaussianSquares.lean 2 declarations
- CoordinateDeriv.lean 6 declarations
- DetMultilinear.lean 7 declarations
- DiagonalSqrt.lean 8 declarations
- DiagonalSum.lean 8 declarations
- DiagonalTMemLp.lean 5 declarations
- EntryLM.lean 14 declarations
- ExpDuhamel.lean 3 declarations
- ExpSum.lean 38 declarations
- FiniteCoordinateDeriv.lean 6 declarations
- FiniteMax.lean 23 declarations
- FiniteTimeMesh.lean 1 declarations
- Fl1.lean 22 declarations
- FourierMoment.lean 6 declarations
- FrobeniusSq.lean 6 declarations
- GOERegression.lean 52 declarations
- GaussianAffineGaussianSup.lean 3 declarations
- GaussianCoordinateMemLp.lean 4 declarations
- GaussianCoordinates.lean 10 declarations
- GaussianFiniteIBPError.lean 1 declarations
- GaussianProductIntegral.lean 4 declarations
- GaussianProductUpperTailLipschitz.lean 1 declarations
- GaussianQuadratic.lean 13 declarations
- GaussianQuadraticSupComparison.lean 1 declarations
- GaussianRows.lean 4 declarations
- GaussianSquareMatrix.lean 29 declarations
- GaussianSquareTails.lean 28 declarations
- GaussianSupport.lean 26 declarations
- GaussianTails.lean 17 declarations
- GoeInverseLoopCentered.lean 1 declarations
- GoeMatrixQuadCoeff.lean 7 declarations
- Imaginary.lean 14 declarations
- IntegralAbsSet.lean 2 declarations
- IntegralProductDeviation.lean 2 declarations
- InverseSubSquareMul.lean 3 declarations
- LiftMatrix.lean 21 declarations
- Lin.lean 15 declarations
- LinCLM.lean 5 declarations
- LinEquiv.lean 4 declarations
- LinSub.lean 7 declarations
- LipschitzNormedConvolution.lean 25 declarations
- MatrixCoordinates.lean 12 declarations
- MatrixEntryCLM.lean 9 declarations
- MatrixQuad.lean 9 declarations
- NormalizedIncrement.lean 6 declarations
- OpNorm.lean 11 declarations
- OpNormKernelMatrixSub.lean 2 declarations
- OpNormNonneg.lean 11 declarations
- PathEnergy.lean 6 declarations
- PathEvaluations.lean 12 declarations
- PathResolvent.lean 3 declarations
- PlantedGOE.lean 22 declarations
- PlantedSquares.lean 10 declarations
- PowExponentialPair.lean 4 declarations
- Quadratic.lean 13 declarations
- QuadraticCoeff.lean 11 declarations
- RandomMatrixBounded.lean 10 declarations
- RandomMatrixNet.lean 6 declarations
- RealPart.lean 9 declarations
- RealPartCLM.lean 10 declarations
- RealSymmetricResolventUnit.lean 3 declarations
- RowGeometry.lean 15 declarations
- SandShift.lean 8 declarations
- SandShiftSpecial.lean 5 declarations
- ScaledDiagonalExpectedMargin.lean 3 declarations
- Spin.lean 48 declarations
- StandardGaussianProduct.lean 7 declarations
- StdGaussianMgfLipschitz.lean 4 declarations
- SymmetricElementaryComm.lean 3 declarations
- TendstoGaussianPDFRealTop.lean 3 declarations
- TruncatedG.lean 6 declarations
- TruncationGoodSet.lean 7 declarations
- UnitBall.lean 22 declarations
- UnitInterval.lean 10 declarations
- Vectorize.lean 11 declarations
- WeightedDiagonalSquares.lean 4 declarations
- WeightedGaussianSquares.lean 4 declarations
- WeightedSquares.lean 8 declarations