OAI/Analysis/FreeEntropy/TotalSecond.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteEntropySeparation.totalSecond line 10
2. theorem OAI.FiniteEntropySeparation.totalSecond_continuous line 11
3. theorem OAI.FiniteEntropySeparation.totalSecond_matrix line 14
4. theorem OAI.FiniteEntropySeparation.totalSecond_norm_bound line 16
5. theorem OAI.FiniteEntropySeparation.wordMoment_second line 28
6. theorem OAI.FiniteEntropySeparation.Model.totalSecond_X line 35
7. theorem OAI.FiniteEntropySeparation.Model.totalSecond_X_lt line 38
8. theorem OAI.FiniteEntropySeparation.Model.totalSecond_heat_le line 47
9. theorem OAI.FiniteEntropySeparation.Model.diagonalMicrostates_norm_eventually line 59