OAI/Probability/SKGap/Stability/TapFieldE.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.exists_small_gradient_step line 20
2. lemma OAI.SKGap.gradient_step_derivative_norm_lt line 36
3. theorem OAI.SKGap.gradient_unique_zero_on_compact line 59
4. lemma OAI.SKGap.weightedTapE_eq_zero_iff line 120
5. lemma OAI.SKGap.weightedTapE_coercive_on_box line 134
6. theorem OAI.SKGap.tap_unique_zero line 154
7. theorem OAI.SKGap.inverseOnConvex_bound line 187
8. def OAI.SKGap.tapFieldE line 245
9. lemma OAI.SKGap.tapFieldE_contDiff line 249
10. lemma OAI.SKGap.norm_EField_eq line 255
11. lemma OAI.SKGap.tapFieldE_fderiv line 258
12. lemma OAI.SKGap.vectorNorm_zero line 269
13. lemma OAI.SKGap.tapField_shift line 272
14. theorem OAI.SKGap.tap_root_and_distance line 278