OAI/Probability/Perceptron/Variational/RoundedCoupling.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptronFreeEnergy.timeGridRound line 13
2. lemma OAI.SphericalPerceptronFreeEnergy.timeGridRound_tendsto line 16
3. lemma OAI.SphericalPerceptronFreeEnergy.roundedTimeValue_code_ae line 20
4. lemma OAI.SphericalPerceptronFreeEnergy.roundedTimeValue_code_array_ae line 39
5. def OAI.SphericalPerceptronFreeEnergy.timeMarkedDecode line 59
6. lemma OAI.SphericalPerceptronFreeEnergy.timeMarkedDecode_measurable line 62
7. theorem OAI.SphericalPerceptronFreeEnergy.cavityLabelMarkedLaw_tendsto_graph line 73