OAI/Probability/SKGap/Localization/ExpDrift.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.expDrift line 15
2. lemma OAI.SKGapCutoff.expDrift_eq_sum line 20
3. lemma OAI.SKGapCutoff.flipRate_nonneg line 33
4. lemma OAI.SKGapCutoff.jumpEnergy_eq_jump_square line 38
5. lemma OAI.SKGapCutoff.abs_flip_sub_le line 47
6. lemma OAI.SKGapCutoff.expDrift_le line 57
7. lemma OAI.SKGapCutoff.backward_exp_hasDerivAt line 98
8. lemma OAI.SKGapCutoff.interpolated_exp_hasDerivAt line 109
9. lemma OAI.SKGapCutoff.semigroup_pos line 126
10. lemma OAI.SKGapCutoff.expDrift_continuous line 133
11. lemma OAI.SKGapCutoff.interpolated_exp_continuous line 138
12. lemma OAI.SKGapCutoff.interpolated_expDrift_continuous line 147
13. theorem OAI.SKGapCutoff.semigroup_jump_mgf line 155