OAI/Probability/DilutedSpin/TerminalMeanCavity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.terminalMean_cavity_marginal line 15
2. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.energyRoot_eq_locatedTerminalRoot line 33
3. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.averagedEnergyRoot_eq_terminalMean line 41
4. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.integrable_locatedTerminalRoot line 51
5. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.terminalMean_bound line 65
6. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.terminalMean_lipschitz line 87