OAI/Probability/SKGap/Stability/HalfDiffField.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.halfDiff_field line 155
2. lemma OAI.SKGapCutoff.halfDiff_field_add line 161
3. lemma OAI.SKGapCutoff.refreshSemigroup_eq_preparationFlow line 168
4. theorem OAI.SKGapCutoff.preparation_poincare line 174
5. lemma OAI.SKGapCutoff.interval_hasFDerivAt_of_continuous line 206
6. lemma OAI.SKGapCutoff.algebra_exp_contDiff line 228
7. lemma OAI.SKGapCutoff.algebra_duhamel line 232
8. lemma OAI.SKGapCutoff.algebra_exp_smul_hasFDerivAt line 254
9. lemma OAI.SKGapCutoff.algebra_exp_curve_hasDerivAt line 296
10. def OAI.SKGapCutoff.meanGeneratorCLM line 311
11. lemma OAI.SKGapCutoff.meanGeneratorCLM_apply line 314
12. def OAI.SKGapCutoff.meanGeneratorMapLM line 323
13. def OAI.SKGapCutoff.meanGeneratorMap line 333
14. lemma OAI.SKGapCutoff.meanGeneratorMap_apply line 337
15. lemma OAI.SKGapCutoff.refreshGeneratorCLM_eq_mean line 340
16. lemma OAI.SKGapCutoff.preparation_mean_hasDerivAt line 344
17. lemma OAI.SKGapCutoff.preparation_generator_hasDerivAt line 355
18. lemma OAI.SKGapCutoff.preparation_semigroup_hasDerivAt line 365
19. theorem OAI.SKGapCutoff.preparation_expectation_hasDerivAt line 373