OAI/Probability/SKRatio/Dynamics/Concentration.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatio.Calculus.flip_sub line 12
2. lemma OAI.SKRatio.Calculus.backward_flow_hasDerivAt line 25
3. lemma OAI.SKRatio.Calculus.backward_square_hasDerivAt line 32
4. lemma OAI.SKRatio.Calculus.interpolated_square_hasDerivAt line 45
5. lemma OAI.SKRatio.Calculus.jumpEnergy_continuous line 62
6. lemma OAI.SKRatio.Calculus.interpolated_energy_continuous line 67
7. lemma OAI.SKRatio.Calculus.semigroup_variance_integral line 75
8. lemma OAI.SKRatio.Calculus.jumpWeight_bounds line 85
9. lemma OAI.SKRatio.Calculus.jumpEnergy_nonneg line 92
10. lemma OAI.SKRatio.Calculus.jumpEnergy_le_gradient line 98
11. lemma OAI.SKRatio.Calculus.semigroup_le_const line 108
12. theorem OAI.SKRatio.Calculus.semigroup_variance_le line 113
13. lemma OAI.SKRatio.Calculus.real_exp_remainder_le line 138
14. def OAI.SKRatio.Calculus.expDrift line 161
15. lemma OAI.SKRatio.Calculus.expDrift_eq_sum line 166
16. lemma OAI.SKRatio.Calculus.flipRate_nonneg line 179
17. lemma OAI.SKRatio.Calculus.jumpEnergy_eq_jump_square line 184
18. lemma OAI.SKRatio.Calculus.abs_flip_sub_le line 193
19. lemma OAI.SKRatio.Calculus.expDrift_le line 203
20. lemma OAI.SKRatio.Calculus.backward_exp_hasDerivAt line 244
21. lemma OAI.SKRatio.Calculus.interpolated_exp_hasDerivAt line 256
22. lemma OAI.SKRatio.Calculus.semigroup_pos line 273
23. lemma OAI.SKRatio.Calculus.expDrift_continuous line 280
24. lemma OAI.SKRatio.Calculus.interpolated_exp_continuous line 285
25. lemma OAI.SKRatio.Calculus.interpolated_expDrift_continuous line 294
26. theorem OAI.SKRatio.Calculus.semigroup_jump_mgf line 302