OAI/Probability/FreeIsing/Gaussian/FreeLawNoise.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.treeNoisePMF line 14
2. lemma OAI.Problem367.treeNoisePMF_apply line 20
3. lemma OAI.Problem367.treeNoisePMF_toMeasure_singleton line 24
4. lemma OAI.Problem367.measurable_connectedSpinEncode_restrict line 31
5. lemma OAI.Problem367.HasFreeIsingLaw.connectedSpinEncode_atom line 40
6. lemma OAI.Problem367.HasFreeIsingLaw.map_connectedSpinEncode line 74
7. lemma OAI.Problem367.HasFreeIsingLaw.map_connectedSpinEncode_coord line 93
8. lemma OAI.Problem367.HasFreeIsingLaw.iIndepFun_connectedSpinEncode line 110