OAI/Probability/SKGap/Terminal/SingleSpinPlantedLaw.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.gaussianPDFReal_tilt line 21
2. lemma OAI.SKGapCutoff.gaussianReal_exponential_tilt line 31
3. lemma OAI.SKGapCutoff.pi_withDensity_ofReal_prod line 45
4. lemma OAI.SKGapCutoff.gaussianPi_exponential_tilt line 65
5. def OAI.SKGapCutoff.singleSpinPlantedLaw line 84
6. lemma OAI.SKGapCutoff.singleSpinPlantedLaw_eq_gaussianPi line 89
7. lemma OAI.SKGapCutoff.singleSpinPlantedLaw_probability line 105
8. def OAI.SKGapCutoff.plantedDisorderLaw line 110
9. lemma OAI.SKGapCutoff.plantedDisorderLaw_probability line 114
10. lemma OAI.SKGapCutoff.planted_density_sum line 129
11. lemma OAI.SKGapCutoff.plantedDisorderLaw_mixture line 138
12. lemma OAI.SKGapCutoff.lower_density_markov line 154
13. lemma OAI.SKGapCutoff.lower_density_markov_div line 166
14. lemma OAI.SKGapCutoff.planted_law_transfer line 176