OAI/Probability/SKGap/Localization/JumpWeight.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.jumpWeight line 25
2. lemma OAI.SKGapCutoff.jumpWeight_pos line 28
3. def OAI.SKGapCutoff.influence line 36
4. def OAI.SKGapCutoff.vectorSquare line 39
5. def OAI.SKGapCutoff.vectorDissipation line 42
6. lemma OAI.SKGapCutoff.vectorSquare_nonneg line 46
7. lemma OAI.SKGapCutoff.vectorDissipation_nonneg line 49
8. lemma OAI.SKGapCutoff.generator_vectorSquare line 54
9. lemma OAI.SKGapCutoff.gradient_square_identity line 65
10. lemma OAI.SKGapCutoff.weighted_cross_young line 85
11. lemma OAI.SKGapCutoff.gradient_first_order_bound line 93
12. lemma OAI.SKGapCutoff.gradient_square_le line 129
13. lemma OAI.SKGapCutoff.gradientSemigroup_apply_hasDerivAt line 139
14. lemma OAI.SKGapCutoff.backward_gradient_hasDerivAt line 149
15. lemma OAI.SKGapCutoff.backward_vectorSquare_hasDerivAt line 157
16. def OAI.SKGapCutoff.roughDefect line 170
17. lemma OAI.SKGapCutoff.roughDefect_nonneg line 175
18. lemma OAI.SKGapCutoff.interpolated_vectorSquare_hasDerivAt line 185
19. lemma OAI.SKGapCutoff.rough_vector_propagation line 209
20. lemma OAI.SKGapCutoff.gradientSemigroup_continuous line 239
21. lemma OAI.SKGapCutoff.vectorDissipation_continuous line 244
22. lemma OAI.SKGapCutoff.roughDefect_continuous line 249
23. lemma OAI.SKGapCutoff.interpolated_vector_continuous line 254
24. lemma OAI.SKGapCutoff.rough_vector_dissipation line 264