OAI/Probability/SwitchChain/PairSquaredEnergy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem315.PairSquaredEnergy.reverseMove line 10
2. lemma OAI.Problem315.PairSquaredEnergy.reverseMove_involutive line 14
3. def OAI.Problem315.PairSquaredEnergy.reverseMoveEquiv line 29
4. lemma OAI.Problem315.PairSquaredEnergy.reverseMove_fst line 33
5. lemma OAI.Problem315.PairSquaredEnergy.crossingPairs_reverse line 42
6. lemma OAI.Problem315.PairSquaredEnergy.reverseMove_crossing line 50
7. theorem OAI.Problem315.PairSquaredEnergy.involution_energy line 58
8. theorem OAI.Problem315.PairSquaredEnergy.pairSwitchLaplacian_energy line 77