OAI/Probability/SKGap/Localization/ThresholdChoice.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.Regression.thresholdChoice line 72
2. lemma OAI.SKGapCutoff.Regression.thresholdChoice_measurable line 75
3. lemma OAI.SKGapCutoff.Regression.thresholdChoice_decomposition line 80
4. theorem OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.threshold_map line 85
5. def OAI.SKGapCutoff.Regression.uniformSeedLaw line 141
6. instance OAI.SKGapCutoff.Regression.uniformSeedLaw_probability line 143
7. instance OAI.SKGapCutoff.Regression.uniformSeedLaw_noAtoms line 147
8. lemma OAI.SKGapCutoff.Regression.uniform_threshold_boundary_null line 151
9. def OAI.SKGapCutoff.DisorderTypical line 176
10. lemma OAI.SKGapCutoff.DisorderTypical.mono line 179
11. lemma OAI.SKGapCutoff.DisorderTypical.and line 188
12. lemma OAI.SKGapCutoff.disorderLimit_of_typical_bound line 203
13. lemma OAI.SKGapCutoff.cutoffTime_nonneg line 217
14. lemma OAI.SKGapCutoff.spin_mass_cutoff_error line 221
15. theorem OAI.SKGapCutoff.continuous_lower_from_typical_spin_mass line 258