OAI/Probability/SKGap/Terminal/SpinDifferenceEnergy.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.spinDifferenceEnergy line 160
2. lemma OAI.SKGapCutoff.spinDifferenceEnergy_eq line 163
3. lemma OAI.SKGapCutoff.halfDiff_spinDifferenceEnergy line 172
4. lemma OAI.SKGapCutoff.refreshGenerator_spinDifferenceEnergy_le line 186
5. lemma OAI.SKGapCutoff.refreshSemigroup_sub_initial_le line 200
6. lemma OAI.SKGapCutoff.refreshSemigroup_spinDifferenceEnergy line 218
7. def OAI.SKGapCutoff.spinEuclidean line 225
8. lemma OAI.SKGapCutoff.spinEuclidean_sub_norm_sq line 228
9. theorem OAI.SKGapCutoff.refresh_lipschitz_recipe_short_time line 233