OAI/Probability/DilutedSpin/FullRootIncrement.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.PhysicalRoot.measurable_reorder_increment line 18
2. lemma OAI.DilutedSpinGlass.PhysicalRoot.measurable_energyRoot_increment line 25
3. lemma OAI.DilutedSpinGlass.PhysicalRoot.fullRoot_energy_increment line 37
4. lemma OAI.DilutedSpinGlass.measurable_cavityArrayValue_joint line 97
5. def OAI.DilutedSpinGlass.cavityPoissonValue line 125
6. lemma OAI.DilutedSpinGlass.measurable_cavityPoissonValue line 131
7. lemma OAI.DilutedSpinGlass.cavityPoissonValue_bound line 146
8. lemma OAI.DilutedSpinGlass.cavity_poisson_bridge line 172
9. lemma OAI.DilutedSpinGlass.KernelTower.Projects.prod_fst line 240
10. lemma OAI.DilutedSpinGlass.KernelTower.pathMap_fst line 251
11. def OAI.DilutedSpinGlass.PrescribedTree.selectCavity line 262
12. lemma OAI.DilutedSpinGlass.PrescribedTree.selectCavity_projects line 269
13. lemma OAI.DilutedSpinGlass.PrescribedTree.cavityProject_select line 288
14. lemma OAI.DilutedSpinGlass.PrescribedTree.cavityProject_pathSelect line 297