OAI/Probability/Perceptron/Cavity/CavityNormalizedIncrement.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptronFreeEnergy.cavityOldJoinedHamiltonian line 11
2. lemma OAI.SphericalPerceptronFreeEnergy.cavity_actual_old_log_identity line 17
3. theorem OAI.SphericalPerceptronFreeEnergy.cavity_normalized_old_increment_lower line 43
4. lemma OAI.SphericalPerceptronFreeEnergy.cavity_truncated_countable_kernel line 77
5. lemma OAI.SphericalPerceptronFreeEnergy.cavity_countable_kernel line 102
6. def OAI.SphericalPerceptronFreeEnergy.cavityCountableField line 120
7. lemma OAI.SphericalPerceptronFreeEnergy.cavityCountableField_measurable line 124
8. theorem OAI.SphericalPerceptronFreeEnergy.cavity_countable_moment line 134