OAI/Probability/SKGap/Stability/GaugeStabilityLaw.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.ObservationBridge.operatorBound line 17
2. lemma OAI.SKGap.ObservationBridge.isClosed_operatorBound line 20
3. def OAI.SKGap.ObservationBridge.literalBadPair line 28
4. lemma OAI.SKGap.ObservationBridge.measurableSet_literalBadPair line 31
5. lemma OAI.SKGap.ObservationBridge.spinMatrixAct_involutive line 36
6. lemma OAI.SKGap.ObservationBridge.spinMatrixAct_mulVec line 44
7. lemma OAI.SKGap.ObservationBridge.operatorBound_spin_iff line 54
8. lemma OAI.SKGap.ObservationBridge.literalBadPair_spin_iff line 66
9. lemma OAI.SKGap.ObservationBridge.gaussianSign_variance_preserving line 76
10. def OAI.SKGap.ObservationBridge.edgeSpinSign line 89
11. lemma OAI.SKGap.ObservationBridge.edgeSpinSign_sq line 90
12. def OAI.SKGap.ObservationBridge.plantedEdges line 93
13. def OAI.SKGap.ObservationBridge.plusPlantedEdges line 95
14. lemma OAI.SKGap.ObservationBridge.coupling_planted_gauge line 97
15. lemma OAI.SKGap.ObservationBridge.spin_observation line 113
16. lemma OAI.SKGap.ObservationBridge.continuous_coupling line 121
17. theorem OAI.SKGap.ObservationBridge.gauged_fixed_time_probability line 129