OAI/Probability/BinarySweep/Representations/
107 declarations, 0 contain sorry, 0 declared as axioms; 14 files
Files
- CharacterComplete.lean 2 declarations
- FiniteUnitaryAverage.lean 14 declarations
- IrrepSupport.lean 4 declarations
- IrrepTransport.lean 7 declarations
- IsotypicCentrality.lean 2 declarations
- IsotypicDensity.lean 10 declarations
- IsotypicMoment.lean 7 declarations
- IsotypicOrthogonal.lean 3 declarations
- IsotypicProjectionMoment.lean 18 declarations
- IsotypicSpectral.lean 8 declarations
- IsotypicTrace.lean 5 declarations
- MatrixIsotypicWhitening.lean 7 declarations
- MultiplicityBound.lean 16 declarations
- UnitaryTransport.lean 4 declarations