OAI/Probability/SKGap/Localization/JumpEnergy.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.semigroup_hasDerivAt line 13
2. lemma OAI.SKGapCutoff.semigroup_hasDerivAt' line 18
3. lemma OAI.SKGapCutoff.semigroup_apply_hasDerivAt line 23
4. lemma OAI.SKGapCutoff.semigroup_apply_hasDerivAt' line 29
5. lemma OAI.SKGapCutoff.semigroup_continuous line 35
6. lemma OAI.SKGapCutoff.semigroup_zero line 41
7. def OAI.SKGapCutoff.jumpEnergy line 44
8. lemma OAI.SKGapCutoff.generator_square line 47
9. lemma OAI.SKGapCutoff.backward_flow_hasDerivAt line 53
10. lemma OAI.SKGapCutoff.backward_square_hasDerivAt line 60
11. lemma OAI.SKGapCutoff.interpolated_square_hasDerivAt line 72
12. lemma OAI.SKGapCutoff.jumpEnergy_continuous line 89
13. lemma OAI.SKGapCutoff.interpolated_energy_continuous line 94
14. lemma OAI.SKGapCutoff.semigroup_variance_integral line 102
15. lemma OAI.SKGapCutoff.jumpWeight_bounds line 112
16. lemma OAI.SKGapCutoff.jumpEnergy_nonneg line 119
17. lemma OAI.SKGapCutoff.jumpEnergy_le_gradient line 125
18. lemma OAI.SKGapCutoff.semigroup_mono line 135
19. lemma OAI.SKGapCutoff.semigroup_le_const line 141
20. theorem OAI.SKGapCutoff.semigroup_variance_le line 146
21. lemma OAI.real_exp_remainder_le line 173