OAI/Probability/SKGap/Matrix/DoublePlantLogNorm.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.doublePlantLogNorm line 77
2. def OAI.SKGapCutoff.doubleSpinPlantedLaw line 80
3. lemma OAI.SKGapCutoff.doubleSpinPlantedLaw_eq_gaussianPi line 86
4. lemma OAI.SKGapCutoff.doubleSpinPlantedLaw_probability line 105
5. def OAI.SKGapCutoff.doublePlantNorm line 110
6. lemma OAI.SKGapCutoff.doublePlantNorm_eq_sum line 113
7. lemma OAI.SKGapCutoff.doublePlantNorm_pos line 119
8. def OAI.SKGapCutoff.doublePlantWeight line 125
9. lemma OAI.SKGapCutoff.doublePlantWeight_pos line 128
10. lemma OAI.SKGapCutoff.doublePlantWeight_sum line 132
11. def OAI.SKGapCutoff.doublePlantedDisorderLaw line 137
12. lemma OAI.SKGapCutoff.doublePlantedDisorderLaw_probability line 142
13. def OAI.SKGapCutoff.doubleGibbsLExpectation line 154
14. lemma OAI.SKGapCutoff.measurable_doubleGibbsLExpectation line 160
15. lemma OAI.SKGapCutoff.double_planted_gibbs_density line 170
16. lemma OAI.SKGapCutoff.double_planted_gibbs_lintegral line 180
17. lemma OAI.SKGapCutoff.doublePlantWeight_eq_overlap_tilt line 233
18. lemma OAI.SKGapCutoff.doublePlantWeight_overlap_tail line 240