OAI/Probability/DilutedSpin/CavityTrialIdentity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.terminalRoot_cavity_marginal line 14
2. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.terminalRoot_cavity_increment line 38
3. def OAI.DilutedSpinGlass.cavityBondEnergy line 68
4. lemma OAI.DilutedSpinGlass.cavityBondEnergy_bound line 71
5. lemma OAI.DilutedSpinGlass.continuous_cavityBondEnergy line 76
6. lemma OAI.DilutedSpinGlass.continuous_cavitySiteEnergy line 83
7. lemma OAI.DilutedSpinGlass.trialLog_cavityBondEnergy line 98
8. lemma OAI.DilutedSpinGlass.integral_trial_cavityBondEnergy line 112
9. lemma OAI.DilutedSpinGlass.integral_trial_cavitySiteEnergy line 126
10. lemma OAI.DilutedSpinGlass.functional_cavity_trial line 142