OAI/Probability/SKGap/Localization/ComponentRefresh.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.componentRefresh line 163
2. def OAI.SKGapCutoff.componentGenerator line 167
3. def OAI.SKGapCutoff.vectorDerivativeSquare line 170
4. lemma OAI.SKGapCutoff.refresh_jensen_square line 173
5. lemma OAI.SKGapCutoff.componentRefresh_vectorSquare line 186
6. lemma OAI.SKGapCutoff.componentRefresh_derivativeSquare line 197
7. def OAI.SKGapCutoff.refreshCorrection line 223
8. lemma OAI.SKGapCutoff.refreshCorrection_square line 226
9. lemma OAI.SKGapCutoff.componentRefresh_hasDerivAt line 262
10. lemma OAI.SKGapCutoff.gradientComponent_interpolate_hasDerivAt line 271
11. def OAI.SKGapCutoff.vectorEvalEuclideanLM line 284
12. def OAI.SKGapCutoff.vectorEvalEuclidean line 290
13. lemma OAI.SKGapCutoff.vectorEvalEuclidean_norm_sq line 294
14. lemma OAI.SKGapCutoff.gradient_component_difference line 299
15. lemma OAI.SKGapCutoff.component_correction_bound line 351
16. lemma OAI.SKGapCutoff.vectorSquare_sub_triangle line 387
17. lemma OAI.SKGapCutoff.componentRefresh_difference line 393
18. theorem OAI.SKGapCutoff.refreshGradient_short_time line 408