OAI/Probability/DilutedSpin/RootEncoding.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.measurable_packRoot_into line 13
2. def OAI.DilutedSpinGlass.HeterogeneousMarks.rootEncoding line 42
3. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_rootEncoding line 46
4. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_rootEncoding_joint line 59
5. def OAI.DilutedSpinGlass.HeterogeneousMarks.rootEncodingLaw line 64
6. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.rootEncoding_moment line 74
7. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.rootEncodingLaw_moment line 82