OAI/Probability/SKGap/Terminal/FiniteSpinCalculus.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SKGap.spinValue_true line 16
2. theorem OAI.SKGap.spinValue_false line 17
3. theorem OAI.SKGap.spinValue_not line 18
4. theorem OAI.SKGap.spinValue_sq line 20
5. theorem OAI.SKGap.coupling_diag line 23
6. theorem OAI.SKGap.coupling_symm line 26
7. theorem OAI.SKGap.flip_same line 32
8. theorem OAI.SKGap.flip_other line 35
9. theorem OAI.SKGap.flip_flip line 38
10. def OAI.SKGap.flipEquiv line 44
11. theorem OAI.SKGap.sum_flip line 47
12. theorem OAI.SKGap.weight_pos line 50
13. theorem OAI.SKGap.partition_pos line 53
14. theorem OAI.SKGap.mass_pos line 56
15. theorem OAI.SKGap.mass_nonneg line 59
16. theorem OAI.SKGap.sum_mass line 62
17. theorem OAI.SKGap.expectation_const line 66
18. theorem OAI.SKGap.expectation_add line 70
19. theorem OAI.SKGap.expectation_sub line 74
20. theorem OAI.SKGap.expectation_mul_const line 78
21. theorem OAI.SKGap.expectation_const_mul line 82
22. theorem OAI.SKGap.expectation_nonneg line 86
23. theorem OAI.SKGap.variance_nonneg line 90
24. theorem OAI.SKGap.dirichlet_nonneg line 93
25. theorem OAI.SKGap.variance_eq_zero_iff line 97
26. theorem OAI.SKGap.variance_pos_of_ne line 105
27. theorem OAI.SKGap.exists_positive_variance line 112
28. theorem OAI.SKGap.lower_bound_discreteGap line 119
29. instance OAI.SKGap.disorderLaw_probability line 130
30. theorem OAI.SKGap.gap_probability_of_poincare line 134