OAI/Probability/SKGap/Matrix/
988 declarations, 0 contain sorry, 0 declared as axioms; 89 files
Files
- BufferedClosedWord.lean 12 declarations
- ClosedErrorTrace.lean 10 declarations
- ClosedMatrix.lean 8 declarations
- ClosedTrace.lean 32 declarations
- ClosedTreeMatrix.lean 14 declarations
- CompletedMatrix.lean 13 declarations
- ConditionalEmpiricalNorm.lean 7 declarations
- ConditionalMiddleNorm.lean 6 declarations
- CorrectionTrace.lean 8 declarations
- DiscreteMatrixCalculus.lean 34 declarations
- DoublePlantLogNorm.lean 18 declarations
- DoublePlantedGOEArray.lean 8 declarations
- FixedNormRecipeEvent.lean 31 declarations
- FockTensor.lean 25 declarations
- GOEBilinearCov.lean 11 declarations
- GOEBlockExpansion.lean 3 declarations
- GOEDiagonalSquare.lean 6 declarations
- GOEGlobalEvents.lean 2 declarations
- GOERegression.lean 16 declarations
- GOEResidualCov.lean 11 declarations
- GOERowLaw.lean 3 declarations
- GOESparse.lean 7 declarations
- GOESubmatrix.lean 12 declarations
- GapHalfSmallOpNorm.lean 2 declarations
- GlobalWordIncrement.lean 4 declarations
- GoeInverseLoopCentered.lean 1 declarations
- InverseDiagram.lean 21 declarations
- InverseSeries.lean 31 declarations
- InverseSubSquareMul.lean 3 declarations
- LiftMatrix.lean 21 declarations
- LipschitzNormedConvolution.lean 25 declarations
- LiteralTrace.lean 7 declarations
- LogDetConcentration.lean 3 declarations
- LogDetExpected.lean 4 declarations
- LogDetIntegral.lean 13 declarations
- LogDetUniform.lean 2 declarations
- LoopPrediction.lean 17 declarations
- MarkedWordIBP.lean 19 declarations
- MatrixCoordinates.lean 12 declarations
- MatrixEntryCLM.lean 9 declarations
- MatrixLogDet.lean 7 declarations
- MatrixQuad.lean 16 declarations
- MatrixSeminorm.lean 15 declarations
- MatrixWhitening.lean 3 declarations
- MatrixWordIncrement.lean 6 declarations
- MatrixWordRegularity.lean 9 declarations
- MeasurableCompletedMatrix.lean 3 declarations
- NormalLogConst.lean 18 declarations
- NormalLogDensityCentered.lean 2 declarations
- NormalizedInfluence.lean 21 declarations
- NormalizedPrimaryRecipe.lean 11 declarations
- NormalizedRecipeLaw.lean 7 declarations
- OpNorm.lean 11 declarations
- OpNormDiagonal.lean 6 declarations
- OpNormKernelMatrixSub.lean 13 declarations
- PolynomialCoeListSum.lean 3 declarations
- PrimaryMatrix.lean 26 declarations
- PrimaryWordControl.lean 8 declarations
- PrimaryWordEventBinding.lean 6 declarations
- PrimitiveTrace.lean 25 declarations
- RankNorm.lean 7 declarations
- RealSymmetricResolventUnit.lean 3 declarations
- RecipeNodeTrace.lean 7 declarations
- RecipeTraceBudget.lean 12 declarations
- RecipeWordEvent.lean 4 declarations
- RegularizedLogDet.lean 21 declarations
- StartedMatrixEvent.lean 4 declarations
- StartedNodeTrace.lean 5 declarations
- StartedTraceBudget.lean 4 declarations
- StartedWordClosure.lean 11 declarations
- StaticCovarianceMatrix.lean 12 declarations
- TanhMatrixBounds.lean 11 declarations
- Trace.lean 7 declarations
- Word.lean 8 declarations
- WordBaseBias.lean 11 declarations
- WordBiasCutoff.lean 2 declarations
- WordBiasInduction.lean 7 declarations
- WordDerivative.lean 11 declarations
- WordDiag.lean 3 declarations
- WordDiagUniform.lean 8 declarations
- WordExpectedRecursion.lean 2 declarations
- WordFockSeries.lean 36 declarations
- WordIncrement.lean 20 declarations
- WordLeading.lean 5 declarations
- WordLoop.lean 12 declarations
- WordLoopLeading.lean 8 declarations
- WordPartnerContraction.lean 28 declarations
- WordSimultaneousPrediction.lean 1 declarations
- WordTemplateSurjective.lean 11 declarations