OAI/Probability/SKGap/Stability/PlantedFieldArray.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.Regression.plantedFieldArray line 180
2. lemma OAI.SKGapCutoff.Regression.plantedFieldArray_measurable line 184
3. lemma OAI.SKGapCutoff.Regression.planted_field_event_eq line 188
4. lemma OAI.SKGapCutoff.Regression.plantedField_common_convergence line 199
5. lemma OAI.SKGapCutoff.Regression.plantedField_mean_bound line 226
6. lemma OAI.SKGapCutoff.Regression.plantedField_scale_bound line 235
7. lemma OAI.SKGapCutoff.Regression.plantedFieldArray_squareTails line 246
8. def OAI.SKGapCutoff.Regression.plantedFieldLimitLaw line 277
9. instance OAI.SKGapCutoff.Regression.plantedFieldLimitLaw_probability line 280
10. lemma OAI.SKGapCutoff.Regression.plantedFieldArray_empirical line 284
11. lemma OAI.SKGapCutoff.Regression.plantedFieldLimitLaw_secondMoment line 308
12. lemma OAI.SKGapCutoff.Regression.plantedFieldArray_secondMoment line 333
13. lemma OAI.SKGapCutoff.Regression.ExponentiallyRare.without_prefactor line 340
14. def OAI.SKGapCutoff.Regression.spinFieldSquareAverage line 355
15. lemma OAI.SKGapCutoff.Regression.continuous_spinFieldSquareAverage line 358
16. lemma OAI.SKGapCutoff.Regression.spinFieldSquareAverage_planted_exponential line 364
17. theorem OAI.SKGapCutoff.Regression.quenched_spinFieldSquareAverage_exponential line 380
18. lemma OAI.SKGapCutoff.Regression.spinFieldSquareAverage_abs_le_opNorm_sq line 391
19. def OAI.SKGapCutoff.Regression.gibbsSpinFieldSquareAverage line 402
20. theorem OAI.SKGapCutoff.Regression.gibbsSpinFieldSquareAverage_limit line 405