OAI/Probability/DilutedSpin/FullSelectedError.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedDeviation line 15
2. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedDeviation_nonneg line 32
3. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedDeviation_split line 37
4. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedDeviation_bound line 57
5. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedRawScore_bound line 67
6. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_fullSelectedRawScore line 75
7. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_fullSelectedDeviation line 82