OAI/Probability/Perceptron/Cavity/CavityLabelAnnealed.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptronFreeEnergy.cavityLabelFullPartition line 12
2. lemma OAI.SphericalPerceptronFreeEnergy.cavityLabelFullPartition_measurable line 18
3. lemma OAI.SphericalPerceptronFreeEnergy.cavityLabelPartition_eq_product line 30
4. lemma OAI.SphericalPerceptronFreeEnergy.integrable_product_of_nonneg_conditional line 52
5. theorem OAI.SphericalPerceptronFreeEnergy.cavityLabel_uncap_annealed line 78
6. lemma OAI.SphericalPerceptronFreeEnergy.cavityLabel_capped_log_integrable line 126
7. lemma OAI.SphericalPerceptronFreeEnergy.cavityLabel_full_log_integrable line 135