OAI/Probability/FreeIsing/Spins/Kernel.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.isingSpin_neg_ne_pos line 9
2. theorem OAI.Problem367.isingSpin_pos_ne_neg line 11
3. theorem OAI.Problem367.spinKernel_univ line 13
4. theorem OAI.Problem367.sum_isingSpin line 15
5. def OAI.Problem367.spinSign line 19
6. theorem OAI.Problem367.spinSign_neg line 23
7. theorem OAI.Problem367.spinSign_pos line 24
8. theorem OAI.Problem367.spinSign_sq line 26
9. theorem OAI.Problem367.spinSign_mul_self line 29
10. theorem OAI.Problem367.spinSign_mul line 32
11. def OAI.Problem367.transitionKernel line 36
12. theorem OAI.Problem367.transitionKernel_eq line 39
13. theorem OAI.Problem367.transitionKernel_symm line 43
14. theorem OAI.Problem367.transitionKernel_zero line 48
15. theorem OAI.Problem367.transitionKernel_one line 52
16. theorem OAI.Problem367.sum_spinSign line 56
17. theorem OAI.Problem367.transitionKernel_sum line 59
18. theorem OAI.Problem367.transitionKernel_spinSum line 65
19. theorem OAI.Problem367.transitionKernel_comp line 71
20. theorem OAI.Problem367.transitionKernel_nonneg line 78
21. theorem OAI.Problem367.transitionKernel_le_one line 83
22. def OAI.Problem367.transitionKernelIter line 88
23. theorem OAI.Problem367.transitionKernelIter_eq line 93
24. theorem OAI.Problem367.transitionKernelIter_sum line 100
25. theorem OAI.Problem367.transitionKernelIter_spinSum line 104
26. theorem OAI.Problem367.transitionKernel_stationary line 109
27. theorem OAI.Problem367.transitionKernelIter_correlation line 115
28. theorem OAI.Problem367.freeCylinderWeight_eq_transitionKernel line 123