OAI/Analysis/FreeEntropy/GUEConcentration.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteEntropySeparation.complex_mean_square_bound line 11
2. theorem OAI.FiniteEntropySeparation.real_tendsto_zero_of_inv_sq line 27
3. theorem OAI.FiniteEntropySeparation.matrixTraceWord_mean_square_tendsto line 32
4. theorem OAI.FiniteEntropySeparation.probability_error_le_mean_square line 47
5. theorem OAI.FiniteEntropySeparation.matrixTraceWord_probability_tendsto line 55