OAI/Probability/RadialTransition/LinearInteractions.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RadialTransition.zero_ite_add line 16
2. lemma OAI.RadialTransition.pairWithin_add line 22
3. lemma OAI.RadialTransition.pairBetween_add line 27
4. lemma OAI.RadialTransition.pairCellEnergy_add line 31
5. lemma OAI.RadialTransition.pairCellEnergy_diagonal line 37
6. def OAI.RadialTransition.singleAttraction line 47
7. lemma OAI.RadialTransition.continuous_singleAttraction line 49
8. lemma OAI.RadialTransition.radialPair_singleAttraction line 52
9. lemma OAI.RadialTransition.deletedPair_macro_energy line 57
10. lemma OAI.RadialTransition.deletedPair_macroKac line 72