OAI/Analysis/FreeEntropy/GUEBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteEntropySeparation.jointNoiseBound line 11
2. def OAI.FiniteEntropySeparation.jointMomentBound line 12
3. theorem OAI.FiniteEntropySeparation.jointNoiseBound_nonneg line 15
4. theorem OAI.FiniteEntropySeparation.jointNoiseBound_measurable line 17
5. theorem OAI.FiniteEntropySeparation.jointMatrix_norm_bound line 19
6. theorem OAI.FiniteEntropySeparation.jointNoiseBound_power line 31
7. theorem OAI.FiniteEntropySeparation.jointNoiseBound_moment line 37
8. theorem OAI.FiniteEntropySeparation.matrixTraceWord_variance_bound line 61