OAI/Probability/SKGap/Terminal/PairInteraction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.gap_le_eigenrate line 13
2. def OAI.SKGapCutoff.pairInteraction line 34
3. lemma OAI.SKGapCutoff.pairInteraction_symm line 36
4. lemma OAI.SKGapCutoff.pairInteraction_diag line 40
5. lemma OAI.SKGapCutoff.tanh_mul_spin line 44
6. lemma OAI.SKGapCutoff.pair_field_zero line 48
7. lemma OAI.SKGapCutoff.pair_field_one line 51
8. lemma OAI.SKGapCutoff.pair_magnetization_eigen line 54
9. lemma OAI.SKGapCutoff.magnetization_centered line 60
10. lemma OAI.SKGapCutoff.pair_gap_upper line 66
11. theorem OAI.SKGapCutoff.no_all_interaction_gap line 72