OAI/Probability/DilutedSpin/CompoundPhysicalMean.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.PhysicalRoot.energyRoot line 14
2. lemma OAI.DilutedSpinGlass.PhysicalRoot.energyRoot_lipschitz line 23
3. def OAI.DilutedSpinGlass.PhysicalRoot.rootSample line 36
4. lemma OAI.DilutedSpinGlass.PhysicalRoot.measurable_rootSample_fixed line 44
5. lemma OAI.DilutedSpinGlass.PhysicalRoot.measurable_rootSample line 59
6. lemma OAI.DilutedSpinGlass.PhysicalRoot.rootSample_bound line 73
7. lemma OAI.DilutedSpinGlass.PhysicalRoot.integral_compound_energyRoot line 84
8. lemma OAI.DilutedSpinGlass.PhysicalRoot.fullRoot_energy_integral line 102