OAI/Probability/SKBarriers/Replicas/MatrixSKGuerra.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SK.Analytic.matrixSKLogPartition line 18
2. theorem OAI.SK.Analytic.matrixSKLogPartition_continuous line 21
3. theorem OAI.SK.Analytic.matrixSKQuenched_endpoint line 29
4. theorem OAI.SK.Analytic.matrixSKGuerra line 39
5. def OAI.SK.Analytic.MatrixStates line 81
6. instance OAI.SK.Analytic.matrixStatesFintype line 84
7. def OAI.SK.Analytic.matrixConstrainedPressure line 90
8. theorem OAI.SK.Analytic.matrixConstrainedPressure_le line 94