OAI/Probability/SKGap/Localization/AttractionBasinIUnion.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.attractionBasin_eq_iUnion line 15
2. lemma OAI.SKGap.isOpen_attractionBasin line 28
3. lemma OAI.SKGap.disjoint_attractionBasins line 34
4. theorem OAI.SKGap.lyapunov_unique_fixed_point line 42
5. theorem OAI.SKGap.local_contraction_attracts line 83
6. theorem OAI.SKGap.strict_derivative_attracts line 113
7. theorem OAI.SKGap.lipschitz_gradient_remainder line 131
8. theorem OAI.SKGap.gradient_step_strict_descent line 166
9. theorem OAI.SKGap.gradient_step_derivative_sq_bound line 179