OAI/Probability/DilutedSpin/UpperTrial.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.UniversalDictionary.cavityProxy_envelope line 13
2. lemma OAI.DilutedSpinGlass.UniversalDictionary.cavityProxy_functional_bound line 34
3. lemma OAI.DilutedSpinGlass.trialSiteField_center line 57
4. lemma OAI.DilutedSpinGlass.trialSiteDisorder_center line 67
5. lemma OAI.DilutedSpinGlass.trialEdge_center line 82
6. lemma OAI.DilutedSpinGlass.functional_center line 99
7. lemma OAI.DilutedSpinGlass.KernelTower.pathMap_pathPrefix line 129
8. lemma OAI.DilutedSpinGlass.KernelTower.piTower_eq_pi line 137
9. lemma OAI.DilutedSpinGlass.KernelTower.piTower_pad line 147
10. lemma OAI.DilutedSpinGlass.KernelTower.proj_eq_pathMap line 162
11. def OAI.DilutedSpinGlass.PrescribedTree.finiteTrialLaw line 173
12. lemma OAI.DilutedSpinGlass.PrescribedTree.finite_trialLog line 177
13. lemma OAI.DilutedSpinGlass.PrescribedTree.edgeRoot_pad line 192