OAI/Probability/BinarySweep/MatrixBounds/
179 declarations, 0 contain sorry, 0 declared as axioms; 19 files
Files
- BlockTrace.lean 14 declarations
- CenteredMatrix.lean 4 declarations
- FourierTrace.lean 2 declarations
- HilbertBlockTrace.lean 13 declarations
- MatrixProjection.lean 8 declarations
- MatrixRegularize.lean 8 declarations
- MatrixSqrtBlocks.lean 4 declarations
- PositiveTraceRestriction.lean 2 declarations
- SchattenBasic.lean 11 declarations
- SchattenBounds.lean 22 declarations
- SchattenTriangle.lean 5 declarations
- SparsePinching.lean 15 declarations
- SpectralMoment.lean 10 declarations
- SymmetricDensity.lean 7 declarations
- TraceConvex.lean 12 declarations
- TraceDensityComparison.lean 4 declarations
- TraceHolder.lean 4 declarations
- TraceInterpolation.lean 21 declarations
- Whitening.lean 13 declarations