OAI/Probability/SKGap/Localization/ScalarConsistency.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.scalar_consistency line 54
2. lemma OAI.SKGap.scalarPsi_eq_entropy line 59
3. lemma OAI.SKGap.scalar_weak_test line 64
4. lemma OAI.SKGap.scalar_strict_test line 84
5. lemma OAI.SKGap.scalar_gaussian_curve line 98
6. lemma OAI.SKGap.continuousOn_scalar_test line 116
7. lemma OAI.SKGap.finite_pos_lower_bound line 135
8. theorem OAI.SKGap.compact_strict_witness line 148
9. lemma OAI.SKGap.compact_zero_fiber_neighborhood line 176
10. theorem OAI.SKGap.compact_small_noise_witness line 196