OAI/Probability/SKBarriers/SpinGlass/GaugeSymmetry.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SK.logPartitionProxy line 12
2. theorem OAI.SK.logPartition_subGaussian line 15
3. theorem OAI.SK.logPartition_upper_tail line 27
4. theorem OAI.SK.logPartition_lower_tail line 32
5. def OAI.SK.gaugeConfig line 37
6. theorem OAI.SK.spin_beq line 39
7. theorem OAI.SK.gaugeConfig_involutive line 42
8. def OAI.SK.gaugeConfigEquiv line 47
9. def OAI.SK.gaugeDisorder line 53
10. theorem OAI.SK.gaugeDisorder_coordinate_law line 56
11. theorem OAI.SK.gaugeDisorder_law line 66
12. theorem OAI.SK.hamiltonian_gauge line 73
13. theorem OAI.SK.partition_gauge line 82
14. theorem OAI.SK.gibbs_gauge line 88
15. theorem OAI.SK.gaugeConfig_self line 92
16. theorem OAI.SK.gaugeConfig_true line 97
17. theorem OAI.SK.gibbs_integral_gauge line 102
18. theorem OAI.SK.gibbs_integral_eq line 108
19. theorem OAI.SK.gibbs_integral_uniform line 114