OAI/Probability/DilutedSpin/TerminalMeanField.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.HeterogeneousMarks.fieldEnergy line 14
2. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_fieldEnergy line 17
3. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.fieldEnergy_bound line 24
4. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.fieldEnergy_norm line 33
5. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.fieldEnergy_cons line 40
6. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.terminalMean_field_integrable line 44
7. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.averagedEnergyRoot_mark_projection line 63
8. lemma OAI.DilutedSpinGlass.FiniteLaw.expect_pi_curry line 91
9. lemma OAI.DilutedSpinGlass.KernelTower.pi_curry_projects line 104
10. lemma OAI.DilutedSpinGlass.KernelTower.pi_injective_projects line 111
11. lemma OAI.DilutedSpinGlass.KernelTower.pi_rect_castSucc_projects line 118