OAI/Probability/SKGap/Localization/ScalarSmallNoiseTests.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.scalar_small_noise_tests line 28
2. lemma OAI.SKGap.continuousOn_scalarPsi_of_pos line 55
3. theorem OAI.SKGap.scalar_compact_isolation line 62
4. lemma OAI.SKGap.scalar_quadratic_envelope line 96
5. lemma OAI.SKGap.sum_centered_sq_lower line 117
6. lemma OAI.SKGap.multiple_gaussian_integrable line 124
7. lemma OAI.SKGap.multiple_gaussian_integral line 129
8. theorem OAI.SKGap.quadratic_envelope_tail line 137
9. lemma OAI.SKGap.choose_quadratic_tail_radius line 165