OAI/Probability/SKGap/Gaussian/GaussianTailScale.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.exists_gaussian_tail_quantile line 12
2. lemma OAI.SKGap.eventually_sqrt_cost_le_linear line 24
3. lemma OAI.SKGap.gaussianSpinPartition_log_mean_lower line 55
4. lemma OAI.SKGap.gaussianSpinPartition_lower_tail_bound line 72
5. lemma OAI.SKGap.gaussianSpinPartition_lower_tail_tendsto line 102
6. lemma OAI.SKGap.gaussian_disorder_hasLaw line 134
7. lemma OAI.SKGap.partition_zero_measurable line 151
8. lemma OAI.SKGap.disorder_partition_mean line 159
9. theorem OAI.SKGap.disorder_partition_lower_tail line 165