OAI/Probability/DilutedSpin/EnergyInsertionMean.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.PhysicalRoot.integrable_energyRoot_field_mean line 17
2. lemma OAI.DilutedSpinGlass.PhysicalRoot.averagedEnergyRoot_increment line 32
3. lemma OAI.DilutedSpinGlass.PhysicalRoot.energyRoot_increment_bound line 51
4. def OAI.DilutedSpinGlass.selectedCount line 68
5. def OAI.DilutedSpinGlass.selectRoot line 73
6. lemma OAI.DilutedSpinGlass.measurePreserving_selectRoot line 78
7. lemma OAI.DilutedSpinGlass.integral_selectRoot line 94