OAI/Probability/SKGap/Localization/PlantedFixedTime.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.badFieldSet_mono_margin line 13
2. def OAI.SKGap.plantedRootBad line 18
3. lemma OAI.SKGap.plantedRootBad_mono line 25
4. lemma OAI.SKGap.two_exponential_tails line 32
5. theorem OAI.SKGap.planted_fixed_time_root_stability line 49
6. lemma OAI.SKGap.tapField_add_diagonal line 92
7. lemma OAI.SKGap.tapField_diagonal_difference_bound line 101
8. lemma OAI.SKGap.hessian_diagonal_difference line 111
9. lemma OAI.SKGap.hessian_diagonal_difference_bound line 134
10. lemma OAI.SKGap.mulvec_add_diagonal_bound line 148