OAI/Probability/Perceptron/Variational/RoundedLaw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptronFreeEnergy.roundedLevelCode line 15
2. lemma OAI.SphericalPerceptronFreeEnergy.roundedLevelCode_measurable line 19
3. lemma OAI.SphericalPerceptronFreeEnergy.roundedLevelCode_mono line 23
4. theorem OAI.SphericalPerceptronFreeEnergy.indexedDepthLaw_eq_rounded_bulk line 26
5. def OAI.SphericalPerceptronFreeEnergy.depthMarkedDecode line 86
6. lemma OAI.SphericalPerceptronFreeEnergy.depthMarkedDecode_measurable line 90
7. lemma OAI.SphericalPerceptronFreeEnergy.gibbsProbabilityKernel_zero line 101
8. lemma OAI.SphericalPerceptronFreeEnergy.annealedInfiniteReplicaMeasure_zero line 110
9. theorem OAI.SphericalPerceptronFreeEnergy.cavityLabelMarkedLaw_eq_depth line 116