OAI/Probability/DilutedSpin/MeasurableShapeEnergy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.FiniteLaw.covarianceEnergy_le_four line 13
2. lemma OAI.DilutedSpinGlass.PrescribedTree.measurable_child_expect_tilt line 43
3. lemma OAI.DilutedSpinGlass.PrescribedTree.measurable_childEnergy_tilt line 57
4. lemma OAI.DilutedSpinGlass.PrescribedTree.measurable_shapeEnergyAt_tilt line 74
5. lemma OAI.DilutedSpinGlass.PrescribedTree.shapeEnergyAt_le_four line 88
6. lemma OAI.DilutedSpinGlass.PrescribedTree.measurable_descendantEnergyAt_tilt line 101
7. lemma OAI.DilutedSpinGlass.PrescribedTree.descendantEnergyAt_le_four line 115